Functor Type Class with Slightly More Complex Instances

(*
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