Help with data type for simple interpreter

Learning
1

Hi all, I’m just starting checking out OCaml. As an exercise, I’m trying to write a simple interpreter. I’m trying to define a polymorphic type 'a term such that the 'a parameter is the “type” of the term at the level of the internal language. Something like:

type 'a term =
  | Val of 'a
  | App of ('b -> 'a) term * 'b term ;;

I’d like to be able to do something like App(App(Val(+), Val(3)), Val(4)) : int term and defer to OCaml’s type-checker to infer 'b where necessary. Is it possible to place these kinds of constraints on a data type?

Thanks!

2

If you tried your example, you saw that it couldn’t work the way you defined it because 'b is unbound.
What you’re looking for is more involved than “basic” sum types, as you need 'b to be existentially quantified; this is called a GADT. This very forum contains many examples and discussions of the topic. Mind the syntax which is not exactly the same as plain sum types:

utop # type _ term =
| Val : 'a -> 'a term
| App : ('b->'a) term * 'b term -> 'a term;;
type _ term = Val : 'a -> 'a term | App : ('b -> 'a) term * 'b term -> 'a term
utop # App(App(Val(+), Val(3)), Val(4));;
- : int term = App (App (Val <fun>, Val <poly>), Val <poly>)
2 Likes