GADT question

[Chris Double]

I have some GADT code that fails at the C compilation stage. It's a variant of:

https://gist.github.com/doublec/a3cc8f3431cabe9a319c8e7ba27e7890

But the Eq constructor of Expr uses the type index instead of being
'int' so equality can be done against booleans and ints. The full code
is:

----------------8<---------------
#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)
| Eq(bool) of (Expr a, Expr a)

extern fun{a:t@ype} equals(t1:a, t2:a): bool
implement equals<int>(t1,t2) = g0int_eq(t1,t2)
implement equals<bool>(t1,t2) = eq_bool0_bool0(t1,t2)

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 (t1, t2) => equals(t1, t2)

implement main0() = let
val term1 = Eq(I(5), Add(I(1), I(4)))
val term2 = Mul(I(2), I(4))
val res1 = eval(term1)
val res2 = eval(term2)
in
println!("res1=", res1, " and res2=", res2)
end
----------------8<---------------

This fails to compile at the C stage with:

In file included from arith3_dats.c:15:0:
arith3_dats.c: In function ‘eval_2__2__1’:
arith3_dats.c:1098:24: error: ‘PMVtmpltcstmat’ undeclared (first use
in this function)
ATSINSmove(tmpret2__1,
PMVtmpltcstmat[0](equals<S2EVar(5554)>)(tmp9__1, tmp10__1)) ;
^
ATS2-Postiats-0.3.11//ccomp/runtime/pats_ccomp_instrset.h:276:37:
note: in definition of macro ‘ATSINSmove’
#define ATSINSmove(tmp, val) (tmp = val)
....

Any thoughts on what I'm doing wrong?

--
https://bluishcoder.co.nz

[Hongwei Xi]

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<int>(t1) + eval<int>(t2)
    | Mul (t1, t2) => eval<int>(t1) * eval<int>(t2)
    | Eq{a2}(t1, t2) => equals<a2>(eval<a2>(t1), eval<a2>(t2))

As a2 can be any type, the ATS compiler cannot find code for equals<a2>

(nor for eval<a2>).

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CALn1vHGGZyh8VFq3p63LRtWxjvGx-mXg1f_dBAZHR99hmwTQsg%40mail.gmail.com.

[Hongwei Xi]

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) -> xint
  overload + with xadd
  overload * with xmul

  datatype Expr(a:type)  =
    | Int(xint) of xint
    | Bool(xbool) of xbool
    | Add(xint) of (Expr xint, Expr xint)
    | Mul(xint) of (Expr xint, Expr xint)
    | Eq(xbool) of ((a, a) -> bool, Expr a, Expr a)

  fun
  eval{a:type}(x:Expr a): a =
    case+ x of
    | Int i => i
    | Bool b => b

    | Add (t1, t2) => eval(t1) + eval(t2)
    | Mul (t1, t2) => eval(t1) * eval(t2)

    | Eq(eq, t1, t2) => B(eq(eval(t1), eval(t2)))

[Julian Fondren]

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) 
  | Eqb(bool) of (Expr bool, Expr bool) 

extern fun{a:t@ype} equals(t1:a, t2:a): bool 
implement equals<int>(t1,t2) = g0int_eq(t1,t2) 
implement equals<bool>(t1,t2) = eq_bool0_bool0(t1,t2) 

extern fun {a:t@ype} eval(x:Expr a): a

implement eval<int>(x) =
  case- x of 
  | I i => i 
  | Add (t1, t2) => eval(t1) + eval(t2) 
  | Mul (t1, t2) => eval(t1) * eval(t2) 

implement eval<bool>(x) =
  case- x of 
  | B b => b 
  | Eqi (t1, t2) => equals<int>(eval(t1), eval(t2))
  | Eqb (t1, t2) => equals<bool>(eval(t1), eval(t2))

implement main0() = let 
  val term1 = Eqi(I(5), Add(I(1), I(4))) 
  val term2 = Mul(I(2), I(4)) 
  val term3 = Eqb(B(true), B(false))

  val res1 = eval(term1) 
  val res2 = eval(term2)

 
  val res3 = eval(term3)
in 
  println!("res1=", res1, " res2=", res2, " and res3=", res3) 
end 

[Artyom Shalkhakov]

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 some kind of type of values. This type could be represented by a flat tagged union. Then you could do a check on the tag of the union at runtime, and select appropriate function to do the equality checking. Essentially what HX proposed, but with a flat unboxed type representing the values.

[Chris Double]

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 issue of the
generated C code not compiling due to not ascertaining the type to
pass to a template function. I imagine there are more "ATS"-ish ways
of solving the related problems that don't involve GADTs, or rework
things so that polymorphic functions are used instead. I'll do more
experimenting in those areas.

--
http://bluishcoder.co.nz