Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
First-class phantom types in ATS
(*
** Hello, world!
** run it here: http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_fil=hello
*)
(* ****** ****** *)
//
#define
LIBATSCC2JS_targetloc
"$PATSHOME\
/contrib/libatscc2js/ATS2-0.3.2"
//
#include
"{$LIBATSCC2JS}/staloadall.hats"
//
(* ****** ****** *)
#staload
"{$LIBATSCC2JS}/SATS/print.sats"
(* ****** ****** *)
#define ATS_MAINATSFLAG 1
#define ATS_DYNLOADNAME "my_dynload"
(* ****** ****** *)
// based on: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.596.7907&rep=rep1&type=pdf
// First-Class Phantom Types
datatype Rep(t@ype) =
| RInt(int)
| RChar(char)
| {a:t@ype} RList(list0(a)) of Rep(a)
| {a,b:t@ype} RTup('(a,b)) of (Rep(a),Rep(b))
extern
fun
equal {t:t@ype} (Rep(t), t, t): bool
implement
equal {t} (r, x, y) =
case- r of
| RInt () => (x = y)
| RChar () => (x = y)
| RList (r0) => (
case+ (x, y) of
| (list0_nil (), list0_nil ()) => true
| (list0_nil (), _) => false
| (_, list0_nil ()) => false
| (list0_cons (x0, x), list0_cons (y0, y)) => equal (r0, x0, y0) andalso equal (r, x, y)
)
| RTup (r0, r1) => let
val+ '(x0, x1) = x
val+ '(y0, y1) = x
in
equal (r0, x0, y0) && equal (r1, x1, y1)
end
// unit-tests!
val () = print(equal (RInt(), 1, 2))
val () = print(equal (RList(RInt()), list0_cons(1,list0_nil()), list0_cons(1,list0_nil())))
(* ****** ****** *)
//
extern
fun
hello(): void = "mac#"
implement
hello() = print("Hello, world!")
//
(* ****** ****** *)
//
val () = hello()
//
(* ****** ****** *)
%{$
//
ats2jspre_the_print_store_clear();
my_dynload();
alert(ats2jspre_the_print_store_join());
//
%} // end of [%{$]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment