Здравствуйте, achmed, Вы писали:
A>Хочу применить функцию саму к себе, как комбинатор A>на ocaml A>
A># let k (x:'a -> 'b) = x x;;
A>Characters 23-24:
A> let k (x:'a -> 'b) = x x;;
A> ^
A>This expression has type 'a -> 'b but is here used with type 'a
A>
A>почему 'a не может параметризоваться как 'a -> 'b?
Что значит "параметризоваться"? Унификация здесь ведет к бесконечной рекурсии при выводе типа. Попробуй подумать, что будет при вызове твоего k с любым конкретным типом, например, k sin.
Спасти дело можно либо так
let k x a = x (x a)
(если ты это имел ввиду), либо двигаясь в сторону комбинатора неподвижной точки
Здравствуйте, achmed, Вы писали:
A>Хочу применить функцию саму к себе, как комбинатор A>на ocaml
A># let k (x:'a -> 'b) = x x;;
A>Characters 23-24:
A> let k (x:'a -> 'b) = x x;;
A> ^
A>This expression has type 'a -> 'b but is here used with type 'a
A>почему 'a не может параметризоваться как 'a -> 'b?
Насколько я помню, Харрисон во «Введении в функциональное программирование» рассматривал этот вопрос, в том числе в применении к ОКамлу, сравнивая с Лиспом.
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, achmed, Вы писали:
A>>Хочу применить функцию саму к себе, как комбинатор A>>на ocaml A>>
A>># let k (x:'a -> 'b) = x x;;
A>>Characters 23-24:
A>> let k (x:'a -> 'b) = x x;;
A>> ^
A>>This expression has type 'a -> 'b but is here used with type 'a
A>>
A>>почему 'a не может параметризоваться как 'a -> 'b?
D>Что значит "параметризоваться"? Унификация здесь ведет к бесконечной рекурсии при выводе типа. Попробуй подумать, что будет при вызове твоего k с любым конкретным типом,
думал что будет ('a -> 'b) -> 'c
D>например, k sin.
понятно что sin не может быть применен сам к себе
но в каких то частных случаях это возможно, например
# (fun a -> fun b -> a)(fun a -> fun b -> a);;
- : '_a -> '_b -> '_c -> '_b = <fun>
D>Спасти дело можно либо так D>
D>let k x a = x (x a)
D>
D>(если ты это имел ввиду), либо двигаясь в сторону комбинатора неподвижной точки D>
D>let fix x = x (fix x)
D>
да, вопрос родился из размышлений о комбинаторе Y
Y=λf.(λx.f(xx))(λx.f(xx))
Здравствуйте, Qbit86, Вы писали:
Q>Насколько я помню, Харрисон во «Введении в функциональное программирование» рассматривал этот вопрос, в том числе в применении к ОКамлу, сравнивая с Лиспом.
В книге приводится реализация Y с помощью рекурсивного типа на caml ligth, но без сравнения с LISP.
Пытаюсь понять почему нельзя реализовать Y без рекурсивного типа в caml.
Здравствуйте, achmed, Вы писали:
A>В книге приводится реализация Y с помощью рекурсивного типа на caml ligth, но без сравнения с LISP. A>Пытаюсь понять почему нельзя реализовать Y без рекурсивного типа в caml.
Потому что он основан на типизированном лямбда-исчислении.
Здравствуйте, nikov, Вы писали:
N>Потому что он [OCaml] основан на типизированном лямбда-исчислении.
А Лисп — на бестиповом. Это я и имел в виду, когда говорил, что Харрисон приводил сравнение с Лиспом. Но achmed говорит, что не приводил — может быть, не помню деталей.
Здравствуйте, achmed, Вы писали:
A>Хочу применить функцию саму к себе, как комбинатор A>на ocaml A>
A># let k (x:'a -> 'b) = x x;;
A>Characters 23-24:
A> let k (x:'a -> 'b) = x x;;
A> ^
A>This expression has type 'a -> 'b but is here used with type 'a
A>
A>почему 'a не может параметризоваться как 'a -> 'b?
Хиндли-Милнер безымянные бесконечные типы не позволяет, они не проходят occurs check при унификации (см. TAPL). В случае окамла есть волшебный ключик -rectypes, который делает ровно то, что ты хотел:
$ ocaml -rectypes
Objective Caml version 3.09.1
# let f x = x x ;;
val f : ('a -> 'b as 'a) -> 'b = <fun>
Но лучше им не пользоваться, that way madness lies.
Стандартное решение: рекурсивные типы должны быть именованными:
type 'b recfun = Fun of ('b recfun -> 'b) ;;
let apply (Fun f) x = f x
let f x = apply x x
Здравствуйте, palm mute, Вы писали:
PM>В случае окамла есть волшебный ключик -rectypes, который делает ровно то, что ты хотел:
Круто, теперь можно записать Y почти в первостепенном виде
# let y f = (fun x z -> f (x x) z) (fun x z -> f (x x) z);;
val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
# let fact = y (fun f n -> if n = 0 then 1 else n * f(n-1));;
val fact : int -> int = <fun>
# fact 5;;
- : int = 120
PM>>В случае окамла есть волшебный ключик -rectypes, который делает ровно то, что ты хотел: A>Круто, теперь можно записать Y почти в первостепенном виде
A>
A># let y f = (fun x z -> f (x x) z) (fun x z -> f (x x) z);;
A>val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
A># let fact = y (fun f n -> if n = 0 then 1 else n * f(n-1));;
A>val fact : int -> int = <fun>
A># fact 5;;
A>- : int = 120
A>
Минус в том, что выводилка типов становится очень креативной и для многих откровенно ошибочных функций выводится некий тип, и только потом, при попытке их использования, ты получишь невнятное сообщение об ошибке.
Например:
let rec map f = function
[] -> [[[f]]]
| (x::xs) -> f x :: map f xs
Для map выводится дикий тип ('b -> ('a list list as 'c) as 'a) -> 'b list -> 'c list
Здравствуйте, achmed, Вы писали:
A>Хочу применить функцию саму к себе, как комбинатор A>на ocaml A>
A># let k (x:'a -> 'b) = x x;;
A>Characters 23-24:
A> let k (x:'a -> 'b) = x x;;
A> ^
A>This expression has type 'a -> 'b but is here used with type 'a
A>
