(*
Does not work with ATS 0.2.11. Try the latest version on your own machine please.
*)
#include "share/atspre_staload.hats"
datatype list (a:t@ype) =
| Nil (a) of ()
| Cons (a) of (a, list a)
datatype listn (a:t@ype, n:int) =
| NilN (a, 0)
| ConsN (a, n+1) of (a, listn(a, n))
typedef listn (a:t@ype) = [n:nat] listn (a, n)
datatype maybe (a:t@ype) =
| Nothing (a) of ()
| Just (a) of a
(* type class *)
sortdef tycon = t@ype -> type
extern fun {f:tycon} {a,b:t@ype} fmap (a -<cloref1> b): f(a) -<cloref1> f(b)
(* instance list *)
implement (a,b:t@ype) fmap<list><a,b> (f) =
lam (xs: list a): list b =>
case+ xs of
| Cons (x, xs) => Cons (f x, (fmap<list><a,b> f) xs)
| _ => Nil ()
(* instance listn *)
implement (a,b:t@ype) fmap<listn><a,b> (f) =
lam (xs: listn a): listn b =>
case+ xs of
| ConsN (x, xs) =>
let
extern praxi lengte0 {a:t@ype} {n:int} (xs: listn (a, n)): [n>=0] unit_p
prval _ = lengte0 xs
in
ConsN (f x, (fmap<listn><a,b> f) xs)
end
| _ => NilN ()
(* instance maybe *)
implement (a,b:t@ype) fmap<maybe><a,b> (f) =
lam (x: maybe a): maybe b =>
case+ x of
| Just a => Just (f a)
| Nothing () => Nothing ()
implement main0 () = let
#define :: Cons
val xs = 1 :: 2 :: 3 :: Nil() : list int
val ys = fmap<list><int,int> (lam x => x + 1) (xs)
val zs = fmap<list><int,int> (lam x => let val _ = println! x in x end) (ys)
#define :: ConsN
val xs = 1 :: 2 :: 3 :: NilN() : listn int
val ys = fmap<listn><int,int> (lam x => x + 1) (xs)
val zs = fmap<listn><int,int> (lam x => let val _ = println! x in x end) (ys)
val mx = Just 1 : maybe int
val my = fmap<maybe><int,string> (lam (x:int):string => "hello") (mx)
val mz = fmap<maybe><string,string> (lam (x:string):string => let val _ = println! x in x end) (my)
in
end
