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_055_0_056_3_056_9_057_either_056_sats__eq_either_either'
collect2: error: ld returned 1 exit status )
Am I doing something wrong here? I tried to get generic equality on lists
working as well, but I couldn't seem to figure out how. I tried this with
ATS 0.3.9 as well as ATS 0.3.10. Any insight would be much appreciated!
Thanks!
--
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 [email protected].
To post to this group, send email to [email protected].
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/d505fd4b-cb10-4170-a8f5-98f15497c6bc%40googlegroups.com.
