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

Ну, тут уже работает partial 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, как показано в этой статье.

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

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

Изменить. Один из способов сделать так, чтобы GADT не поддерживал частичную оценку, заключается в наличии специального типа значения, не содержащего функций, и типа "функционального значения" с функциями. Взяв простейшее представление первой статьи, мы можем изменить его следующим образом:

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)))

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