First-class phantom types in ATS

fc-phantom-types.dats

(*
** 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 [%{$]