тип функций высокого порядка - PullRequest
Новая
       65

тип функций высокого порядка

7 голосов
/ 14 декабря 2010

если я укажу (я думаю) правильный тип для функции высокого порядка, компилятор OCaml отклонит секунду использования этой функции.

код 

let foo ():string  =
    let f: ('a -> string) -> 'a -> string = fun g v -> g v
    in let h = string_of_int
    in let i = string_of_float
    in let x = f h 23
    in let y = f i 23.0
    in x ^ y

приводит к следующему сообщению об ошибке 

File "test.ml", line 6, characters 14-15:
Error: This expression has type float -> string
       but an expression was expected of type int -> string

Таким образом, первое использование f, по-видимому, фиксирует тип его первого параметра на int -> string. Я мог это понять. Но что я не понимаю, так это то, что пропущенное ограничение типа f решает проблему. 

let foo ():string  =
    let f g v = g v
    in let h = string_of_int
    in let i = string_of_float
    in let x = f h 23
    in let y = f i 23.0
    in x ^ y

И перемещение f в глобальную область также устраняет проблему: 

let f: ('a -> string) -> 'a -> string = fun g v -> g v

let foo ():string  =
  let h = string_of_int
  in let i = string_of_float
  in let x = f h 23
  in let y = f i 23.0
  in x ^ y

Почему первый пример не компилируется, а более поздние?

Ответы [ 3 ]

9 голосов
/ 14 декабря 2010

Позвольте мне использовать более простой пример, иллюстрирующий проблему. 

# let cons0 (x : 'a) (y : 'a list) = x :: y;;
val cons0 : 'a -> 'a list -> 'a list = <fun>
# let cons1 (x : 'a) (y : 'a list) = x :: y in cons1 1 [];;
- : int list = [1]
# let cons2 (x : 'a) (y : 'a list) = x :: y in (cons2 1 [], cons2 true []);;
This expression has type bool but is here used with type int
# let cons3 x y = x :: y in (cons3 1 [], cons3 true []);;
- : int list * bool list = ([1], [true])

cons0 - это определение полиморфной функции, определенное в глобальной области видимости.Это просто тривиальная оболочка для оператора ::.Неудивительно, что определение работает.cons1 почти совпадает с cons0, за исключением того, что его область действия ограничена выражением в теле in.Изменение масштаба выглядит безобидным, и, конечно же, оно проверяет тип.cons3 опять та же самая функция, без аннотации типов, и мы можем использовать ее полиморфно в теле in.

Так что же не так с cons2?Проблема в объеме 'a: это целая фраза верхнего уровня.Семантика фразы, которая определяет cons2, является 

for some type 'a, (let cons2 (x : 'a) (y : 'a list) = ... in ...)

, поскольку 'a должен быть совместим с int (из-за cons3 1 []) и с bool (из-за cons3 true [],'a не может быть реализовано. Следовательно, фраза имеет неправильный тип.

Если вам нравится думать о типизации ML в терминах ее обычного алгоритма вывода типов, каждая явная переменная пользователя вводит набор ограничений.в алгоритме объединения. Здесь ограничения: 'a = "type of the parameter x" и ' = "type of the parameter y". Но область действия 'a - это целая фраза, она не обобщена ни в одной внутренней области. Таким образом, int и bool оба в конечном итоге объединяются вНеобобщенный 'a.

Последние версии OCaml вводят переменные типа scoped (как в ответ Ники Йошиути ). Такой же эффект мог быть достигнут с локальным модулем в более ранних версиях (≥2.0): 

let module M = struct
    let cons2 (x : 'a) (y : 'a list) = x :: y
  end in
(M.cons2 1 [], M.cons2 true []);;

(Примечание по стандартным MLers: это единственное место, где OCaml и SML отличаются.)

4 голосов
/ 14 декабря 2010

Это настоящий головокружитель, и я не удивлюсь, если это ошибка компилятора.Тем не менее, вы можете делать то, что вы хотите, явно указав тип: 

let f (type t) (g: t->string) (v: t) = g v in

Из руководства: http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#htoc108

Редактировать:

Это также работает: 

let f g v:string = g v in

, который имеет искомую сигнатуру типа: ('a -> string) -> 'a -> string

Странно, что это не работает, когда вы аннотируете тип аргументов.

EDIT:

Аннотации полиморфного типа имеют специальный синтаксис: 

let f: 'a. ('a -> string)-> 'a -> string = fun g v -> g v in

И тип должен быть полиморфным: http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc79

0 голосов
/ 14 декабря 2010

В качестве ориентира компилируется эквивалент F # 

let foo ():string  = 
    let f: ('a -> string) -> 'a -> string = fun g v -> g v 
    let h = string 
    let i = string
    let x = f h 23 
    let y = f i 23.0 
    x ^ y

...