On Tue, Jan 7, 2020 at 2:25 PM wrote: > ... 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 = 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