Re: Difficulties getting equality working with higher-kinded types
Great, thanks for the reply! I'll have a look at updating it soon. -- 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/641eb202-abf3-4cb1-979c-fd0c8f1e3b23%40googlegroups.com.
Re: Difficulties getting equality working with higher-kinded types
Forgot to paste the code for 'eq' that I used:
implement
{a}{b}
eq_either_either (x, y) =
case+ (x, y) of
| (right (_), left (_)) => false
| (left (_), right (_)) => false
| (left (x), left (y)) => gequal_val_val(x, y)
| (right (x), right (y)) => gequal_val_val(x, y)
On Monday, February 12, 2018 at 12:07:33 AM UTC-5, gmhwxi wrote:
>
> There are several issues here.
>
> First, eq and neq should be function templates (rather than polymorphic
> functions):
>
> datatype either(a: t@ype, b: t@ype+) =
> | left of a
> | right of b
>
> fun
> {a:t@ype}
> {b:t@ype}
> eq_either_either(x : either(a, INV(b)), y : either(a, b)) : bool
>
> fun
> {a:t@ype}
> {b:t@ype}
> neq_either_either(x : either(a, INV(b)), y : either(a, b)) : bool
>
> overload = with eq_either_either
>
> overload != with neq_either_either
>
>
> Since the second argument of 'either' is declared to be co-variant, INV(b)
> is used in the interface for eq and neq
> to make overloading of = and != work.
>
> The function of test_eq1 needs to be modified slightly:
>
>
> fn test_eq1() : bool =
> let
> val rhs = right{string,string}("eq")
> val lhs = right{string,string}("eq")
> in
> rhs = lhs
> end
>
> If you write rhs:either(string, string) = right("eq"), then the
> typechecker only knows that the type assigned to rhs is either(string, X)
> for some X <= string.
>
> Now your code can be compiled to an executable. I saw the following when
> trying it:
>
> monad_join:
> succeeded: eq (1/2)
> succeeded: eq (2/2)
>
> Test suite complete (2/2)
>
> A more serious issue with your code is the following one:
>
> assume monad_type(b : t0p) = [a:t0p] either(a, b)
>
> This is unlikely to work. I think what you need is monad(a, b) where 'a'
> serves
> as a parameter:
>
> abstype monad_type(a: t@ype, b:t@ype)
> assume monad_type(a:t0p, b:t0p) = either(a, b)
>
> On Sunday, February 11, 2018 at 8:27:15 PM UTC-5
>
>> Hi all,
>>
>> I have been trying to implement something like Haskell's Data.Either
>> module in ATS. I'd like to be able to test equality generically. This is my
>> .sats file:
>>
>> #include "share/atspre_staload_libats_ML.hats"
>> #include "libats/ML/SATS/SHARE/monad.hats"
>>
>> datatype either(a: t@ype, b: t@ype+) =
>> | left of a
>> | right of b
>>
>> fun eq_either_either {a:t@ype}{b:t@ype+} (x : either(a, b), y : either(a,
>> b)) : bool
>>
>> fun neq_either_either {a:t@ype}{b:t@ype+} (x : either(a, b), y : either(a
>> , b)) : bool
>>
>> overload = with eq_either_either
>>
>> overload != with neq_either_either
>>
>> fun lefts {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
>> [ m : int | m <= n ] list(a, m)
>>
>> fun rights {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
>> [ m : int | m <= n ] list(b, m)
>>
>> fun either_ {a:t@ype}{b:t@ype+}{c:t@ype} (f : a -> c, g : b -> c, x :
>> either(a, b)) : c
>>
>> fun is_left {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
>>
>> fun is_right {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
>>
>> fun from_right {a:t@ype}{b:t@ype+} (x : b, y : either(a, b)) : b
>>
>> fun from_left {a:t@ype}{b:t@ype+} (x : a, y : either(a, b)) : a
>>
>>
>> and this is my .dats file:
>>
>> staload "either.sats"
>> staload "prelude/SATS/list.sats"
>>
>> #include "prelude/DATS/basics.dats"
>> #include "prelude/DATS/list.dats"
>>
>> assume monad_type(b : t0p) = [a:t0p] either(a, b)
>>
>> implement eq_either_either (x, y) =
>> case+ (x, y) of
>> | (right (_), left (_)) => false
>> | (left (_), right (_)) => false
>> | (left (x), left (y)) => gequal_val_val(x, y)
>> | (right (x), right (y)) => gequal_val_val(x, y)
>>
>> implement neq_either_either (x, y) =
>> not(eq_either_either(x, y))
>>
>> datasort list =
>> | NIL
>> | CONS of list
>>
>> dataprop LENGTH(list, int) =
>> | L_NIL(NIL, 0)
>> | {l:list}{len:nat} L_CONS(CONS(l), 1 + len) of (LENGTH(l, len))
>>
>> implement lefts (ys) =
>> case- ys of
>> | list_nil() => list_nil()
>> | list_cons (right (x), xs) => lefts(xs)
>>
>> // | list_cons (left (x), xs) => list_cons(x, lefts(xs))
>> // functorial proof functions?
>> // want to prove: if length(f(xs)) <= n, length(xs) = n, length(cons(x,
>> xs)) <= length(cons(x, f(xs)))
>> implement {a} monad_return (x) =
>> right(x)
>>
>> implement {a} monad_join (x) =
>> case+ x of
>> | left (y) => left(y)
>> | right (left (y)) => left(y)
>> | right (right (x)) => right(x)
>>
>> implement {a}{b} monad_fmap (fopr, x) =
>> case+ x of
>> | left (y) => left(y)
>> | right (x) => right(fopr(x))
>>
>> implement {a}{b} monad_bind (x, fopr) =
>> case+ x of
>> | left (y) => left(y)
>> | right (y) => fopr(y)
>>
>>
>> my .hats file:
>>
>> staload "./either.sats"
>> staload _ = "./either.dats"
>>
>>
>> and finally the actual test suite:
>>
>> #include "share/atspre_staload.hats"
>> #include "share/atspre_staload_libats_ML.hats"
>> #include "either.hats"
>>
>> staload "prelude/SATS/tostring.sats"
>> staloa
Re: Difficulties getting equality working with higher-kinded types
There are several issues here.
First, eq and neq should be function templates (rather than polymorphic
functions):
datatype either(a: t@ype, b: t@ype+) =
| left of a
| right of b
fun
{a:t@ype}
{b:t@ype}
eq_either_either(x : either(a, INV(b)), y : either(a, b)) : bool
fun
{a:t@ype}
{b:t@ype}
neq_either_either(x : either(a, INV(b)), y : either(a, b)) : bool
overload = with eq_either_either
overload != with neq_either_either
Since the second argument of 'either' is declared to be co-variant, INV(b)
is used in the interface for eq and neq
to make overloading of = and != work.
The function of test_eq1 needs to be modified slightly:
fn test_eq1() : bool =
let
val rhs = right{string,string}("eq")
val lhs = right{string,string}("eq")
in
rhs = lhs
end
If you write rhs:either(string, string) = right("eq"), then the typechecker
only knows that the type assigned to rhs is either(string, X) for some X <=
string.
Now your code can be compiled to an executable. I saw the following when
trying it:
monad_join:
succeeded: eq (1/2)
succeeded: eq (2/2)
Test suite complete (2/2)
A more serious issue with your code is the following one:
assume monad_type(b : t0p) = [a:t0p] either(a, b)
This is unlikely to work. I think what you need is monad(a, b) where 'a'
serves
as a parameter:
abstype monad_type(a: t@ype, b:t@ype)
assume monad_type(a:t0p, b:t0p) = either(a, b)
On Sunday, February 11, 2018 at 8:27:15 PM UTC-5
> Hi all,
>
> I have been trying to implement something like Haskell's Data.Either
> module in ATS. I'd like to be able to test equality generically. This is my
> .sats file:
>
> #include "share/atspre_staload_libats_ML.hats"
> #include "libats/ML/SATS/SHARE/monad.hats"
>
> datatype either(a: t@ype, b: t@ype+) =
> | left of a
> | right of b
>
> fun eq_either_either {a:t@ype}{b:t@ype+} (x : either(a, b), y : either(a,
> b)) : bool
>
> fun neq_either_either {a:t@ype}{b:t@ype+} (x : either(a, b), y : either(a,
> b)) : bool
>
> overload = with eq_either_either
>
> overload != with neq_either_either
>
> fun lefts {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
> [ m : int | m <= n ] list(a, m)
>
> fun rights {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
> [ m : int | m <= n ] list(b, m)
>
> fun either_ {a:t@ype}{b:t@ype+}{c:t@ype} (f : a -> c, g : b -> c, x :
> either(a, b)) : c
>
> fun is_left {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
>
> fun is_right {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
>
> fun from_right {a:t@ype}{b:t@ype+} (x : b, y : either(a, b)) : b
>
> fun from_left {a:t@ype}{b:t@ype+} (x : a, y : either(a, b)) : a
>
>
> and this is my .dats file:
>
> staload "either.sats"
> staload "prelude/SATS/list.sats"
>
> #include "prelude/DATS/basics.dats"
> #include "prelude/DATS/list.dats"
>
> assume monad_type(b : t0p) = [a:t0p] either(a, b)
>
> implement eq_either_either (x, y) =
> case+ (x, y) of
> | (right (_), left (_)) => false
> | (left (_), right (_)) => false
> | (left (x), left (y)) => gequal_val_val(x, y)
> | (right (x), right (y)) => gequal_val_val(x, y)
>
> implement neq_either_either (x, y) =
> not(eq_either_either(x, y))
>
> datasort list =
> | NIL
> | CONS of list
>
> dataprop LENGTH(list, int) =
> | L_NIL(NIL, 0)
> | {l:list}{len:nat} L_CONS(CONS(l), 1 + len) of (LENGTH(l, len))
>
> implement lefts (ys) =
> case- ys of
> | list_nil() => list_nil()
> | list_cons (right (x), xs) => lefts(xs)
>
> // | list_cons (left (x), xs) => list_cons(x, lefts(xs))
> // functorial proof functions?
> // want to prove: if length(f(xs)) <= n, length(xs) = n, length(cons(x,
> xs)) <= length(cons(x, f(xs)))
> implement {a} monad_return (x) =
> right(x)
>
> implement {a} monad_join (x) =
> case+ x of
> | left (y) => left(y)
> | right (left (y)) => left(y)
> | right (right (x)) => right(x)
>
> implement {a}{b} monad_fmap (fopr, x) =
> case+ x of
> | left (y) => left(y)
> | right (x) => right(fopr(x))
>
> implement {a}{b} monad_bind (x, fopr) =
> case+ x of
> | left (y) => left(y)
> | right (y) => fopr(y)
>
>
> my .hats file:
>
> staload "./either.sats"
> staload _ = "./either.dats"
>
>
> and finally the actual test suite:
>
> #include "share/atspre_staload.hats"
> #include "share/atspre_staload_libats_ML.hats"
> #include "either.hats"
>
> staload "prelude/SATS/tostring.sats"
> staload "libats/ML/SATS/string.sats"
>
> #define nil list_vt_nil
>
> #define :: list_vt_cons
>
> fn test_eq1() : bool =
> let
> val rhs: either(string, string) = right("eq")
> val lhs: either(string, string) = right("eq")
> in
> rhs = lhs
> end
>
> fn test_eq2() : bool =
> true
>
> vtypedef named = @{ fst = string, snd = bool }
> vtypedef test_tree = @{ group = string, leaves = List_vt(named) }
>
> fn fail_incomplete(i : int, n : int) : void =
> {
> val _ = prerr!("\nTest suite complete (" + tostring_int(i) + "/" +
> tostring_int(n) + ")\n")
> val
Re: Difficulties getting equality working with higher-kinded types
Also, the full source code is here: http://github.com/vmchale/either
This might occlude some relevant bits since it uses atspkg but hopefully
not?
On Sunday, February 11, 2018 at 7:27:15 PM UTC-6, vamc...@gmail.com wrote:
>
> Hi all,
>
> I have been trying to implement something like Haskell's Data.Either
> module in ATS. I'd like to be able to test equality generically. This is my
> .sats file:
>
> #include "share/atspre_staload_libats_ML.hats"
> #include "libats/ML/SATS/SHARE/monad.hats"
>
> datatype either(a: t@ype, b: t@ype+) =
> | left of a
> | right of b
>
> fun eq_either_either {a:t@ype}{b:t@ype+} (x : either(a, b), y : either(a,
> b)) : bool
>
> fun neq_either_either {a:t@ype}{b:t@ype+} (x : either(a, b), y : either(a,
> b)) : bool
>
> overload = with eq_either_either
>
> overload != with neq_either_either
>
> fun lefts {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
> [ m : int | m <= n ] list(a, m)
>
> fun rights {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
> [ m : int | m <= n ] list(b, m)
>
> fun either_ {a:t@ype}{b:t@ype+}{c:t@ype} (f : a -> c, g : b -> c, x :
> either(a, b)) : c
>
> fun is_left {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
>
> fun is_right {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
>
> fun from_right {a:t@ype}{b:t@ype+} (x : b, y : either(a, b)) : b
>
> fun from_left {a:t@ype}{b:t@ype+} (x : a, y : either(a, b)) : a
>
>
> and this is my .dats file:
>
> staload "either.sats"
> staload "prelude/SATS/list.sats"
>
> #include "prelude/DATS/basics.dats"
> #include "prelude/DATS/list.dats"
>
> assume monad_type(b : t0p) = [a:t0p] either(a, b)
>
> implement eq_either_either (x, y) =
> case+ (x, y) of
> | (right (_), left (_)) => false
> | (left (_), right (_)) => false
> | (left (x), left (y)) => gequal_val_val(x, y)
> | (right (x), right (y)) => gequal_val_val(x, y)
>
> implement neq_either_either (x, y) =
> not(eq_either_either(x, y))
>
> datasort list =
> | NIL
> | CONS of list
>
> dataprop LENGTH(list, int) =
> | L_NIL(NIL, 0)
> | {l:list}{len:nat} L_CONS(CONS(l), 1 + len) of (LENGTH(l, len))
>
> implement lefts (ys) =
> case- ys of
> | list_nil() => list_nil()
> | list_cons (right (x), xs) => lefts(xs)
>
> // | list_cons (left (x), xs) => list_cons(x, lefts(xs))
> // functorial proof functions?
> // want to prove: if length(f(xs)) <= n, length(xs) = n, length(cons(x,
> xs)) <= length(cons(x, f(xs)))
> implement {a} monad_return (x) =
> right(x)
>
> implement {a} monad_join (x) =
> case+ x of
> | left (y) => left(y)
> | right (left (y)) => left(y)
> | right (right (x)) => right(x)
>
> implement {a}{b} monad_fmap (fopr, x) =
> case+ x of
> | left (y) => left(y)
> | right (x) => right(fopr(x))
>
> implement {a}{b} monad_bind (x, fopr) =
> case+ x of
> | left (y) => left(y)
> | right (y) => fopr(y)
>
>
> my .hats file:
>
> staload "./either.sats"
> staload _ = "./either.dats"
>
>
> and finally the actual test suite:
>
> #include "share/atspre_staload.hats"
> #include "share/atspre_staload_libats_ML.hats"
> #include "either.hats"
>
> staload "prelude/SATS/tostring.sats"
> staload "libats/ML/SATS/string.sats"
>
> #define nil list_vt_nil
>
> #define :: list_vt_cons
>
> fn test_eq1() : bool =
> let
> val rhs: either(string, string) = right("eq")
> val lhs: either(string, string) = right("eq")
> in
> rhs = lhs
> end
>
> fn test_eq2() : bool =
> true
>
> vtypedef named = @{ fst = string, snd = bool }
> vtypedef test_tree = @{ group = string, leaves = List_vt(named) }
>
> fn fail_incomplete(i : int, n : int) : void =
> {
> val _ = prerr!("\nTest suite complete (" + tostring_int(i) + "/" +
> tostring_int(n) + ")\n")
> val _ = if n != i then
> (exit(1) ; ())
> else
> ()
> }
>
> fnx iterate_list(t : test_tree, i : int, n : int) : void =
> let
> val _ = if i = 0 then
> println!(t.group + ":")
> else
> ()
>
> fun handle_loop(s : string, b : bool, xs : test_tree) : void =
> if b then
> (println!(" \33[32msucceeded:\33[0m " + s) ; iterate_list(xs, i +
> 1, n))
> else
> (println!(" \33[31mfailed:\33[0m " + s) ; iterate_list(xs, i, n))
> in
> case+ t.leaves of
> | ~list_vt_nil() => fail_incomplete(i, n)
> | ~list_vt_cons (x, xs) => handle_loop(x.fst, x.snd, @{ group = t.
> group, leaves = xs })
> end
>
> implement main0 () =
> {
> var n0 = @{ fst = "eq (1/2)", snd = test_eq1() }
> var n1 = @{ fst = "eq (2/2)", snd = test_eq2() }
> var xs = n0 :: n1 :: nil
> var total = list_vt_length(xs)
> val g = @{ group = "monad_join", leaves = xs } : test_tree
> val _ = iterate_list(g, 0, total)
> }
>
>
> which fails to build with the following error:
>
> /tmp/ccrn6Wjd.o: In function `mainats_void_0': test_dats.c:(.text+0x391):
> undefined reference to `
> _057_home_057_vanessa_057__056_atspkg_057_0_056_3_056_9_057_lib_057_ats2_055_postiats_05
