GADTs для представления функций приложения с несколькими параметрами (AST)

Question

я видел в руководстве OCaml этот пример, чтобы использовать GADT для AST с применением функции:

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 
    | Add  -> (fun x y -> x+y) 
    | App(f,x) -> (eval f) (eval x) 

Это правильный способ представления приложения функции для язык не поддержка частичного применения?

Есть ли способ сделать приложение поддержки GADT с произвольным количеством аргументов?

И, наконец, GADT - хороший способ представить типизированный АСТ? Есть ли альтернатива?

Answer 1

Ну, частичная Eval уже работает здесь:

# eval (App(App(Add, Int 3),Int 4)) ;; 
- : int = 7 

# eval (App(Add, Int 3)) ;; 
- : int -> int = <fun> 

# eval (App(Add, Int 3)) 4 ;; 
- : int = 7 

То, что вы не в этой маленькой gadt это абстракция (лямбды), но это, безусловно, можно добавить его.

Если вас интересует эта тема, существует обширная (академическая) литература. This В документе представлена ​​различная кодировка, которая поддерживает частичную оценку.

Существуют также решения без гадта, как показано в this paper.

В целом, GADT - очень интересный способ представить оценщиков. Они, как правило, немного сокращаются, когда вы пытаетесь преобразовать AST для компиляций (но есть ways).

Кроме того, вы должны иметь в виду, что вы кодируете систему типов языка, который вы определяете на своем языке хоста, а это значит, что вам нужна кодировка требуемой функции типа. Иногда это сложно.

Редактировать: способ иметь GADT не, поддерживающий частичный eval, должен иметь специальный тип значения, не содержащий функций, и тип «функционального значения» с функциями. Принимая простейшее представление первой статьи, мы можем изменить его таким образом:

type _ v = 
    | Int : int -> int v 
    | String : string -> string v 

and _ vf = 
    | Base : 'a v -> ('a v) vf 
    | Fun : ('a vf -> 'b vf) -> ('a -> 'b) vf 

and _ t = 
    | Val : 'a vf -> 'a t 
    | Lam : ('a vf -> 'b t) -> ('a -> 'b) t 
    | App : ('a -> 'b) t * 'a t -> 'b t 

let get_val : type a . a v -> a = function 
    | Int i -> i 
    | String s -> s 

let rec reduce : type a . a t -> a vf = function 
    | Val x -> x 
    | Lam f -> Fun (fun x -> reduce (f x)) 
    | App (f, x) -> let Fun f = reduce f in f (reduce x) 

let eval t = 
    let Base v = reduce t in get_val v 

(* Perfectly defined expressions. *) 
let f = Lam (fun x -> Lam (fun y -> Val x)) 
let t = App (f, Val (Base (Int 3))) 
(* We can reduce t to a functional value. *) 
let x = reduce t 
(* But we can't eval it, it's a type error. *) 
let y = eval t 

(* HOF are authorized. *) 
let app = Lam (fun f -> Lam (fun y -> App(Val f, Val y))) 

Вы можете сделать это arbitrarly более сложным, следуя ваши потребности, важное свойство является то, что 'a v типа не может производить функции.