ocaml GADT: зачем набирать файл. нужный?

В базовом примере GADT из §7.20 руководства по ocaml, что означает «тип а». ? Почему недостаточно объявить eval: a term -> a?

type _ term =
          | Int : int -> int term
          | Add : (int -> int -> int) term
          | App : ('b -> 'a) term * 'b term -> 'a term

        let rec eval : type a. a term -> a = function
          | Int n    -> n                 (* a = int *)
          | Add      -> (fun x y -> x+y)  (* a = int -> int -> int *)
          | App(f,x) -> (eval f) (eval x)

ocaml gadt locally-abstract-type
person Pierre G.    schedule 24.10.2015    source источник
comment
Я не являюсь теоретиком типов, но, читая ссылку, предоставленную @nnarklrh, мне кажется, что функция eval требует полиморфной рекурсии, а присутствие type a. ... отчасти является сигналом для включения ее поддержки. Если вы опустите type, вы получите ошибки, которых ожидаете от попытки использовать полиморфную рекурсию, когда это не разрешено.   -  person Jeffrey Scofield    schedule 24.10.2015

Ответы (1)


arrow_upward
5
arrow_downward

слайд на семинаре ML'2011 Жака хорошее введение. Идея использовать синтаксис локально абстрактного типа для введения универсальной переменной в области выражения.

person objmagic    schedule 24.10.2015