{-
  Pseudo "Categorical programmming" using Haskell. :-P

  References:
    Tatsuya Hagino. "A Categorical Programming Language"
    Ph.D thesis, University of Edinburgh, 1987.
-}


pt :: x -> (Pt x)
pt x () = x

from_pt :: (Pt x)->x
from_pt m = m ()

true  = pt True
false = pt False


---- terminal object

type Pt x = ()->x

bang :: x -> ()
bang _ = ()


---- product

type Prod a b = (a,b)

prod :: (a->b, c->d) -> (Prod a c) -> (Prod b d)
prod(f,g) = pair(f.pi1, g.pi2)

pair :: (x->a, x->b) -> (x->(Prod a b))
pair(a,b) = \x -> (a x, b x)

pi1 :: (Prod a b) -> a
pi1(a,b) = a

pi2 :: (Prod a b) -> b
pi2(a,b) = b


---- coproduct

data CoProd a b = In1 a | In2 b  deriving (Show, Read)

coprod :: (a->b, c->d) -> ((CoProd a c) -> (CoProd b d))
coprod(f,g) = my_case(in1.f, in2.g)

my_case :: (a->x, b->x) -> ((CoProd a b) -> x)
my_case(a,b) = let
                f (In1 x) = a x
                f (In2 x) = b x
              in f

in1 :: a -> (CoProd a b)
in1 a = In1 a

in2 :: b -> (CoProd a b)
in2 a = In2 a


---- exponential

newtype Exp a b = MakeExp (a->b)

my_curry :: ((Prod t a)->b) -> (t->(Exp a b))
my_curry f = \t -> MakeExp(\a -> f (t,a))

ev :: (Prod (Exp a b) a) -> b
ev(MakeExp f, x) = f x


---- naturail number

data Nat = Zero | Succ Nat deriving (Show, Read)
zero = pt Zero
s n = Succ n

pr :: (()->x, x->x) -> (Nat -> x)
pr(a,h) = let
            f Zero     = a ()
            f (Succ n) = h (f n)
          in f

{-
pr' :: (()->x, x->x) -> (Nat -> x)
pr' (a,h) = \n ->
  let
    g c r = if n==c then r
            else g (s c) (h r)
  in g Zero (a ())
-}


---- list

prl :: (()->b, (Prod a b)->b) -> ([a] -> b)
prl(a,h) = let
             f []        = a ()
             f (car:cdr) = h (car, (f cdr))
           in f

cons (car,cdr) = car:cdr
nil = pt []


-- inifinite list

type InfList a = [a] --- XXX

fold :: (a->b, a->a) -> (a->(InfList b))
fold(h,t) = f where f a = (h a) : f (t a)

my_head :: (InfList a) -> a
my_head (h:_) = h

my_tail :: (InfList a) -> (InfList a)
my_tail (_:t) = t


---- examples

my_add = ev.pair(pr(my_curry(pi2), my_curry(s.ev)).pi1, pi2)
my_mul = ev.prod(pr(my_curry(zero.bang), my_curry(my_add.pair(ev, pi2))), id)
fact = pi1.pr(pair(s.zero, zero), pair(my_mul.pair(s.pi2, pi1), s.pi2))

test_fact = from_pt(putStr.show.fact.s.s.s.s.s.s.zero)


my_append = ev.prod(prl(my_curry(pi2),
                        my_curry(cons.pair(pi1.pi1, ev.pair(pi2.pi1, pi2)))),
                    id)
my_reverse = prl(nil, my_append.pair(pi2, cons.pair(pi1, nil.bang)))
hd  = prl(in2, in1.pi1)
hdp = my_case(hd, in2)
tl  = my_case(in1.pi2, in2) . prl(in2, in1.pair(pi1, my_case(cons, nil).pi2))
tlp = my_case(tl, in2)
my_seq = pi2.pr(pair(zero,nil), pair(s.pi1, cons))
is_empty = prl(true, false.bang)

test_seq = from_pt(my_seq.s.s.s.zero)


incseq = fold(id,s).zero
alt    = fold(my_head.pi1, pair(pi2, tail.pi1))
infseq = fold(id,id).zero
sumseq = fold(pi2, pair(my_tail.pi1, my_add.pair(my_head.pi1, pi2))).pair(my_tail, my_head)
nth    = my_head.ev.prod(pr(my_curry(pi2), my_curry(my_tail.ev)), id)

test_incseq = from_pt(my_head.my_tail.my_tail.alt.pair(incseq,infseq))
test_alt    = from_pt(my_head.my_tail.my_tail.alt.pair(incseq,infseq))
test_sumseq = from_pt(my_head.my_tail.my_tail.sumseq.incseq)
test_nth    = from_pt(nth.pair(s.s.s.s.s.zero, sumseq.incseq))