GADTs for Representing Function Application with Multiple Parameters (AST)

Question

I saw in the OCaml manual this example to use GADT for an AST with function application:

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)

Is this the right way of representing function application for a language not supporting partial application?

Is there a way to make a GADT supporting function application with an arbitrary number of arguments?

Finally, is GADT a good way to represent a typed AST? Is there any alternative?

Answer 1

Well, partial eval already works here:

# 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   

What you don't have in this small gadt is abstraction (lambdas), but it's definitely possible to add it.

If you are interested in the topic, there is an abundant (academic) literature. This paper presents various encoding that supports partial evaluation.

There are also non-Gadt solutions, as shown in this paper.

In general, GADT are a very interesting way to represent evaluators. They tend to fall a bit short when you try to transform the AST for compilations (but there are ways).

Also, you have to keep in mind that you are encoding the type system of the language you are defining in your host language, which means that you need an encoding of the type feature you want. Sometimes, it's tricky.

Edit: A way to have a GADT not supporting partial eval is to have a special value type not containing functions and a "functional value" type with functions. Taking the simplest representation of the first paper, we can modify it that way:

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

You can make that arbitrarly more complicated, following your needs, the important property is that the 'a v type can't produce functions.