Typing of GADT from function declaration

Learning
1

Hello,

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 expression:

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.

2

In the Arrow branch, matching on the Arrow constructor refines the type a into $0 -> $1. This is not the case in the Elem branch.

There are few more issues with your code. First, in

let rec spec_to_expr : type a b. a spec -> a expr -> b expr

what is b?

Second, in

type _ expr =
  | Apply : ('a -> 'b) expr * 'a expr -> 'b expr
  | Term : 'a -> 'a expr
  | Fun : ('a -> 'b) -> ('a -> 'b) expr

the Fun constructor is redundant with the Term one.
(And I don’t see what spec_to_expr is supposed to do).

3

the Fun constructor is redundant with the Term one.

Indeed, the goal was to have a kind of explicit name.

–

Spec is supposed to give a reprensentation of a function with Elem representing a generator for its type.
Where expr is supposed to be the full application of the function described in spec using generators.

let spec = int ^> int ^> int
let f x y = x + y

let expr =
  let expr = spec_to_expr spec (Fun f) in
  (* expr = Apply ( Apply (Fun f, Term <1>),
                    Term <2> )
     where <_> is a randomly generated value *)
  eval_expr expr = 3

–

what is b

b is the expression where I have applied one more Term to the application.

(int -> int) expr => int expr
4

The function might be wrong in that way and should more be something like:


let rec spec_to_expr : type a b. a spec -> a expr -> b expr =
 fun spec expr ->
  match spec with
  (* a = $0 -> $1 and b = $1 *)
  | Arrow (Elem x, y) ->
      let x = Gen.sample x in
      let expr = Apply (expr, Term x) in
      spec_to_expr y expr
  (* a = $0  and v has type $0, type clash with b *)
  | Elem x ->
      let v = Gen.sample x in
      Term v
  | _ -> assert false
5

Then you have the issue that your types allow higher-order function that doesn’t match this model.
Similarly a spec -> a expr -> (the expression where I have applied one more Term to the application) expr is not a valid type in OCaml.

It seems that the type that you wanted for spec is something akin to

type ('fn, 'r) spec =
| Term : ('r,'r) spec
| Arrow: 'a Gen.t * ('f,'r) spec -> ('a -> 'f, 'r) spec

With this definition the type of spec_to_expr becomes ('a,'b) spec -> 'a expr -> 'b expr.

6

I’m not sure to understand what’s inside Arrow, especially ('f , 'r)

7

There was a missing spec is 'a Gen.t * ('fn, 'r) spec -> ('a -> 'fn, 'r) spec.

Here the advantage of this type is that you can only cons a generator (and not a full spec) to an existing spec. Moreover, the result type variable 'r points to the resulting type after application of the fn type to all generators in the list. (and indeed it would be possible to define spec as a heterogeneous list).

1 Like
8

Thanks a lot!

cons is a better idea, I would have to enforce it with constructors otherwise.

Here’s the code for anyone that’d be interested:

type ('fn, 'r) spec =
  | Term : ('r, 'r) spec
  | Arrow : 'a Gen.t * ('fn, 'r) spec -> ('a -> 'fn, 'r) spec

type _ expr =
  | Apply : ('a -> 'b) expr * 'a expr -> 'b expr
  | Term : 'a -> 'a expr
  | Fun : ('a -> 'b) -> ('a -> 'b) expr

let rec spec_to_expr : type a b. (a, b) spec -> a expr -> b expr =
 fun spec expr ->
  match spec with
  | Term -> expr
  | Arrow (gen, spec) ->
      let x = Gen.sample gen in
      let expr = Apply (expr, Term x) in
      spec_to_expr spec expr

Having 'r pointing on the resulting type is a great idea. Thanks again for your help :slight_smile: