... but using a GADT:
---
module Gadt =
struct
type _ term =
| Int : int -> int term
| Add : (int -> int -> int) term
| App : ('b -> 'a) term * 'b term -> 'a term
let rec fold : type a. 'r -> ('r -> _ term -> 'r) -> 'r = fun i f -> function
| Int _ as t -> f i t
| Add -> f i Add
(*
^ Error: This pattern matches values of type (int -> int -> int) term
but a pattern was expected which matches values of type int term
Type int -> int -> int is not compatible with type int
*)
| App (x, y) as t -> f (fold (fold i f x) f y) t
end
---
I've tried other variants of the syntax and got many encouragements but no green flag from the type-checker.
Why is the compiler expecting an int term in there? I though the whole point of the `type a. ...` syntax was to allow the matched type to vary from one pattern to the next?
Is there a way to do this?
It is the limitation of the let-bound polymorphism. A parameter of a function is monomorphic in its body. The classical example doesn't even reference any GADT,
let example f = f "hello", f 42
It won't compile even though we can provide a polymorphic function that can applied both to integers and to strings, e.g., `exampe (fun x -> x)` should be possible, but not, because of the let-bounded polymorphism. There are a few solutions available in OCaml, the simplest is to use records, e.g.,
type app = {apply : 'a. 'a -> 'a}
let example {apply} = apply "hello", apply 42;;
val example : app -> string * int = <fun>
Now we have `app` that is polymorphic.
In your case, I would define a visitor type, e.g.,
type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r}
let rec fold : type a. 'r -> 'r visitor -> a term -> 'r =
fun i f t -> match t with
| Int _ as t -> f.visit i t
| Add as t -> f.visit i t
| App (x,y) as t ->
let i = fold i f x in
let i = fold i f y in
f.visit i t
Cheers,
Ivan Gotovchits