Thanks for the help everyone, I wrote a post on using GADTs based on
my explorations:
https://bluishcoder.co.nz/2018/10/16/generalized-algebraic-data-types-in-ats.html
I'll have a play around with some of the other ideas. Trying some of
the other common GADT examples tends to hit the similar
Chris,
What if a runtime tag for type is introduced?
datatype rtti (t@ype) =
| Rbool(bool)
| Rint(int)
and then in Eq:
| Eq(bool) of (rtti(a), Expr a, Expr a)
during evalution there would be some kind of dynamic check on the tag as
well.
Another idea is to make [eval] evaluate to
It's easier if you split up Eq
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
datatype Expr(a:t@ype) =
| I(int) of int
| B(bool) of bool
| Add(int) of (Expr int, Expr int)
| Mul(int) of (Expr int, Expr int)
| Eqi(bool) of (Expr int, Expr int)
|
This is not pretty but it is the closest thing I can come up with at the
moment:
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
datatype xint = I of int
datatype xbool = B of bool
extern
fun
xadd : (xint, xint) -> xint
extern
fun
xmul : (xint, xint)
I annotated your code as follows:
fun{a:t@ype} eval(x:Expr a): a =
case+ x of
| I i => i
| B b => b
| Add (t1, t2) => eval(t1) + eval(t2)
| Mul (t1, t2) => eval(t1) * eval(t2)
| Eq{a2}(t1, t2) => equals(eval(t1), eval(t2))
As a2 can be any type, the ATS compiler cannot
