Categorical Programming Language (Haskell version)
version 0.2.0

Type help for help

cpl> edit
| right object 1 with !
| end object;
right object 1 is defined
cpl> edit
| right object prod(a,b) with pair is
|   pi1: prod -> a
|   pi2: prod -> b
| end object;
right object prod(+,+) is defined
cpl> edit
| right object exp(a,b) with curry is
|   eval: prod(exp,a) -> b
| end object;
right object exp(-,+) is defined
cpl> edit
| left object nat with pr is
|   0: 1 -> nat
|   s: nat -> nat
| end object;
left object nat is defined
cpl> edit
| left object coprod(a,b) with case is
|   in1: a -> coprod
|   in2: b -> coprod
| end object;
left object coprod(+,+) is defined
cpl> show pair(pi2,eval)
pair(pi2,eval)
    : prod(exp(*a,*b),*a) -> prod(*a,*b)
cpl> let add=eval.prod(pr(curry(pi2), curry(s.eval)), I)
add = eval.prod(pr(curry(pi2),curry(s.eval)),I)
    : prod(nat,nat) -> nat
cpl> simp add.pair(s.s.0, s.0)
s.s.s.0
    : 1 -> nat
cpl> let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I)
mult = eval.prod(pr(curry(0.!),curry(add.pair(eval,pi2))),I)
    : prod(nat,nat) -> nat
cpl> let fact=pi1.pr(pair(s.0,0), pair(mult.pair(s.pi2,pi1), s.pi2))
fact = pi1.pr(pair(s.0,0),pair(mult.pair(s.pi2,pi1),s.pi2))
    : nat -> nat
cpl> simp fact.s.s.s.s.0
s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.0
    : 1 -> nat
cpl> edit
| left object list(p) with prl is
|   nil: 1 -> list
|   cons: prod(p,list) -> list
| end object;
left object list(+) is defined
cpl> let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I)
append = eval.prod(prl(curry(pi2),curry(cons.pair(pi1.pi1,eval.pair(pi2.pi1,pi2)))),I)
    : prod(list(*a),list(*a)) -> list(*a)
cpl> let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)))
reverse = prl(nil,append.pair(pi2,cons.pair(pi1,nil.!)))
    : list(*a) -> list(*a)
cpl> let hd = prl(in2, in1.pi1)
hd = prl(in2,in1.pi1)
    : list(*a) -> coprod(*a,1)
cpl> let hdp=case(hd,in2)
hdp = case(hd,in2)
    : coprod(list(*a),1) -> coprod(*a,1)
cpl> let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil)))
tl = coprod(pi2,I).prl(in2,in1.prod(I,case(cons,nil)))
    : list(*a) -> coprod(list(*a),1)
cpl> let tlp = case(tl, in2)
tlp = case(tl,in2)
    : coprod(list(*a),1) -> coprod(list(*a),1)
cpl> let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons))
seq = pi2.pr(pair(0,nil),pair(s.pi1,cons))
    : nat -> list(nat)
cpl> simp seq.s.s.s.0
cons.pair(s.pi1,cons).pair(s.pi1,cons).pair(0,nil)
    : 1 -> list(nat)
cpl> simp full seq.s.s.s.0
cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil)))
    : 1 -> list(nat)
cpl> simp hdp.tl.seq.s.s.s.0
in1.s.0
    : 1 -> coprod(nat,1)
cpl> simp full append.pair(seq.s.s.0, seq.s.s.s.0)
cons.pair(s.0,cons.pair(0,cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil)))))
    : 1 -> list(nat)
cpl> simp full reverse.it
cons.pair(0,cons.pair(s.0,cons.pair(s.s.0,cons.pair(0,cons.pair(s.0,nil.!)))))
    : 1 -> list(nat)
cpl> edit
| right object inflist(a) with fold is
|   head: inflist -> a
|   tail: inflist -> inflist
| end object;
right object inflist(+) is defined
cpl> let incseq=fold(I,s).0
incseq = fold(I,s).0
    : 1 -> inflist(nat)
cpl> simp head.incseq
0
    : 1 -> nat
cpl> simp head.tail.tail.tail.incseq
s.s.s.0
    : 1 -> nat
cpl> let alt=fold(head.pi1, pair(pi2, tail.pi1))
alt = fold(head.pi1,pair(pi2,tail.pi1))
    : prod(inflist(*a),inflist(*a)) -> inflist(*a)
cpl> let infseq=fold(I,I).0
infseq = fold(I,I).0
    : 1 -> inflist(nat)
cpl> simp head.tail.tail.alt.pair(incseq, infseq)
s.0
    : 1 -> nat
cpl> exit
