Re: GADT question
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 -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@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/CALn1vHGkJj8P9o-wySGC8BHQpCq31r6qmms5oA3AfRLJpc2saA%40mail.gmail.com.
Re: GADT question
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.
On Tuesday, October 16, 2018 at 4:51:15 AM UTC+3, Chris Double wrote:
>
> 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(t1,t2) = g0int_eq(t1,t2)
> implement equals(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)(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
>
--
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@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/3fa603b6-eda2-4f0e-b5ff-b69ff2ed6c27%40googlegroups.com.
Re: GADT question
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(t1,t2) = g0int_eq(t1,t2)
implement equals(t1,t2) = eq_bool0_bool0(t1,t2)
extern fun {a:t@ype} eval(x:Expr a): a
implement eval(x) =
case- x of
| I i => i
| Add (t1, t2) => eval(t1) + eval(t2)
| Mul (t1, t2) => eval(t1) * eval(t2)
implement eval(x) =
case- x of
| B b => b
| Eqi (t1, t2) => equals(eval(t1), eval(t2))
| Eqb (t1, t2) => equals(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
On Monday, October 15, 2018 at 8:51:15 PM UTC-5, Chris Double wrote:
>
> 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(t1,t2) = g0int_eq(t1,t2)
> implement equals(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)(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
>
--
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@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/de1a3962-e1b1-42d5-82ef-0d1980b68ef4%40googlegroups.com.
Re: GADT question
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)))
On Mon, Oct 15, 2018 at 10:12 PM Hongwei Xi wrote:
> 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 find code for equals
> (nor for eval).
>
>
> On Mon, Oct 15, 2018 at 9:51 PM Chris Double
> wrote:
>
>> 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(t1,t2) = g0int_eq(t1,t2)
>> implement equals(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)(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
>>
>> --
>> 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-users+unsubscr...@googlegroups.com.
>> To post to this group, send email to ats-lang-users@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
>> .
>>
>
--
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@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/CAPPSPLpBA892O11L2L6afWZriKzfjP3Cw%3Dz7JP%2BmERk1d0aszw%40mail.gmail.com.
Re: GADT question
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 find code for equals
(nor for eval).
On Mon, Oct 15, 2018 at 9:51 PM Chris Double
wrote:
> 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(t1,t2) = g0int_eq(t1,t2)
> implement equals(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)(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
>
> --
> 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-users+unsubscr...@googlegroups.com.
> To post to this group, send email to ats-lang-users@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
> .
>
--
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@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/CAPPSPLrMsBR9XXHUtW9JmSRuA4kKCdcXEcx0cAwb3WtiDkHoKw%40mail.gmail.com.
