# Typing of GADT from function declaration
**URL:** https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148
**Category:** Learning
**Created:** [July 15, 2021, 9:19am UTC](https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148 "2021-07-15T09:19:16Z")
**Posts on this page:** 8
**Page:** 1
### Author:  [@vch9](https://discuss.ocaml.org/u/vch9)
#### Post date: [July 15, 2021, 9:19am UTC](https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148/1 "2021-07-15T09:19:16Z")
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:
```ocaml
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:
```ocaml
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:
```ocaml
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:
```ocaml
| 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.
---
### Author:  [@octachron](https://discuss.ocaml.org/u/octachron)
#### Post date: [July 15, 2021, 10:13am UTC](https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148/2 "2021-07-15T10:13:33Z")
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
```ocaml
let rec spec_to_expr : type a b. a spec -> a expr -> b expr
```
what is `b`?
Second, in
```ocaml
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).
---
### Author:  [@vch9](https://discuss.ocaml.org/u/vch9)
#### Post date: [July 15, 2021, 10:58am UTC](https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148/3 "2021-07-15T10:58:43Z")
> 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.
```ocaml
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.
```ocaml
(int -> int) expr => int expr
```
---
### Author:  [@vch9](https://discuss.ocaml.org/u/vch9)
#### Post date: [July 15, 2021, 12:04pm UTC](https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148/4 "2021-07-15T12:04:00Z")
The function might be wrong in that way and should more be something like:
```ocaml
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
```
---
### Author:  [@octachron](https://discuss.ocaml.org/u/octachron)
#### Post date: [July 15, 2021, 12:07pm UTC](https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148/5 "2021-07-15T12:07:21Z")
> [@vch9](#):
>
> Spec is supposed to give a reprensentation of a function with `Elem` representing a generator for its type.
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
```ocaml
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`.
---
### Author:  [@vch9](https://discuss.ocaml.org/u/vch9)
#### Post date: [July 15, 2021, 12:53pm UTC](https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148/6 "2021-07-15T12:53:55Z")
> [@octachron](#):
>
> ```auto
> type ('fn, 'r) spec =
> | Term : ('r,'r) spec
> | Arrow: 'a Gen.t * ('f,'r) -> ('a -> 'f, 'r) spec
>
> ```
I’m not sure to understand what’s inside `Arrow`, especially `('f , 'r)`
---
### Author:  [@octachron](https://discuss.ocaml.org/u/octachron)
#### Post date: [July 15, 2021, 1:10pm UTC](https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148/7 "2021-07-15T13:10:09Z")
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).
---
### Author:  [@vch9](https://discuss.ocaml.org/u/vch9)
#### Post date: [July 15, 2021, 1:38pm UTC](https://discuss.ocaml.org/t/typing-of-gadt-from-function-declaration/8148/8 "2021-07-15T13:38:42Z")
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:
```ocaml
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 🙂