I work with a small language which has a
literal type in its AST that’s similar to this (I removed most cases because they’re not relevant):
type literal = | Null | Bool of bool | Num of float | LList of literal list
I don’t think I need to spend too much time interpreting the different cases.
Because ASTs are the textbook example for GADTs, trying GADTs here has been in my todo list for quite a while.
So I did this:
type null type llist (* not sure about those phantom types *) type _ literal = | Null : null literal | Bool : bool -> bool literal | Num : float -> float literal | LList : ??? -> llist literal
The issue is that LLists are polymorphic. They can contain anything, so I don’t know how to express it.
One might think that adding ADTs has little meaning here but I think there are some nice things to do.
First of all, my language has expressions, and I would want to have a function with the following signature
val eval_expr : type a. a expr -> a literal
Which brings me to my second question, what’s the type of a variable in an AST ?
type _ expr = | Lit : 'a literal -> 'a expr | Plus : float expr -> float expr -> float expr | ListCons : 'a expr -> llist expr -> llist expr | Var : string -> 'a expr (* ??? *)
Moreover, my language also has (logic) formulae which are basically boolean expressions with quantifiers.
Right now, we have a function with the following signature:
val lift_expr : expr -> formula
Which has a lot of failing cases, and I would like to use GADTs to have something more like
val lift_expr : bool expr -> formula
And that would even allow me to rewrite the formula type as something similar to this:
type formula = | QF of bool formula | Forall of var list * formula
instead of having
formula being basically a duplicate of expr with less cases and quantifiers.
I don’t know how clear that is, but to summarise, here are my two questions:
- In that GADT literal type, what should be the type of the
LListconstructor to accept any kind of literal list ?
- In an AST that has variables which are dynamically typed, what would be the definition for a nice GADT ?
And a more global question: are GADTs even interesting in my case ?
Thank you !