I am trying for the (real) first time to solve a problem using a GADT.
I wan’t to represente a function specification using the type spec:
type _ spec = | Elem : 'a Gen.t -> 'a spec | Arrow : 'a spec * 'b spec -> ('a -> 'b) spec let (^>) x y = Arrow (x, y) let int = Term Gen.int let foo : (int -> int -> int) spec = int ^> int ^> int
Then, from this function spec, I would like to transform it into an application through a
type _ expr = | Apply : ('a -> 'b) expr * 'a expr -> 'b expr | Term : 'a -> 'a expr | Fun : ('a -> 'b) -> ('a -> 'b) expr let rec eval_expr : type a. a expr -> a = function | Apply (f, x) -> (eval_expr f) (eval_expr x) | Term x -> x | Fun f -> f
The problem I currently have is typing of that transformation:
let rec spec_to_expr : type a b. a spec -> a expr -> b expr = fun spec expr -> match spec with | Arrow (Elem x, y) -> let x = Gen.sample x in let expr = Apply (expr, Term x) in spec_to_expr y expr | Elem x -> let x = Gen.sample x in Apply (expr, Term x) | _ -> assert false (* Typing error: *) | Elem x -> Apply (expr, Term x) ^^^^ Error: This expression has type a expr but an expression was expected of type ('a -> b) expr Type a is not compatible with type 'a -> b
I get that I have defined expr as an
a expr, but in:
| Arrow (Elem x, y) -> let x = Gen.sample x in let expr = Apply (expr, Term x) in spec_to_expr y expr
expr has the same type but it does not appear to raise a typing error, and I don’t understand
why it is allowed in that case ?
I’m sorry if my question does not make any sens, but that’s really one of the first times I’m trying
to implement a GADT.