diff --git a/COPYING b/COPYING
new file mode 100644
--- /dev/null
+++ b/COPYING
@@ -0,0 +1,27 @@
+Copyright 2004-2008 Masahiro Sakai. All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+   1. Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+   2. Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+   3. The name of the author may not be used to endorse or promote
+      products derived from this software without specific prior
+      written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
+INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING
+IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
diff --git a/CPL.cabal b/CPL.cabal
new file mode 100644
--- /dev/null
+++ b/CPL.cabal
@@ -0,0 +1,32 @@
+Name:		CPL
+Version:	0.0.5
+License:	BSD3
+License-File:	COPYING
+Author:		Masahiro Sakai (masahiro.sakai@gmail.com)
+Maintainer:	masahiro.sakai@gmail.com
+Category:	Compilers/Interpreters
+Synopsis:	An interpreter of Hagino's Categorical Programming Language (CPL).
+Description:	An interpreter of Hagino's Categorical Programming Language (CPL).
+Extra-Source-Files:
+   README,
+   NEWS,
+   samples/ack.cpl,
+   samples/automata.cdt,
+   samples/ccc.cdt,
+   samples/examples.cpl,
+   samples/examples.txt,
+   samples/misc.cdt,
+   samples/obscure.cdt,
+   samples/rec.cdt,
+   samples/benchmark.cpl,
+   samples/ack_3_4.cpl,
+   samples/function.cpl,
+   src/CDT.hs-boot
+Build-Type: Simple
+
+Executable:	cpl
+Main-is:	Main.hs
+HS-Source-Dirs:	src
+Other-Modules: AExp CDT CDTParser CPLSystem Exp ExpParser FE Funct ParserUtils Simp Statement Subst Type Typing Variance 
+Build-Depends: base >=4 && <5, mtl, containers, array, parsec
+Extensions: CPP, GeneralizedNewtypeDeriving
diff --git a/NEWS b/NEWS
new file mode 100644
--- /dev/null
+++ b/NEWS
@@ -0,0 +1,17 @@
+= Changes since the 0.0.3 release
+
+Function defintions are added.
+
+Examples:
+
+  > let uncurry(f) = eval . prod(f, I)
+  uncurry(f) = eval.prod(f,I)
+  f: *a -> exp(*b,*c)
+  -----------------------------
+  uncurry(f): prod(*a,*b) -> *c
+
+  > let primrec(f,g) = pi2.pr(pair(0,f), pair(s.pi1, g))
+  primrec(f,g) = pi2.pr(pair(0,f),pair(s.pi1,g))
+  f: 1 -> *a  g: prod(nat,*a) -> *a
+  ---------------------------------
+  primrec(f,g): nat -> *a
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,60 @@
+An implementation of "A Categorical Programing Language".
+version 0.0.5
+====================
+
+  This package is an implementation of "A Categorical Programing Language"
+  (CPL for short)[1][2] written in Haskell.
+
+  CPL is a functional programming language based on category
+  theory[3]. Data types are declared in a categorical manner by
+  adjunctions. Data types that can be handled include the terminal
+  object, the initial object, the binary product functor, the binary
+  coproduct functor, the exponential functor, the natural number object,
+  the functor for finite lists, and the functor for infinite lists.
+  Each data type is declared with its basic operations or
+  morphisms. Programs consist of these morphisms, and execution of
+  programs is the reduction of elements (i.e. special morphisms) to
+  their canonical form.
+
+Requirements
+------------
+
+  * GHC-6.10
+
+Install
+-------
+
+  De-Compress archive and enter its top directory.
+  Then type:
+
+    $ runhaskell Setup.hs configure
+    $ runhaskell Setup.hs build
+    $ runhaskell Setup.hs install
+
+Usage
+-----
+
+  See chapter 5 of [1]
+
+License
+-------
+  This program is licenced under the BSD-style license.
+  (See the file 'COPYING'.)
+
+  Copyright (C) 2004-2009 Masahiro Sakai <masahiro.sakai@gmail.com>
+
+Author
+----------
+  Masahiro Sakai <masahiro.sakai@gmail.com>
+
+Bibliography
+------------
+
+[1]  Tatsuya Hagino, ``A Categorical Programming Languge''.
+     Ph.D. Thesis, University of Edinburgh, 1987
+     available at <http://www.tom.sfc.keio.ac.jp/~hagino/index.html.en>
+
+[2]  Tatsuya Hagino, ``Categorical Functional Programming Language''
+     Computer Software, Vol 7, No.1.
+     Advances in Software Science and Technology 4, 1992
+     ISBN 0-12-037104-9
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runghc
+import Distribution.Simple
+main = defaultMain
diff --git a/samples/ack.cpl b/samples/ack.cpl
new file mode 100644
--- /dev/null
+++ b/samples/ack.cpl
@@ -0,0 +1,55 @@
+
+right object 1 with ! is
+end object;
+
+right object prod(a,b) with pair is
+  pi1: prod -> a
+  pi2: prod -> b
+end object;
+
+right object exp(a,b) with curry is
+  eval: prod(exp,a) -> b
+end object;
+
+left object nat with pr is
+  0: 1 -> nat
+  s: nat -> nat
+end object;
+
+let times=eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1,eval.pair(pi2.pi1,pi2))))),I);
+let ack_0=curry(s.pi2);
+let ack_s=curry(eval.pair(times.pair(s.pi2,pi1),s.0.!));
+let ack=eval.prod(pr(ack_0,ack_s),I);
+
+#show aexp eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1,eval.pair(pi2.pi1,pi2))))),I);
+#show aexp curry(s.pi2);
+#show aexp curry(eval.pair(times.pair(s.pi2,pi1),s.0.!));
+#show aexp eval.prod(pr(ack_0,ack_s),I);
+
+simp full ack.pair(s.s.s.0,s.s.s.0);
+
+# time ~/cpl/cpl/bin/cpl.rb ack.cpl
+# cpl.rb (An implementation of Categorical Programming Language)
+# version 0.0.4
+# Type help for help
+# right object 1 defined
+# right object prod(+,+) defined
+# right object exp(-,+) defined
+# left object nat defined
+# times : prod(nat,exp(*a,*a)) -> exp(*a,*a)  defined
+# ack_0 : *a -> exp(nat,nat)  defined
+# ack_s : exp(nat,nat) -> exp(nat,nat)  defined
+# ack : prod(nat,nat) -> nat  defined
+# s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.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.!
+#     : *a -> nat
+# 
+# real	21m17.567s
+# user	20m43.233s
+# sys	0m0.296s
+
+
+# HaskellӁ
+# real	0m9.230s
+# user	0m0.031s
+# sys	0m0.000s
+
diff --git a/samples/ack_3_4.cpl b/samples/ack_3_4.cpl
new file mode 100644
--- /dev/null
+++ b/samples/ack_3_4.cpl
@@ -0,0 +1,23 @@
+right object 1 with ! is
+end object;
+
+right object prod(a,b) with pair is
+  pi1: prod -> a
+  pi2: prod -> b
+end object;
+
+right object exp(a,b) with curry is
+  eval: prod(exp,a) -> b
+end object;
+
+left object nat with pr is
+  0: 1 -> nat
+  s: nat -> nat
+end object;
+
+let times=eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1,eval.pair(pi2.pi1,pi2))))),I);
+let ack_0=curry(s.pi2);
+let ack_s=curry(eval.pair(times.pair(s.pi2,pi1),s.0.!));
+let ack=eval.prod(pr(ack_0,ack_s),I);
+
+simp full ack.pair(s.s.s.0, s.s.s.s.0);
diff --git a/samples/automata.cdt b/samples/automata.cdt
new file mode 100644
--- /dev/null
+++ b/samples/automata.cdt
@@ -0,0 +1,12 @@
+# categorical data type of automata
+
+# Moore automata
+right object dyn'(I,O) with univ' is
+  next': prod(dyn',I) -> dyn'
+  output': dyn' -> O
+end object;
+
+# Mealy automata
+right object dyn''(I,O) with univ'' is
+  next'': prod(dyn'',I) -> prod(dyn'',O)
+end object;
diff --git a/samples/benchmark.cpl b/samples/benchmark.cpl
new file mode 100644
--- /dev/null
+++ b/samples/benchmark.cpl
@@ -0,0 +1,36 @@
+right object 1 with ! is
+end object;
+
+right object prod(a,b) with pair is
+  pi1: prod -> a
+  pi2: prod -> b
+end object;
+
+right object exp(a,b) with curry is
+  eval: prod(exp,a) -> b
+end object;
+
+left object nat with pr is
+  0: 1 -> nat
+  s: nat -> nat
+end object;
+
+let times=eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1,eval.pair(pi2.pi1,pi2))))),I);
+let ack_0=curry(s.pi2);
+let ack_s=curry(eval.pair(times.pair(s.pi2,pi1),s.0.!));
+let ack=eval.prod(pr(ack_0,ack_s),I);
+
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+simp full ack.pair(s.s.s.0,s.s.s.0);
+
+# src/cpl.exe samples/test.cpl  0.00s user 0.03s system 0% cpu 5.864 total
+
+# src/cpl.exe samples/test.cpl  0.00s user 0.00s system 0% cpu 5.348 total
diff --git a/samples/ccc.cdt b/samples/ccc.cdt
new file mode 100644
--- /dev/null
+++ b/samples/ccc.cdt
@@ -0,0 +1,17 @@
+# Cartesian Closed Category
+
+# terminal object
+right object 1 with !
+end object;
+
+# product functor 
+right object prod(X,Y) with pair is
+  pi1: prod -> X
+  pi2: prod -> Y
+end object;
+
+# exponential functor
+right object exp(X,Y) with curry is
+  eval: prod(exp,X) -> Y
+end object;
+
diff --git a/samples/examples.cpl b/samples/examples.cpl
new file mode 100644
--- /dev/null
+++ b/samples/examples.cpl
@@ -0,0 +1,81 @@
+right object 1 with !
+end object;
+
+right object prod(a,b) with pair is
+  pi1: prod -> a
+  pi2: prod -> b
+end object;
+
+right object exp(a,b) with curry is
+  eval: prod(exp,a) -> b
+end object;
+
+left object nat with pr is
+  0: 1 -> nat
+  s: nat -> nat
+end object;
+
+left object coprod(a,b) with case is
+  in1: a -> coprod
+  in2: b -> coprod
+end object;
+
+show pair(pi2,eval);
+
+let add=eval.prod(pr(curry(pi2), curry(s.eval)), I);
+
+simp add.pair(s.s.0, s.0);
+
+let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I);
+
+let fact=pi1.pr(pair(s.0,0), pair(mult.pair(s.pi2,pi1), s.pi2));
+
+simp fact.s.s.s.s.0;
+
+left object list(p) with prl is
+  nil: 1 -> list
+  cons: prod(p,list) -> list
+end object;
+
+let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I);
+
+let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)));
+
+let hd = prl(in2, in1.pi1);
+
+let hdp=case(hd,in2);
+
+let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil)));
+
+let tlp = case(tl, in2);
+
+let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons));
+
+simp seq.s.s.s.0;
+
+simp full seq.s.s.s.0;
+
+simp hdp.tl.seq.s.s.s.0;
+
+simp full append.pair(seq.s.s.0, seq.s.s.s.0);
+
+simp full reverse.it;
+
+right object inflist(a) with fold is
+  head: inflist -> a
+  tail: inflist -> inflist
+end object;
+
+let incseq=fold(I,s).0;
+
+simp head.incseq;
+
+simp head.tail.tail.tail.incseq;
+
+let alt=fold(head.pi1, pair(pi2, tail.pi1));
+
+let infseq=fold(I,I).0;
+
+simp head.tail.tail.alt.pair(incseq, infseq);
+
+#exit;
diff --git a/samples/examples.txt b/samples/examples.txt
new file mode 100644
--- /dev/null
+++ b/samples/examples.txt
@@ -0,0 +1,102 @@
+% cpl.rb 
+cpl.rb (An Implementation of Categorical Programming Language)
+version 0.0.1
+cpl> edit
+| right object 1 with !
+| end object;
+right object 1 defined
+cpl> edit
+| right object prod(a,b) with pair is
+|   pi1: prod -> a
+|   pi2: prod -> b
+| end object;
+right object prod(+,+) defined
+cpl> edit
+| right object exp(a,b) with curry is
+|   eval: prod(exp,a) -> b
+| end object;
+right object exp(-,+) defined
+cpl> edit
+| left object nat with pr is
+|   0: 1 -> nat
+|   s: nat -> nat
+| end object;
+left object nat defined
+cpl> edit
+| left object coprod(a,b) with case is
+|   in1: a -> coprod
+|   in2: b -> coprod
+| end object;
+left object coprod(+,+) 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 : prod(nat,nat) -> nat  defined
+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 : prod(nat,nat) -> nat
+cpl> let fact=pi1.pr(pair(s.0,0), pair(mult.pair(s.pi2,pi1), s.pi2))
+fact : nat -> nat  defined
+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(+) defined
+cpl> let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I)
+append : prod(list(*a),list(*a)) -> list(*a)  defined
+cpl> let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)))
+reverse : list(*a) -> list(*a)  defined
+cpl> let hd = prl(in2, in1.pi1)
+hd : list(*a) -> coprod(*a,1)  defined
+cpl> let hdp=case(hd,in2)
+hdp : coprod(list(*a),1) -> coprod(*a,1)  defined
+cpl> let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil)))
+tl : list(*a) -> coprod(list(*a),1)  defined
+cpl> let tlp = case(tl, in2)
+tlp : coprod(list(*a),1) -> coprod(list(*a),1)  defined
+cpl> let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons))
+seq : nat -> list(nat)  defined
+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,*a)
+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(+) defined
+cpl> let incseq=fold(I,s).0
+incseq : 1 -> inflist(nat)  defined
+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 : prod(inflist(*a),inflist(*a)) -> inflist(*a)  defined
+cpl> let infseq=fold(I,I).0
+infseq : 1 -> inflist(nat)  defined
+cpl> simp head.tail.tail.alt.pair(incseq, infseq)
+s.0
+    : 1 -> nat
+cpl> exit
diff --git a/samples/function.cpl b/samples/function.cpl
new file mode 100644
--- /dev/null
+++ b/samples/function.cpl
@@ -0,0 +1,84 @@
+right object 1 with !
+end object;
+
+right object prod(a,b) with pair is
+  pi1: prod -> a
+  pi2: prod -> b
+end object;
+
+right object exp(a,b) with curry is
+  eval: prod(exp,a) -> b
+end object;
+
+let uncurry(f) = eval . prod(f, I);
+
+left object nat with pr is
+  0: 1 -> nat
+  s: nat -> nat
+end object;
+
+left object coprod(a,b) with case is
+  in1: a -> coprod
+  in2: b -> coprod
+end object;
+
+show pair(pi2,eval);
+
+let add=eval.prod(pr(curry(pi2), curry(s.eval)), I);
+
+simp add.pair(s.s.0, s.0);
+
+let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I);
+
+let primrec(f,g) = pi2.pr(pair(0,f), pair(s.pi1, g));
+let fact = primrec(s.0, mult.prod(s,I));
+
+simp fact.s.s.s.s.0;
+
+left object list(p) with prl is
+  nil: 1 -> list
+  cons: prod(p,list) -> list
+end object;
+
+let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I);
+
+let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)));
+
+let hd = prl(in2, in1.pi1);
+
+let hdp=case(hd,in2);
+
+let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil)));
+
+let tlp = case(tl, in2);
+
+let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons));
+
+simp seq.s.s.s.0;
+
+simp full seq.s.s.s.0;
+
+simp hdp.tl.seq.s.s.s.0;
+
+simp full append.pair(seq.s.s.0, seq.s.s.s.0);
+
+simp full reverse.it;
+
+right object inflist(a) with fold is
+  head: inflist -> a
+  tail: inflist -> inflist
+end object;
+
+let incseq=fold(I,s).0;
+
+simp head.incseq;
+
+simp head.tail.tail.tail.incseq;
+
+let alt=fold(head.pi1, pair(pi2, tail.pi1));
+
+let infseq=fold(I,I).0;
+
+simp head.tail.tail.alt.pair(incseq, infseq);
+
+#exit;
diff --git a/samples/misc.cdt b/samples/misc.cdt
new file mode 100644
--- /dev/null
+++ b/samples/misc.cdt
@@ -0,0 +1,28 @@
+# initial object
+left object 0 with !! is
+end object;
+
+# coproduct functor
+left object coprod(X,Y) with case is
+  in1: X -> coprod
+  in2: Y -> coprod
+end object;
+
+# co-"natural number object"
+right object conat with copr is
+  pred: conat -> coprod(1,conat)
+end object;
+
+right object colist(X) with coprl is
+  delist: colist -> coprod(1,prod(X,colist))
+end object;
+
+# let list2colist = coprl(prl(in1, in2.prod(I, case(nil, cons))));
+# let inflist2colist = coprl(in2.pair(head,tail));
+# let colist-length = copr(coprod(I, pi2).delist);
+
+# ordinals
+left object ord with pro is
+  ozero: 1 -> ord
+  sup: exp(nat, ord) -> ord
+end object;
diff --git a/samples/obscure.cdt b/samples/obscure.cdt
new file mode 100644
--- /dev/null
+++ b/samples/obscure.cdt
@@ -0,0 +1,12 @@
+# Examples of obscure categorical data type
+# which are not computable in the sense of CPL.
+
+# the left adjoint functor of the list functor
+left object ladjlist(X) with psi is
+  a: X -> list(ladjlist)
+end object;
+
+# the right adjoint functor of the list functor
+right object radjlist(X) with psi' is
+  a': list(radjlist) -> X
+end object;
diff --git a/samples/rec.cdt b/samples/rec.cdt
new file mode 100644
--- /dev/null
+++ b/samples/rec.cdt
@@ -0,0 +1,19 @@
+# Some of the recursively defined object
+
+# natural number object
+left object nat with pr is
+   0: 1 -> nat
+   s: nat -> nat
+end object;
+
+# list
+left object list(X) with prl is
+  nil:  1 -> list
+  cons: prod(X,list) -> list
+end object;
+
+# infinite list (a.k.a stream)
+right object inflist(X) with fold is
+  head: inflist -> X
+  tail: inflist -> inflist
+end object;
diff --git a/src/AExp.hs b/src/AExp.hs
new file mode 100644
--- /dev/null
+++ b/src/AExp.hs
@@ -0,0 +1,157 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  AExp
+-- Copyright   :  (c) Masahiro Sakai 2004,2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- Annotated Expression.
+--
+-----------------------------------------------------------------------------
+
+module AExp
+  ( AExp(..)
+  , aexpType
+  , isElement
+
+  , TypeScheme
+  , AExpScheme
+  , quantify
+
+  , skelton
+  ) where
+
+import Variance
+import Funct
+import qualified FE
+import qualified CDT
+import Type (GenType(..), Type)
+import Subst
+import qualified Exp as E
+import Exp (Id)
+
+import Data.List (nub, intercalate)
+
+----------------------------------------------------------------------------
+
+-- Annotated expression with type information
+data AExp
+  = Identity FE.FE
+  | Comp AExp AExp
+  | Nat !CDT.Nat [FE.FE]
+  | Fact !CDT.CDT [AExp] [FE.FE]
+  | Funct !CDT.CDT [AExp]
+  | Var !Id [FE.FE] [AExp] Type
+
+instance FEs AExp where
+  apply s (Identity annotation) = Identity (apply s annotation)
+  apply s (Comp a b)            = Comp (apply s a) (apply s b)
+  apply s (Nat sym annotation)  = Nat sym (apply s annotation)
+  apply s (Fact obj args annotations) =
+      Fact obj (apply s args) (apply s annotations)
+  apply s (Funct obj args) =
+      Funct obj (apply s args)
+  apply s (Var v annotations args typ) =
+      Var v (apply s annotations) (apply s args) (apply s typ)
+  tv (Identity x)          = tv x
+  tv (Comp a b)            = nub (tv a ++ tv b)
+  tv (Nat _ annotations)   = tv annotations
+  tv (Fact _ args _)       = tv args
+  tv (Funct _ args)        = tv args
+  tv (Var _ annotations args _) = nub (tv annotations ++ tv args)
+
+instance Show AExp where
+  show (Identity fe) = "I" ++ showAnnotations [fe]
+  show (Comp a b) = show a ++ "." ++ show b
+  show (Nat sym annotations) =
+      CDT.natName sym ++ showAnnotations annotations
+  show (Fact obj args annotations) =
+      CDT.factName obj ++ showAnnotations annotations ++ showAExpArgs args
+  show (Funct obj args) =
+      CDT.factName obj ++ showAExpArgs args
+  show (Var v annotations args _) = v ++ showAnnotations annotations ++ showAExpArgs args
+
+showAnnotations :: [FE.FE] -> String
+showAnnotations [] = ""
+showAnnotations xs = "[" ++ intercalate "," (map show xs) ++ "]"
+
+showAExpArgs :: [AExp] -> String
+showAExpArgs [] = ""
+showAExpArgs xs = "(" ++ intercalate "," (map show xs) ++ ")"
+
+skelton :: AExp -> E.Exp
+skelton = f
+  where
+    f (Identity _) = E.Identity
+    f (Comp a b) = f a `E.Comp` f b
+    f (Nat sym _) = E.Nat sym
+    f (Fact sym args _) = E.Fact sym (map f args)
+    f (Funct sym args) = E.Funct sym (map f args)
+    f (Var name _ args _) = E.Var name (map f args)
+
+-- XXX
+aexpType :: AExp -> Type
+aexpType = f
+  where 
+    f (Identity a) = a :-> a
+    f (Comp g h) = dom (f h) :-> cod (f g)
+    f (Nat nat annotation) =
+      apply (zip [0..] annotation) (CDT.natType nat)
+    f (Fact obj _ annotation) =
+      apply (zip [0..] annotation) (CDT.factDestType obj)
+    f (Funct obj args) = FE.Ap obj xs :-> FE.Ap obj ys
+      where
+        (xs,ys) = foldr phi ([],[]) (zip (variance obj) (map aexpType args))
+        phi (v, (x:->y)) (xs,ys) =
+          case v of
+            Contravariance -> (y:xs, x:ys)
+            _ -> (x:xs, y:ys)
+    f (Var _ _ args typ) = typ -- FIXME?
+
+isElement :: AExp -> Bool
+isElement x =
+  case dom (AExp.aexpType x) of
+    FE.Var _ -> True
+    FE.Ap obj _ -> CDT.isTerminalObject obj
+
+----------------------------------------------------------------------------
+
+-- data Scheme t = Forall !Int t
+type Scheme t = (Int, t)
+type TypeScheme = Scheme Type
+type AExpScheme = Scheme AExp
+
+quantify :: FEs t => t -> Scheme t
+quantify x = (length vars, apply s x)
+  where
+    vars = tv x
+    s = zip vars [FE.Var i | i<-[0..]]
+
+----------------------------------------------------------------------------
+
+simp :: AExp -> AExp
+simp (Comp a b) =
+  case (simp a, simp b) of
+    (Identity _, b') -> b'
+    (a', Identity _) -> a'
+    (a', b') -> Comp a' b'
+simp orig@(Fact obj args _) =
+  if a==b && all f (zip (CDT.nats obj) (map simp args))
+    then Identity a
+    else orig
+  where
+    (a :-> b) = aexpType orig
+    f (nat, Nat sym _) = nat==sym
+    f _ = False
+simp orig@(Funct _ args) =
+  if a==b && all f (map simp args)
+    then Identity a
+    else orig
+  where
+    (a :-> b) = aexpType orig
+    f (Identity _) = True
+    f _ = False
+simp x = x
diff --git a/src/CDT.hs b/src/CDT.hs
new file mode 100644
--- /dev/null
+++ b/src/CDT.hs
@@ -0,0 +1,274 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  CDT
+-- Copyright   :  (c) Masahiro Sakai 2004,2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- Categorical Data Type
+--
+-----------------------------------------------------------------------------
+
+module CDT
+  ( ObjectType (..)
+  , CDT
+  , mkCDT
+  , objectType
+  , nats
+  , nNats
+  , isUnconditioned
+
+  , functName
+  , functVariance
+  , functArity
+
+  , Nat
+  , natName
+  , natNTypeParams
+  , natType
+  , natCDT
+  , natIndex
+  , natDeclType
+  , natDeclDom
+  , natDeclCod
+  {- for optimization -}
+  , natProjectionSequence
+  , natIsUnconditioned
+
+  , factName
+  , factParams
+  , factDestType
+  , factNTypeParams
+
+  , _eqCDT -- XXX
+
+  , isComputable
+  , isProductiveIn
+  , showFunctNameWithVariance
+
+  , isTerminalObject
+  ) where
+
+import Variance
+import Funct
+import FE
+import Type
+import Subst (tv, apply)
+
+import Data.List (findIndices, transpose, find, findIndex, intercalate)
+
+
+data ObjectType
+  = LeftObject
+  | RightObject
+  deriving (Show, Read, Eq)
+
+data CDT
+  = CDT
+  { objectType      :: !ObjectType
+  , nats            :: ![Nat]
+  , nNats           :: !Int -- = length of nats
+  , isUnconditioned :: !Bool
+
+  , functName       :: !String
+  , functVariance   :: ![Variance]
+  , functArity      :: !Int -- = length of functVariance
+
+  , factName        :: !String
+  , factParams      :: ![Type]
+  , factDestType    :: Type -- $B%k!<%W$rHr$1$k$?$a$K@53J%U%i%0$rIU$1$J$$(B
+  }
+
+instance Funct CDT where
+  variance CDT{ functVariance = vs } = vs
+
+instance Eq CDT where
+  a==b = objectType a == objectType b &&
+         nNats a      == nNats b &&
+         functName a  == functName b &&
+         functArity a == functArity b &&
+         all (\(n1,n2) -> natName n1 == natName n2 &&
+                          natDeclType n1 == natDeclType n2)
+             (zip (nats a) (nats b))
+
+_eqCDT :: CDT -> CDT -> Bool
+_eqCDT a b = a==b
+
+data Nat
+  = Nat
+  { natName     :: !String
+  , natType     :: !Type
+  , natCDT      :: !CDT
+  , natIndex    :: !Int
+  , natDeclType :: !Type
+
+  {- for optimization -}
+
+  -- right object $B$G$7$+0UL#$,L5$$$N$G(B!$B$rIU$1$J$$(B
+  , natProjectionSequence :: [Int]
+
+  , natIsUnconditioned :: !Bool
+    {- LeftObject$B$J$i(BnatDecl$B$N(Bdom$B$K!"(B
+     - RightObject$B$J$i(BnatDecl$B$N(Bcod$B$K(B
+     - $B$=$N%*%V%8%'%/%H(B(Var 0)$B$,8=$o$l$F$$$J$$>l9g$K??!#(B
+     -}
+  }
+
+instance Eq Nat where
+  a==b = natCDT a == natCDT b && natIndex a == natIndex b
+
+{-# INLINE natNTypeParams #-}
+natNTypeParams :: Nat -> Int
+natNTypeParams = functArity . natCDT
+
+{-# INLINE natDeclDom #-}
+natDeclDom :: Nat -> FE
+natDeclDom = dom . natDeclType
+
+{-# INLINE natDeclCod #-}
+natDeclCod :: Nat -> FE
+natDeclCod = cod . natDeclType
+
+{-# INLINE factNTypeParams #-}
+factNTypeParams :: CDT -> Int
+factNTypeParams factObj = functArity factObj + 1
+
+
+mkCDT :: ObjectType -> String -> Int -> String -> [(String,Type)] -> CDT
+mkCDT t functName functArity factName natDecls = object
+  where
+    object =
+      CDT
+      { objectType      = t
+      , nats            = nats
+      , nNats           = length (natDecls)
+      , isUnconditioned = isUnconditioned
+
+      , functName       = functName
+      , functVariance   = vs
+      , functArity      = functArity
+
+      , factName     = factName
+      , factParams   = map snd natDecls
+      , factDestType = factDestType
+      }
+
+    vs = map joinL . transpose . map f $ natDecls
+      where
+        f (_,dom:->cod) =
+          zipWith g (tail (variance (CFE (1+functArity) dom)))
+                    (tail (variance (CFE (1+functArity) cod)))
+        g = case t of
+              LeftObject  ->
+                \a b -> a `join` (Contravariance `mult` b)
+              RightObject ->
+                \a b -> (Contravariance `mult` a) `join` b
+
+    factDestType =
+      case t of
+        LeftObject  -> a :-> b
+        RightObject -> b :-> a
+      where a = Ap object [Var x | x <- [1..functArity]]
+            b = Var 0
+
+    nats = zipWith f natDecls [0..]
+      where
+        f (name, declType@(dom :-> cod)) idx = nat
+          where
+            nat = Nat{ natName     = name
+                     , natType     = apply s declType
+                     , natCDT      = object
+                     , natIndex    = idx
+                     , natDeclType = declType
+                     , natProjectionSequence =
+                         case t of
+                           LeftObject -> error "not a right object"
+                           RightObject -> makeProjectionSequence dom
+                     , natIsUnconditioned =
+                         case t of
+                           LeftObject  -> not (0 `elem` tv dom)
+                           RightObject -> not (0 `elem` tv cod)
+                     }
+            s = [(x, h x) | x <- [0..functArity]]
+              where
+                h 0 = Ap object [Var x | x <- [0..(functArity-1)]]
+                h n = Var (n-1)
+
+    isUnconditioned = all f natDecls
+      where
+        f (_, dom :-> cod) =
+          case t of
+            LeftObject  -> 0 `notElem` tv dom
+            RightObject -> 0 `notElem` tv cod
+
+----------------------------------------------------------------------------
+
+isComputable :: CDT -> Bool
+isComputable obj =
+  case objectType obj of
+    LeftObject -> all f (nats obj)
+      where
+        f nat = case natDeclCod nat of
+                  Var 0 -> True
+                  _     -> False
+    RightObject -> all f (nats obj)
+      where
+        f nat = feIsProductiveIn (natDeclDom nat) 0
+
+isProductiveIn :: CDT -> Int -> Bool
+isProductiveIn obj i =
+  objectType obj == RightObject &&
+  isUnconditioned obj &&
+  all (\(dom :-> _) -> i+1 `notElem` tv dom) natDecls &&
+  case filter (\(_ :-> cod) -> i+1 `elem` tv cod) natDecls of
+    [Var 0 :-> cod] -> feIsProductiveIn cod (i+1)
+    _ -> False
+  where natDecls = map natDeclType (nats obj)
+
+feIsProductiveIn :: FE -> Int -> Bool
+feIsProductiveIn (Var m) n = m==n
+feIsProductiveIn (Ap functObj args) n =
+  case findIndices (\arg -> n `elem` tv arg) args of
+    [i] -> isProductiveIn functObj i
+    _   -> False
+
+----------------------------------------------------------------------------
+
+makeProjectionSequence :: FE -> [Int]
+makeProjectionSequence fe = 
+  case fe of
+    FE.Var 0 -> []
+    FE.Var _ ->
+      error "BUG: not a natural transformation of a computable right object"
+    FE.Ap functObj args ->
+      case findIndex (\arg -> 0 `elem` tv arg) args of
+        Just i -> getProjection functObj i
+        _      -> error "BUG"
+
+getProjection :: CDT -> Int -> [Int]
+getProjection obj i =
+  case find f (nats obj) of
+    Just nat -> natIndex nat : makeProjectionSequence (natDeclDom nat)
+    _        -> error "BUG"
+  where
+    f nat = i+1 `elem` tv (natDeclCod nat) && 
+            case natDeclDom nat of
+              FE.Var 0 -> True
+              _        -> False
+
+----------------------------------------------------------------------------
+
+showFunctNameWithVariance :: CDT -> String
+showFunctNameWithVariance funct =
+  functName funct ++
+    case variance funct of
+      [] -> ""
+      vs -> "(" ++ intercalate "," (map Variance.mnemonic vs) ++ ")"
+
+----------------------------------------------------------------------------
+
+isTerminalObject :: CDT -> Bool
+isTerminalObject obj = objectType obj == RightObject && null (nats obj)
diff --git a/src/CDT.hs-boot b/src/CDT.hs-boot
new file mode 100644
--- /dev/null
+++ b/src/CDT.hs-boot
@@ -0,0 +1,9 @@
+module CDT where
+
+import Variance
+
+data CDT
+
+functName     :: CDT -> String
+functVariance :: CDT -> [Variance]
+_eqCDT        :: CDT -> CDT -> Bool
diff --git a/src/CDTParser.hs b/src/CDTParser.hs
new file mode 100644
--- /dev/null
+++ b/src/CDTParser.hs
@@ -0,0 +1,102 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  CDTParser
+-- Copyright   :  (c) Masahiro Sakai 2006,2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-----------------------------------------------------------------------------
+
+module CDTParser
+    ( FE
+    , Type
+    , CDTDecl
+    , cdtDecl
+    , evalCDTDecl
+    ) where
+
+import qualified FE
+import qualified Type as T
+import Type (GenType(..))
+import CDT
+import ParserUtils
+
+import Text.ParserCombinators.Parsec
+import Control.Monad
+import Data.List
+
+type FE   = FE.GenFE String
+type Type = T.GenType String
+data CDTDecl = CDTDecl !ObjectType String !Int String [(String, Type)]
+
+cdtDecl :: Parser CDTDecl
+cdtDecl = 
+    do t <- mplus (string' "left"  >> return LeftObject)
+                  (string' "right" >> return RightObject)
+       string' "object"
+       name <- ident
+       params <- option [] $ between (char' '(') (char' ')')
+                           $ sepBy ident (char' ',')
+       spaces
+       string' "with"
+       fact_name <- ident
+       let endObject  = string' "end" >> string' "object"
+           normalDecl = do string' "is"
+                           manyTill (try (nat_decl (name : params)))
+                                    (try endObject)
+           emptyDecl  = endObject >> return []
+       nat_decls <- normalDecl <|> emptyDecl
+       return $ CDTDecl t name (length params) fact_name nat_decls
+
+nat_decl :: [String] -> Parser (String, Type)
+nat_decl params = 
+    do name <- ident
+       char' ':'
+       let f x = x `elemIndex` params
+       a <- fe f
+       string' "->"
+       b <- fe f
+       return (name, a :-> b)
+
+fe :: (String -> Maybe Int) -> Parser FE
+fe lookupVar = fe'
+    where fe' = 
+            do name <- ident
+               params <- option [] $ between (char' '(') (char' ')')
+                                   $ sepBy fe' (char' ',')
+               spaces
+               return $ case lookupVar name of
+                        Just n  -> FE.Var n
+                        Nothing -> FE.Ap name params
+
+-----------------------------------------------------------------------------
+
+type CDTEnv = [CDT]
+
+evalCDTDecl :: Monad m => CDTEnv -> CDTDecl -> m CDT
+evalCDTDecl cenv (CDTDecl lr name arity fact_name nat_decls) =
+    do nat_decls' <- mapM (evalNatDecl cenv) nat_decls
+       return $ mkCDT lr name arity fact_name nat_decls'
+
+evalNatDecl :: Monad m => CDTEnv -> (String, Type) -> m (String, T.Type)
+evalNatDecl cenv (name, a :-> b) =
+    do a' <- evalFE cenv a
+       b' <- evalFE cenv b
+       return (name, a' :-> b')
+
+evalFE :: Monad m => CDTEnv -> FE -> m FE.FE
+evalFE _ (FE.Var n) = return (FE.Var n)
+evalFE cenv (FE.Ap sym xs) =
+    do ys <- mapM (evalFE cenv) xs
+       case find (\cdt -> sym == CDT.functName cdt) cenv of
+        Just f ->
+            if CDT.functArity f == length xs
+               then return (FE.Ap f ys)
+               else fail "wrong number of arguments"
+        Nothing ->
+            fail $ "no such functor or variable: " ++ sym
+
+-----------------------------------------------------------------------------
diff --git a/src/CPLSystem.hs b/src/CPLSystem.hs
new file mode 100644
--- /dev/null
+++ b/src/CPLSystem.hs
@@ -0,0 +1,162 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  CPLSystem
+-- Copyright   :  (c) Masahiro Sakai 2004,2009
+
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-----------------------------------------------------------------------------
+
+module CPLSystem
+    ( VarTable
+    , System (..)
+    , emptySystem
+    , parseExp
+    , checkName
+    , parseCDT
+    , parseDef
+    , addCDT
+    , letExp
+    , simp
+    ) where
+
+import CDT
+import qualified CDTParser
+import qualified ExpParser
+import Exp
+import qualified AExp
+import qualified Simp
+import Type
+import qualified Typing
+import Typing (Typing(..))
+
+-- FIXME
+import qualified FE
+import qualified Subst
+
+import Control.Monad
+import Data.Maybe
+import Data.List
+import Text.ParserCombinators.Parsec
+import qualified Data.Map as Map
+
+type CDTEnv = [CDT]
+
+type VarTable = Map.Map Id ([Id], Exp, FType)
+
+data System
+    = System
+    { objects  :: !CDTEnv
+    , varTable :: !VarTable
+    , trace    :: !Bool
+    , lastExp  :: !(Maybe Exp)
+    }
+
+emptySystem :: System
+emptySystem =
+    System{ objects  = []
+          , varTable = Map.empty
+          , trace    = False
+          , lastExp  = Nothing
+          }
+
+parseExp :: System -> String -> Either String (Int, Typing)
+parseExp sys str =
+  case parse ExpParser.exp "" str of
+    Left err -> fail (show err)
+    Right e ->
+      case ExpParser.evalExp (objects sys) (arityEnv sys) e of
+        Nothing -> Left "invalid expression" -- FIXME
+        Just e ->
+          Typing.runTI (tiEnv sys) $ do
+            t <- Typing.inferType (substIt sys e)
+            t <- Typing.appSubst t
+            return $ AExp.quantify t
+
+type Def = (Id, [Id], AExp.AExp, FType)
+
+parseDef :: System -> String -> Either String Def
+parseDef sys str =
+  case parse ExpParser.def "" str of
+    Left err -> fail (show err)
+    Right (name,ps,e) ->
+      case ExpParser.evalExp (objects sys) (Map.union (Map.fromList (zip ps (repeat 0))) (arityEnv sys)) e of
+        Nothing -> Left "invalid definition" -- FIXME
+        Just e1 ->
+          Typing.runTI (tiEnv sys) $ do
+            (ts, t) <- Typing.inferType2 ps e1
+            ts <- Typing.appSubst ts
+            t@(ae :! t') <- Typing.appSubst t
+            let vars = Subst.tv (t' : ts)
+                s = zip vars [FE.Var i | i<-[0..]]
+            return (name, ps, Subst.apply s ae, FType (length vars) (Subst.apply s ts) (Subst.apply s t'))
+
+arityEnv :: System -> Map.Map Id Int
+arityEnv sys = if isJust (lastExp sys) then Map.insert "it" 0 env0 else env0
+  where env0 = Map.map (\(ps,_,_) -> length ps) (varTable sys)
+
+tiEnv :: System -> Map.Map Id (Either FType Type)
+tiEnv sys = Map.map (\(ps, body, t) -> Left t) (varTable sys)
+
+substIt :: System -> Exp -> Exp
+substIt sys e = 
+  case lastExp sys of
+    Just it -> f it e
+    Nothing -> e
+  where
+    f it Identity         = Identity
+    f it (Comp a b)       = Comp (f it a) (f it b)
+    f it e@(Nat _)        = e
+    f it (Fact obj args)  = Fact obj $ map (f it) args
+    f it (Funct obj args) = Funct obj $ map (f it) args
+    f it (Var "it" [])    = it
+    f it (Var v args)     = Var v $ map (f it) args
+
+checkName :: Monad m => System -> String -> m ()
+checkName sys name =
+  if name `elem` names
+    then fail ("\"" ++ name ++ "\" is already used")
+    else return ()
+  where
+    vt = varTable sys
+    objs = objects sys
+    names = Map.keys vt ++
+            map CDT.functName objs ++
+            map CDT.factName objs  ++
+            concatMap (map CDT.natName . CDT.nats) objs
+
+parseCDT :: Monad m => System -> String -> m CDT.CDT
+parseCDT sys src = case parse CDTParser.cdtDecl "" src of
+                   Left err   -> fail (show err)
+                   Right decl -> CDTParser.evalCDTDecl (objects sys) decl
+
+addCDT :: Monad m => System -> CDT.CDT -> m System
+addCDT sys obj =
+    if CDT.isComputable obj
+    then do checkName sys (CDT.functName obj)
+            checkName sys (CDT.factName obj)
+            mapM_ (checkName sys . CDT.natName) (CDT.nats obj)
+            return sys{ objects = obj : objects sys }
+    else fail "not a computable object"
+
+compile :: System -> Exp -> Simp.CompiledExp
+compile sys e = Simp.compile env e
+  where env = Map.map (\(ps,body,_) -> (ps, body)) (varTable sys)
+
+letExp :: Monad m => System -> Def -> m System
+letExp sys (name,ps,e,ftype) = do
+  checkName sys name
+  return sys{ varTable = Map.insert name (ps, AExp.skelton e, ftype) (varTable sys) }
+
+simp :: System -> Bool -> Exp -> [(Int, Simp.CompiledExp, Simp.CompiledExp)]
+simp sys full exp =
+    let exp' = compile sys exp
+        traces =
+            if trace sys
+               then Simp.simpWithTrace full exp'
+               else [(0, compile sys Identity, Simp.simp full exp')]
+    in traces
diff --git a/src/Exp.hs b/src/Exp.hs
new file mode 100644
--- /dev/null
+++ b/src/Exp.hs
@@ -0,0 +1,64 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Exp
+-- Copyright   :  (c) Masahiro Sakai 2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- Expression of CPL.
+--
+-----------------------------------------------------------------------------
+
+module Exp
+    ( Id
+    , Exp (..)
+    , comp
+    , expandFunct
+    ) where
+
+import qualified CDT
+import qualified FE
+import Type (GenType(..))
+import Data.List (intercalate)
+
+----------------------------------------------------------------------------
+
+type Id = String
+
+data Exp
+    = Identity
+    | Comp Exp Exp
+    | Nat !CDT.Nat
+    | Fact !CDT.CDT ![Exp]
+    | Funct !CDT.CDT ![Exp]
+    | Var !Id ![Exp]
+
+instance Show Exp where
+    show Identity = "I"
+    show (Comp a b) = show a ++ "." ++ show b
+    show (Nat nat)   = CDT.natName nat
+    show (Fact fact args) = CDT.factName fact ++ showArgs args
+    show (Funct funct args) = CDT.functName funct ++ showArgs args
+    show (Var name args) = name ++ showArgs args
+
+showArgs :: [Exp] -> String
+showArgs [] = ""
+showArgs args = "(" ++ intercalate "," (map show args) ++ ")"
+
+{-# INLINE comp #-}
+comp :: Exp -> Exp -> Exp
+comp a Identity = a
+comp Identity b = b
+comp a b        = Comp a b
+
+expandFunct :: CDT.CDT -> [Exp] -> Exp
+expandFunct _   []   = Identity
+expandFunct obj args = Fact obj (map g (CDT.nats obj))
+    where g nat = FE.fold h expandFunct cod `comp`
+                  (Nat nat `comp` FE.fold h expandFunct dom)
+              where h 0 = Identity
+                    h i = args !! (i-1)
+                    dom:->cod = CDT.natDeclType nat
diff --git a/src/ExpParser.hs b/src/ExpParser.hs
new file mode 100644
--- /dev/null
+++ b/src/ExpParser.hs
@@ -0,0 +1,90 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  ExpParser
+-- Copyright   :  (c) Masahiro Sakai 2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-----------------------------------------------------------------------------
+
+module ExpParser
+    ( Exp (..)
+    , exp
+    , def
+    , evalExp
+    ) where
+
+import qualified CDT
+import qualified Exp as E
+import ParserUtils
+
+import Prelude hiding (exp)
+import Control.Monad
+import Text.ParserCombinators.Parsec
+import Data.Maybe
+import qualified Data.Map as Map
+
+----------------------------------------------------------------------------
+
+data Exp
+    = Comp Exp Exp
+    | Ident String [Exp]
+    deriving (Show, Read)
+
+exp :: Parser Exp
+exp =
+    do xs <- sepBy1 pident (tok (char '.' `mplus` char '\x2218'))
+       return (foldr1 Comp xs)
+    where pident = 
+              do s  <- ident
+                 xs <- option [] $ between (char' '(') (char' ')')
+                                 $ exp `sepBy` char' ','
+                 spaces
+                 return (Ident s xs)
+
+def :: Parser (E.Id, [E.Id], Exp)
+def = do
+  spaces
+  s <- ident
+  ps <- option [] $ between (char' '(') (char' ')') $ ident `sepBy` char' ','
+  spaces
+  char' '='
+  body <- exp
+  spaces
+  return (s, ps, body)
+
+----------------------------------------------------------------------------
+
+type CDTEnv = [CDT.CDT]
+
+evalExp :: CDTEnv -> (Map.Map String Int) -> Exp -> Maybe E.Exp
+evalExp cenv env = listToMaybe . f
+    where f (Comp a b) =
+              do a' <- f a
+                 b' <- f b
+                 return (E.Comp a' b')
+          f (Ident "I" args) =
+              do guard (length args == 0)
+                 return E.Identity
+          f (Ident s args)  =
+              do let arity = length args
+                 args' <- mapM f args
+                 o <- cenv
+                 msum [ do guard $ CDT.functName o  == s &&
+                                   CDT.functArity o == arity
+                           return (E.Funct o args')
+                      , do guard $ CDT.factName o == s &&
+                                   CDT.nNats o == arity
+                           return (E.Fact o args')
+                      , do guard $ arity == 0
+                           n <- CDT.nats o
+                           guard $ CDT.natName n == s
+                           return (E.Nat n)
+                      , do guard $ Just arity == Map.lookup s env
+                           return (E.Var s args')
+                      ]
+
+----------------------------------------------------------------------------
diff --git a/src/FE.hs b/src/FE.hs
new file mode 100644
--- /dev/null
+++ b/src/FE.hs
@@ -0,0 +1,81 @@
+{-# OPTIONS -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  FE
+-- Copyright   :  (c) Masahiro Sakai 2004,2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- Functorial expression and functorial calculus.
+--
+-----------------------------------------------------------------------------
+
+module FE
+    ( VarId
+    , GenFE (..)
+    , FE
+    , fold
+    , GenCFE (..)
+    , CFE
+    ) where
+
+import Variance
+import Funct
+import {-# SOURCE #-} CDT (CDT, functName, functVariance, _eqCDT)
+
+import Data.List (transpose, intercalate)
+
+----------------------------------------------------------------------------
+
+type VarId = Int
+
+showVarId :: VarId -> String
+showVarId v = seq m $ seq n $
+              '*' : (table !! n) : (if m /= 0 then show m else "")
+    where table = ['a'..'z']
+          tableSize = length table
+          (m,n) = v `divMod` tableSize
+
+----------------------------------------------------------------------------
+-- Functorial Expression
+
+data GenFE f = Var !VarId | Ap !f [GenFE f] --deriving Eq
+type FE = GenFE CDT
+
+instance Eq FE where
+    Var i == Var j     = i==j
+    Ap f xs == Ap g ys = _eqCDT f g && xs==ys
+    _ == _ = False
+
+instance Show FE where
+    show = fold showVarId f
+        where f funct args =
+                  case functVariance funct of
+                  [] -> functName funct
+                  _  -> functName funct ++ "(" ++ intercalate "," args ++ ")"
+
+{-# INLINE fold #-}
+fold :: (VarId -> a) -> (f -> [a] -> a) -> GenFE f -> a
+fold f g = func
+    where func (Var v) = f v
+          func (Ap funct l) = g funct (map func l)
+
+----------------------------------------------------------------------------
+-- Closed Functorial Expression
+
+data GenCFE f = CFE !Int !(GenFE f)
+type CFE = GenCFE CDT
+
+instance Funct f => Funct (GenCFE f) where
+    variance (CFE n fe) = fold f g fe
+        where f v = [if x==v then Covariance else FreeVariance | x <- [0..(n-1)] ]
+              g obj args = case variance obj of
+                           [] -> nFree
+                           xs -> [ joinL [x `mult` y | (x,y) <- zip xs col]
+                                 | col <- transpose args ]
+              nFree = replicate n FreeVariance
+
+----------------------------------------------------------------------------
diff --git a/src/Funct.hs b/src/Funct.hs
new file mode 100644
--- /dev/null
+++ b/src/Funct.hs
@@ -0,0 +1,8 @@
+module Funct
+    ( Funct(..)
+    ) where
+
+import Variance
+
+class Funct f where
+    variance :: f -> [Variance]
diff --git a/src/Main.hs b/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Main.hs
@@ -0,0 +1,418 @@
+{-# LANGUAGE CPP #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Main
+-- Copyright   :  (c) Masahiro Sakai 2004,2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-----------------------------------------------------------------------------
+
+module Main where
+
+import CDT
+import Exp
+import qualified Statement
+import qualified CPLSystem as Sys
+import qualified AExp
+import Type
+import Typing (Typing(..))
+import qualified Simp
+
+import Data.Maybe
+import Data.List
+import Data.Char (isSpace)
+import System.Environment
+import System.Exit
+import System.IO
+import Control.Monad.State
+import Control.Monad.Error
+import System.Console.GetOpt
+#ifdef HAVE_READLINE_PACKAGE
+import qualified System.Console.SimpleLineEditor as SLE
+#endif
+import Control.Exception
+
+----------------------------------------------------------------------------
+
+type UIState = Sys.System
+
+getSystem :: (Monad m) => StateT UIState m Sys.System
+getSystem = get
+
+putSystem :: (Monad m) => Sys.System -> StateT UIState m ()
+putSystem = put
+
+initialState :: UIState
+initialState = Sys.emptySystem
+
+----------------------------------------------------------------------------
+--- Utility
+
+shift :: String -> (String, String)
+shift = break isSpace . dropWhile isSpace
+
+strip :: String -> String
+strip = reverse . f . reverse . f
+    where f = dropWhile isSpace
+
+indent :: Int -> String -> String
+indent n = unlines . map (prefix++) . lines
+    where prefix = replicate n ' '
+
+showObjectInfo :: CDT.CDT -> String
+showObjectInfo obj =
+    t ++ showFunctNameWithVariance obj ++ "\n" ++
+    "- natural transformations:\n" ++
+    natsStr ++
+    "- factorizer:\n" ++ factorizerInfoStr ++
+    "- equations:\n" ++ indent 4 equations ++
+    "- unconditioned: " ++ (if CDT.isUnconditioned obj then "yes" else "no") ++
+    "\n" ++
+    "- productive: (" ++ productiveStr ++ ")\n"
+    where t = case CDT.objectType obj of
+              LeftObject  -> "left object "
+              RightObject -> "right object "
+          natsStr = indent 4 $ concatMap f (CDT.nats obj)
+              where f nat = CDT.natName nat ++ ": " ++
+                            show (CDT.natType nat) ++ "\n"
+          productiveStr = intercalate "," (map f [0 .. CDT.functArity obj - 1])
+              where f n = if CDT.isProductiveIn obj n
+                          then "yes"
+                          else "no"
+          factorizerInfoStr =
+              indent 4 $
+                  upper ++ "\n" ++
+                  replicate (max (length upper) (length lower)) '-' ++ "\n" ++
+                  lower ++ "\n"
+              where upper = intercalate "  " $ zipWith f factArgs $ factParams obj
+                        where f fact typ = show fact ++ ": " ++ show typ
+                    lower =
+                        show (Fact obj factArgs) ++ ": " ++
+                        show (factDestType obj)
+                    factArgs = map f (CDT.nats obj)
+                        where f nat = Var ("f" ++ show (CDT.natIndex nat)) []
+          equations = concat (map (++"\n") (eqs ++ [feq, ceq]))
+              where eqs = zipWith g [(1::Int)..] (Statement.eqs obj)
+                        where g n eq = "("++lr++"EQ" ++ show n ++ "): " ++
+                                       show eq
+                    feq = "("++lr++"FEQ): " ++ show (Statement.feq obj)
+                    ceq = "("++lr++"CEQ): " ++ show (Statement.ceq obj)
+                    lr = case CDT.objectType obj of
+                         LeftObject  -> "L"
+                         RightObject -> "R"
+
+readLine :: String -> IO String
+#ifdef HAVE_READLINE_PACKAGE
+readLine prompt = fmap (fromMaybe "") (SLE.getLineEdited prompt)
+#else
+readLine prompt =
+    do putStr prompt
+       getLine
+#endif
+
+----------------------------------------------------------------------------
+
+type Command = String -> StateT UIState IO ()
+
+commandTable :: [(String, Command)]
+commandTable =
+    [ ("show",  cmdShow)
+    , ("edit",  cmdEdit)
+    , ("simp",  cmdSimp)
+    , ("let",   cmdLet)
+    , ("load",  cmdLoad)
+    , ("quit",  cmdQuit)
+    , ("exit",  cmdQuit)
+    , ("bye",   cmdQuit)
+    , ("help",  cmdHelp)
+    , ("set",   cmdSet)
+    , ("reset", cmdReset)
+
+    , ("left",  cmdLeft)
+    , ("right", cmdRight)
+    ]
+
+dispatchCommand :: String -> StateT UIState IO ()
+dispatchCommand l =
+    case shift l of
+        ([], _) -> return ()
+        (cmdStr, arg) ->
+            case lookup cmdStr commandTable of
+            Just cmd -> cmd arg
+            Nothing  -> throwError (userError ("unknown command: " ++ l))
+
+----------------------------------------------------------------------------
+
+defineObject :: Command
+defineObject src =
+    do sys <- getSystem
+       obj <- Sys.parseCDT sys src
+       sys' <- Sys.addCDT sys obj
+       putSystem sys'
+       let lr = case CDT.objectType obj of
+                     LeftObject  -> "left"
+                     RightObject -> "right"
+           msg = concat [lr, " object ", showFunctNameWithVariance obj, " is defined"]
+       lift $ putStrLn $ msg
+
+cmdLeft, cmdRight :: Command
+cmdLeft  s = defineObject ("left " ++ s)
+cmdRight s = defineObject ("right " ++ s)
+
+cmdShow :: Command
+cmdShow arg =
+    case shift arg of
+    ("object", arg') ->
+        do sys <- getSystem
+           let name    = strip arg'
+               objects = Sys.objects sys
+           lift $ putStrLn $
+                case find (\x -> CDT.functName x == name) objects of
+                Just obj -> showObjectInfo obj
+                Nothing  -> "unknown object: " ++ name
+    ("aexp", arg') -> do -- XXX
+      sys <- getSystem
+      case Sys.parseExp sys (strip arg') of
+        Left err -> fail err
+        Right (_, e :! t) -> lift $ do
+          putStrLn $ show e
+          putStrLn $ "    : " ++ show t
+    _ -> do
+      sys <- getSystem
+      case Sys.parseExp sys (strip arg) of
+        Left err -> fail err
+        Right (_, e :! t) -> lift $ do
+          putStrLn $ show $ AExp.skelton e
+          putStrLn $ "    : " ++ show t
+
+cmdLet :: Command
+cmdLet arg = do
+  sys <- getSystem
+  case Sys.parseDef sys (strip arg) of
+    Left err -> fail err
+    Right def@(name, args, e, FType _ args' t) -> do
+      sys' <- Sys.letExp sys def
+      putSystem sys'
+      if null args
+        then lift $ do
+          putStrLn $ name ++ " = " ++ show (AExp.skelton e)
+          putStrLn $ "    : " ++ show t
+        else lift $ do
+          let lhs = name ++ "(" ++ intercalate "," args ++ ")"
+          putStrLn $ lhs ++ " = " ++ show (AExp.skelton e)
+          let upper = intercalate "  " $ [p ++ ": " ++ show t | (p,t) <- zip args args']
+              lower = lhs ++ ": " ++ show t
+              s = upper ++ "\n" ++
+                  replicate (max (length upper) (length lower)) '-' ++ "\n" ++
+                  lower
+          putStrLn $ s
+          -- putStrLn $ "    : " ++ intercalate ", " (map show args') ++ " => " ++ show t
+
+cmdSimp :: Command
+cmdSimp arg =
+  case shift arg of
+    ("full", arg') ->
+        doSimp True (strip arg')
+    _ ->
+        doSimp False (strip arg)
+  where
+    doSimp full str = do
+      sys <- getSystem
+      unless (any isTerminalObject (Sys.objects sys))
+             (fail "No terminal object is defined.")
+      case Sys.parseExp sys str of
+        Left err -> fail err
+        Right (_, e :! t) -> do
+          unless (AExp.isElement e) (fail "not a element")
+          let traces = Sys.simp sys full (AExp.skelton e)
+              loop ((step,(depth,exp,cexp)) : xs) = do
+                let line = show step
+                         ++ (if depth==0 then "" else "[" ++ show depth ++ "]")
+                         ++ ":" ++ show (Simp.decompile exp) ++ "*" ++ show (Simp.decompile cexp)
+                when (Sys.trace sys) $ lift $ putStrLn line
+                if null xs
+                  then do
+                    let it = Simp.decompile cexp
+                    lift $ putStrLn (show it)
+                    lift $ putStrLn ("    : " ++ show t)
+                    putSystem sys{ Sys.lastExp = Just it }
+                  else
+                    loop xs
+          loop (zip [(0::Int)..] traces)
+
+cmdLoad :: Command
+cmdLoad s =
+    do h <- lift $ openFile filename ReadMode
+       contents <- lift $ hGetContents h
+       let src  = unlines (map removeComment (lines contents))
+           cmds = split src
+       mapM_ (\x -> do lift $ (putStr . unlines . map ("> "++) . lines $ x)
+                       dispatchCommand x)
+             cmds
+    where filename = -- FIXME
+              let s' = strip s in
+                  case s' of
+                  '"':_ -> read s'
+                  _     -> s'
+          removeComment []      = []
+          removeComment ('#':_) = []
+          removeComment (x:xs)  = x : removeComment xs
+          split :: String -> [String]
+          split s = map (strip . reverse) (f s [])
+              where f (';':xs) tmp = tmp : (f xs [])
+                    f (x:xs) tmp   = f xs (x:tmp)
+                    f [] tmp       = [tmp]
+
+cmdEdit :: Command
+cmdEdit _ =
+    do s <- lift editLoop
+       dispatchCommand s
+    where editLoop =
+              do l <- readLine "| "
+                 case dropWhile isSpace (reverse l) of
+                     ';':s -> return (reverse s)
+                     _ -> do s <- editLoop
+                             return $ l ++ "\n" ++ s
+
+cmdQuit :: Command
+cmdQuit _ = lift $ exitWith ExitSuccess
+
+cmdHelp :: Command
+cmdHelp _ = lift $ mapM_ putStrLn l
+    where l = [ "  exit                        exit the interpreter"
+              , "  quit                        ditto"
+              , "  bye                         ditto"
+              , "  edit                        enter editing mode"
+              , "  simp [full] <exp>           evaluate expression"
+              , "  show <exp>                  print type of expression"
+              , "  show object <functor>       print information of functor"
+              , "  load <filename>             load from file"
+              , "  set trace [on|off]          enable/disable trace"
+              , "  reset                       remove all definitions"
+              ]
+
+cmdSet :: Command
+cmdSet arg =
+    case shift arg of
+    (flag, a) ->
+        case shift a of
+        ([], _) ->
+            case flag of
+            "trace" ->
+                do sys <- getSystem
+                   lift $ putStrLn $
+                            "trace=" ++ (if Sys.trace sys then "on" else "off")
+            _ ->
+                lift $ putStrLn $ "unknown flag:" ++ flag
+        (value, _) ->
+            case flag of
+            "trace" ->
+                case value of
+                "on"  ->
+                    do sys <- getSystem
+                       putSystem (sys{ Sys.trace = True })
+                "off" ->
+                    do sys <- getSystem
+                       putSystem (sys{ Sys.trace = False })
+                _ ->
+                    lift $ putStrLn ("unknown value:" ++ value)
+            _ ->
+                lift $ putStrLn ("unknown flag:" ++ flag)
+
+cmdReset :: Command
+cmdReset _ = put initialState
+
+----------------------------------------------------------------------------
+
+data Flag
+    = Help
+    | Version
+    | Interactive
+    -- | Load String
+    | Trace String
+    deriving Eq
+
+options :: [OptDescr Flag]
+options =
+    [ Option ['h'] ["help"]    (NoArg Help)            "show help"
+    , Option ['v'] ["version"] (NoArg Version)         "show version number"
+    , Option ['i'] ["interactive"] (NoArg Interactive) "force interactive mode"
+    -- , Option ['l'] ["load"]    (ReqArg Load "FILE") "load FILE"
+    , Option ['t'] ["trace"]    (OptArg (Trace . fromMaybe "on") "[on|off]")
+             "enable/disable trace"
+    ]
+
+main :: IO ()
+main =
+#ifndef HAVE_READLINE_PACKAGE
+    do bracket (do x <- hGetBuffering stdout
+                   hSetBuffering stdout NoBuffering
+                   return x)
+               (hSetBuffering stdout)
+               (const main_)
+#else
+    do bracket SLE.initialise
+               (const SLE.restore)
+               (const main_)
+#endif
+
+main_ :: IO ()
+main_ =
+    do args <- getArgs
+       case getOpt Permute options args of
+         (o,_,[]) | Help `elem` o ->
+                      putStrLn (usageInfo header options)
+         (o,_,[]) | Version `elem` o ->
+                      putStrLn versionStr
+         (o,n,[]) ->
+             do putStr banner
+                evalStateT (do mapM_ processOpt o
+                               mapM_ cmdLoad n
+                               if null n || Interactive `elem` o
+                                   then mainLoop
+                                   else return ())
+                           initialState
+         (_,_,errs) ->
+             ioError $ userError $ concat errs ++ usageInfo header options
+
+version :: [Int]
+version = [0,0,2]
+
+versionStr :: String
+versionStr = intercalate "." $ map show $ version
+
+header :: String
+header = "Usage: cpl [OPTION...] files..."
+
+banner :: String
+banner =
+    "Categorical Programming Language (Haskell version)\n" ++
+    "version " ++ versionStr ++ "\n" ++
+    "\n" ++
+    "Type help for help\n" ++
+    "\n"
+
+processOpt :: Flag -> StateT UIState IO ()
+processOpt (Trace s) =
+    do sys <- getSystem
+       val <- case s of
+              "on"  -> return True
+              "off" -> return False
+              _     -> fail "invalid option"
+       putSystem sys{ Sys.trace = val }
+       return ()
+processOpt _ = return ()
+
+mainLoop :: StateT UIState IO ()
+mainLoop =
+    do l <- lift $ readLine "cpl> "
+       catchError (dispatchCommand l)
+                  (lift . putStrLn . show)
+       mainLoop
+
+----------------------------------------------------------------------------
diff --git a/src/ParserUtils.hs b/src/ParserUtils.hs
new file mode 100644
--- /dev/null
+++ b/src/ParserUtils.hs
@@ -0,0 +1,26 @@
+module ParserUtils
+    ( tok
+    , char'
+    , string'
+    , Ident
+    , ident
+    ) where
+
+import Text.ParserCombinators.Parsec
+import Data.Char
+
+type Ident = String
+
+tok :: Parser a -> Parser a
+tok p = do x <- p
+           spaces
+           return x
+
+char' :: Char -> Parser Char
+char' = tok . char
+
+string' :: String -> Parser String
+string' = tok . string
+
+ident :: Parser Ident
+ident  = tok $ many1 $ satisfy $ \c -> isAlphaNum c || (c `elem` "'!_")
diff --git a/src/Simp.hs b/src/Simp.hs
new file mode 100644
--- /dev/null
+++ b/src/Simp.hs
@@ -0,0 +1,352 @@
+{- # OPTIONS -ddump-simpl -ddump-stg # -}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Simp
+-- Copyright   :  (c) Masahiro Sakai 2004-2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- Simplifier
+--
+-----------------------------------------------------------------------------
+
+module Simp
+    ( CompiledExp
+    , compile
+    , decompile
+    , simp
+    , simpWithTrace
+    ) where
+
+import qualified Exp as E
+import qualified CDT
+import qualified FE
+import Exp (Id)
+import Type
+import Control.Monad.RWS
+import Data.Array
+import qualified Data.Map as Map
+
+----------------------------------------------------------------------------
+
+data CompiledExp
+  = Identity
+  | Comp CompiledExp CompiledExp
+  | LNat !CDT.Nat
+  | RNat !CDT.Nat
+  | LFact !CDT.CDT [CompiledExp] !(Array Int CompiledExp)
+  | RFact !CDT.CDT [CompiledExp]
+  | Var E.Exp CompiledExp
+
+compile :: (Map.Map E.Id ([E.Id], E.Exp)) -> E.Exp -> CompiledExp
+compile env = f
+  where
+    f E.Identity         = Identity
+    f (E.Comp a b)       = f a `comp` f b
+    f (E.Funct sym args) = expandFunct sym (map f args)
+    f (E.Fact sym args)  = mkFact sym (map f args)
+    f (E.Nat sym)        = mkNat sym
+    f src@(E.Var v args) = Var src (compile env' body)
+      where
+        (ps, body) = env Map.! v
+        -- Note that Map.union is left biased
+        env' = Map.union (Map.fromList [(p, ([], arg)) | (p,arg) <- zip ps args]) env
+
+{-# INLINE mkFact #-}
+mkFact :: CDT.CDT -> [CompiledExp] -> CompiledExp
+mkFact obj args =
+  case CDT.objectType obj of
+    CDT.LeftObject -> lfact
+      where
+        lfact = LFact obj args (listArray (0, CDT.nNats obj - 1) l)
+        l = zipWith f args (CDT.nats obj)
+        f arg nat =
+          case CDT.natIsUnconditioned nat of --- optimize
+            True  -> arg
+            False -> arg `comp` (subst1 lfact (CDT.natDeclDom nat))
+    CDT.RightObject -> RFact obj args
+
+{-# INLINE mkNat #-}
+mkNat :: CDT.Nat -> CompiledExp
+mkNat sym =
+  case CDT.objectType (CDT.natCDT sym) of
+    CDT.LeftObject  -> LNat sym
+    CDT.RightObject -> RNat sym
+
+decompile :: CompiledExp -> E.Exp
+decompile Identity = E.Identity
+decompile (Comp e1 e2) = E.Comp (decompile e1) (decompile e2)
+decompile (LNat nat) = E.Nat nat
+decompile (RNat nat) = E.Nat nat
+decompile (LFact sym args _) = E.Fact sym (map decompile args)
+decompile (RFact sym args)   = E.Fact sym (map decompile args)
+decompile (Var src _) = src
+
+----------------------------------------------------------------------------
+
+simp :: Bool -> CompiledExp -> CompiledExp
+simp full startExp =
+  if full
+  then simpFull startExp
+  else simpLazy startExp
+
+{-# NOINLINE simpFull #-}
+{-# NOINLINE simpLazy #-}
+simpFull, simpLazy :: CompiledExp -> CompiledExp
+simpFull = simpImpl True
+simpLazy = simpImpl False
+
+{-# INLINE simpImpl #-}
+simpImpl :: Bool -> CompiledExp -> CompiledExp
+simpImpl full startExp = seq full $ simp1 startExp Identity
+  where
+    simp1 :: CompiledExp -> CompiledExp -> CompiledExp
+
+    simp1 Identity c = c --- IDENT
+    
+    simp1 (Comp a b) c = simp1 a (simp1 b c) --- COMP
+    
+    simp1 e@(LNat _) c = e `comp` c -- L-NAT
+    simp1 (RNat sym) c
+      | full = simp1_FULL_R_NAT sym c --- FULL-R-NAT
+      | otherwise = simp1_R_NAT sym c --- R-NAT
+    
+    simp1 (LFact _ _ table) c = --- L-FACT
+      case split c of
+      (LNat sym, c') -> simp1 (table ! (CDT.natIndex sym)) c'
+      _ -> impossible
+    
+    simp1 e@(RFact obj args) c
+      | full && CDT.isUnconditioned obj = simp1_FULL_C_FACT obj args c
+      | otherwise = e `comp` c -- R-FACT
+    
+    simp1 (Var _ e) c = simp1 e c
+    
+    ----------------------------------
+    
+    simp1_R_NAT :: CDT.Nat -> CompiledExp -> CompiledExp
+    simp1_R_NAT sym c =
+      case simp2 c sym of
+      (factR@(RFact _ args), c'') ->
+        if CDT.natIsUnconditioned sym --- optimize
+        then simp1 (args !! CDT.natIndex sym) c''
+        else simp1 (subst1 factR (CDT.natDeclCod sym))
+                   (simp1 (args !! CDT.natIndex sym) c'')
+      _ -> impossible
+    
+    simp1_FULL_R_NAT :: CDT.Nat -> CompiledExp -> CompiledExp
+    simp1_FULL_R_NAT sym factP =
+        case pickupFactR sym factP of
+        (factR@(RFact _ args), factP') ->
+            if CDT.natIsUnconditioned sym
+            then simp1 (args !! CDT.natIndex sym) factP'
+            else simp1 (subst1 factR (CDT.natDeclCod sym))
+                       (simp1 (args !! CDT.natIndex sym) factP')
+        _ -> impossible
+    
+    simp1_FULL_C_FACT :: CDT.CDT -> [CompiledExp] -> CompiledExp -> CompiledExp
+    simp1_FULL_C_FACT obj args p = RFact obj (zipWith f args (CDT.nats obj))
+        {- 並列処理出来るのって、ここのzipWithくらいだろうか -}
+        where
+          f e nat =
+            case CDT.natDeclDom nat of
+              FE.Var 0 -> simp1 e p
+              fe       -> e `comp` subst1 p fe -- ack(3,3)で16000回くらい
+    
+    ----------------------------------
+    
+    simp2 :: CompiledExp -> CDT.Nat -> (CompiledExp, CompiledExp)
+    simp2 c sym = f (CDT.natProjectionSequence sym) c
+        where
+          f :: [Int] -> CompiledExp -> (CompiledExp, CompiledExp)
+          f [] c      = split c --- R-NAT-V
+          f (j:js) c_ =         --- R-NAT-F
+            case split c_ of
+            (RFact p args, c) ->
+                case g 0 args (CDT.nats p) of
+                    (factR, args') -> (factR, (RFact p args'))
+                where
+                  g i (arg:args) (nat:nats)
+                      | i==j =
+                          case f js (simp1 arg c) of
+                            (factR', arg') -> (factR',arg':args')
+                      | otherwise =
+                          let arg' = arg `comp` subst1 c (CDT.natDeclDom nat)
+                          in (factR, arg':args')
+                      where (factR, args') = g (i+1) args nats
+                  g _ [] [] = (undefined, [])
+                  g _ _ _ = impossible
+            _ -> impossible
+
+{-# INLINE pickupFactR #-}
+pickupFactR :: CDT.Nat -> CompiledExp -> (CompiledExp,CompiledExp)
+pickupFactR sym = f (CDT.natProjectionSequence sym)
+  where
+    f :: [Int] -> CompiledExp -> (CompiledExp, CompiledExp)
+    f [] e = split e
+    f (j:js) (RFact p args) =
+        case processArgs 0 args of
+          (factR, args') -> (factR, RFact p args')
+      where
+        processArgs :: Int -> [CompiledExp] -> (CompiledExp, [CompiledExp])
+        processArgs i (arg:args)
+            | i==j =
+                case f js arg of
+                  (factR, arg') -> (factR, arg':args)
+            | otherwise =
+                case processArgs (i+1) args of
+                  (factR, args') -> (factR, arg:args')
+        processArgs _ _ = impossible
+    f _ _ = impossible
+
+----------------------------------------------------------------------------
+
+type Trace = [(Int,CompiledExp,CompiledExp)]
+type M = RWS Int Trace ()
+
+runM :: M x -> Trace
+runM x =
+  case runRWS x 0 () of
+    (_,_,c) -> c
+
+trace :: CompiledExp -> CompiledExp -> M ()
+trace e c = do
+  depth <- ask
+  seq depth $ seq e $ seq c $ tell [(depth,e,c)]
+
+deepen :: M a -> M a
+deepen = local (+1)
+
+simpWithTrace :: Bool -> CompiledExp -> Trace
+simpWithTrace full startExp = seq full $ runM $ do
+    c <- simp1 startExp Identity
+    trace Identity c
+    return ()
+  where
+    simp1 :: CompiledExp -> CompiledExp -> M CompiledExp
+
+    simp1 a c = trace a c >> simp1' a c
+
+    simp1' Identity c = return c
+
+    simp1' (Comp a b) c = do
+      c' <- deepen (simp1 b c)
+      simp1 a c'
+
+    simp1' e@(LNat _) c = return (e `comp` c) --- L-NAT
+    simp1' (RNat sym) c
+      | full = simp1_FULL_R_NAT sym c --- FULL-R-NAT
+      | otherwise = simp1_R_NAT sym c --- R-NAT
+
+    simp1' (LFact _ _ table) c = --- L-FACT
+      case split c of
+        (LNat sym, c') -> simp1 (table ! (CDT.natIndex sym)) c'
+        _ -> impossible
+
+    simp1' e@(RFact obj args) c
+      | full && CDT.isUnconditioned obj = simp1_FULL_C_FACT obj args c --- FULL-C-FACT
+      | otherwise = return (e `comp` c) -- R-FACT
+
+    simp1' (Var _ e) c = simp1 e c
+
+    ----------------------------------
+
+    simp1_R_NAT :: CDT.Nat -> CompiledExp -> M CompiledExp
+    simp1_R_NAT sym c = do
+      tmp <- simp2 c sym
+      case tmp of
+        (factR@(RFact _ args), c'') ->
+          if CDT.natIsUnconditioned sym
+          then simp1 (args !! CDT.natIndex sym) c''
+          else simp1 (subst1 factR (CDT.natDeclCod sym) `comp` (args !! CDT.natIndex sym)) c''
+        _ -> impossible
+
+    simp1_FULL_R_NAT :: CDT.Nat -> CompiledExp -> M CompiledExp
+    simp1_FULL_R_NAT sym factP =
+      case pickupFactR sym factP of
+        (factR@(RFact _ args), factP') ->
+          if CDT.natIsUnconditioned sym
+          then simp1 (args !! CDT.natIndex sym) factP'
+          else simp1 (subst1 factR (CDT.natDeclCod sym) `comp` (args !! CDT.natIndex sym)) factP'
+        _ -> impossible
+
+    simp1_FULL_C_FACT :: CDT.CDT -> [CompiledExp] -> CompiledExp -> M CompiledExp
+    simp1_FULL_C_FACT obj args p = do
+      args' <- zipWithM f args (CDT.nats obj)
+      return (RFact obj args')
+      where
+        f e nat =
+          case CDT.natDeclDom nat of
+            FE.Var 0 -> simp1 e p
+            fe       -> return (e `comp` subst1 p fe) -- ack(3,3)で16000回くらい
+
+    ----------------------------------
+
+    simp2 :: CompiledExp -> CDT.Nat -> M (CompiledExp, CompiledExp)
+    simp2 c sym = f (CDT.natProjectionSequence sym) c
+      where
+        f :: [Int] -> CompiledExp -> M (CompiledExp, CompiledExp)
+        f [] c      = return (split c) --- R-NAT-V
+        f (j:js) c_ =                  --- R-NAT-F
+          case split c_ of
+            (RFact p args, c) -> do
+              (factR, args') <- g 0 args (CDT.nats p)
+              return (factR, (RFact p args'))
+              where
+                g _ [] [] = return (undefined, [])
+                g i (arg:args) (nat:nats)
+                  | i==j = do
+                    (_, args') <- g (i+1) args nats
+                    tmp <- simp1 arg c
+                    (factR', arg') <- f js tmp
+                    return (factR',arg':args')
+                  | otherwise = do
+                    (factR, args') <- g (i+1) args nats
+                    let arg' = arg `comp` subst1 c (CDT.natDeclDom nat)
+                    return (factR, arg':args')
+                g _ _ _ = impossible
+            _ -> impossible
+
+----------------------------------------------------------------------------
+
+{-# INLINE comp #-}
+comp :: CompiledExp -> CompiledExp -> CompiledExp
+comp a Identity = a
+comp Identity b = b
+comp a b        = Comp a b
+
+split :: CompiledExp -> (CompiledExp, CompiledExp)
+split (Comp a b) =
+    case split a of
+    (c, d) -> (c, d `comp` b)
+split a = (a,Identity)
+{-
+split :: CompiledExp -> (CompiledExp, CompiledExp)
+split (Comp a b) = go a b
+  where
+    go (Comp a b) r = go a (Comp b r)
+    go e r = (e, r)
+split e = (e, Identity)
+-}
+
+subst1 :: CompiledExp -> FE.FE -> CompiledExp
+subst1 x e = FE.fold f expandFunct e
+  where
+    f 0 = x
+    f _ = Identity
+
+expandFunct :: CDT.CDT -> [CompiledExp] -> CompiledExp
+expandFunct _   []   = Identity
+expandFunct obj args = mkFact obj (map g (CDT.nats obj))
+  where
+    g nat = FE.fold h expandFunct cod `comp` (mkNat nat `comp` FE.fold h expandFunct dom)
+      where
+        h 0 = Identity
+        h i = args !! (i-1)
+        dom:->cod = CDT.natDeclType nat
+
+impossible :: a
+impossible = error "impossible happens"
diff --git a/src/Statement.hs b/src/Statement.hs
new file mode 100644
--- /dev/null
+++ b/src/Statement.hs
@@ -0,0 +1,97 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Statement
+-- Copyright   :  (c) Masahiro Sakai 2004,2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-----------------------------------------------------------------------------
+
+module Statement
+    ( ConditionalEquation (..)
+    , Equation (..)
+    , eqs
+    , ceq
+    , feq
+    , statements
+    ) where
+
+import CDT
+import Exp
+import qualified FE
+import Data.List
+
+infix 4 :=:
+infixr 3 :=>
+
+data ConditionalEquation = [Equation] :=> Equation
+data Equation = Exp :=: Exp
+
+instance Show ConditionalEquation where
+    show (premisses :=> body) =
+        case premisses of
+        [] -> show body
+        _  -> intercalate " & " (map show premisses) ++ " => " ++ show body
+
+instance Show Equation where
+    show (a :=: b) = show a ++ "=" ++ show b
+
+eqs :: CDT.CDT -> [ConditionalEquation]
+eqs obj = map f (CDT.nats obj)
+    where f nat =
+              case CDT.objectType obj of
+              LeftObject ->
+                  [] :=>
+                  FE.fold g mkFunct (CDT.natDeclCod nat) `comp` Nat nat
+                  :=: (factArgs !! CDT.natIndex nat) `comp`
+                      FE.fold g mkFunct (CDT.natDeclDom nat)
+              RightObject ->
+                  [] :=>
+                  Nat nat `comp` FE.fold g mkFunct (CDT.natDeclDom nat)
+                  :=: FE.fold g mkFunct (CDT.natDeclCod nat) `comp`
+                      (factArgs !! CDT.natIndex nat)
+          factArgs = map (\i -> Var ("f" ++ show i) []) [0 .. CDT.nNats obj - 1]
+          g 0 = Fact obj factArgs
+          g _ = Identity
+
+ceq :: CDT -> ConditionalEquation
+ceq obj = map f (CDT.nats obj) :=> (u :=: Fact obj args)
+    where f nat =
+              case CDT.objectType obj of
+              LeftObject ->
+                  FE.fold g mkFunct (CDT.natDeclCod nat) `comp` Nat nat
+                  :=:
+                  (args !! CDT.natIndex nat) `comp`
+                    FE.fold g mkFunct (CDT.natDeclDom nat)
+              RightObject ->
+                  Nat nat `comp` FE.fold g mkFunct (CDT.natDeclDom nat)
+                  :=:
+                  FE.fold g mkFunct (CDT.natDeclCod nat) `comp`
+                  (args !! CDT.natIndex nat)
+          args = map (\i -> Var ("f" ++ show i) []) [0 .. CDT.nNats obj - 1]
+          u = Var "g" []
+          g 0 = u
+          g _ = Identity
+
+feq :: CDT -> ConditionalEquation
+feq obj = [] :=> Funct obj functArgs :=: Fact obj factArgs
+    where functArgs = map f [0 .. CDT.functArity obj - 1]
+              where f i = Var ("f" ++ show i) []
+          factArgs  = map f (CDT.nats obj)
+              where f nat = FE.fold g mkFunct (CDT.natDeclCod nat) `comp`
+                            Nat nat `comp`
+                            FE.fold g mkFunct (CDT.natDeclDom nat)
+                    g 0 = Identity
+                    g n = functArgs !! (n-1)
+
+statements :: CDT -> [ConditionalEquation]
+statements obj = eqs obj ++ [feq obj, ceq obj]
+
+-----------------------------------------------------------------------------
+
+mkFunct :: CDT -> [Exp] -> Exp
+mkFunct _ []     = Identity
+mkFunct obj args = Funct obj args
diff --git a/src/Subst.hs b/src/Subst.hs
new file mode 100644
--- /dev/null
+++ b/src/Subst.hs
@@ -0,0 +1,99 @@
+{-# OPTIONS -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Subst
+-- Copyright   :  (c) Masahiro Sakai 2006,2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  
+--
+-- Based on "Typing Haskell in Haskell".
+-- http://www.cse.ogi.edu/~mpj/thih/
+-----------------------------------------------------------------------------
+
+module Subst
+    ( Subst
+    , nullSubst
+    , (+->)
+    , FEs (..)
+    , (@@)
+    , merge
+    , mgu
+    , match
+    , varBind
+    ) where
+
+import FE
+import {-# SOURCE #-} CDT (_eqCDT)
+
+import Data.List (nub, intersect)
+import Data.Maybe (fromMaybe)
+
+
+type Subst = [(VarId,FE)]
+
+nullSubst :: Subst
+nullSubst = []
+
+(+->) :: VarId -> FE -> Subst
+u+->t = [(u,t)]
+
+class FEs t where
+    apply :: Subst -> t -> t
+    tv    :: t -> [VarId]
+
+instance FEs FE where
+    apply s = fold (\v -> fromMaybe (Var v) (lookup v s)) Ap
+    tv      = nub . fold return (const concat)
+
+instance FEs a => FEs [a] where
+    apply s = map (apply s)
+    tv      = nub . concat . map tv
+
+infixr 4 @@
+(@@) :: Subst -> Subst -> Subst
+s1 @@ s2 = [(u, apply s1 t) | (u,t) <- s2] ++ s1
+
+merge :: Monad m => Subst -> Subst -> m Subst
+merge s1 s2 = if agree then return (s1 ++ s2) else fail "merge fails"
+    where agree = all (\v -> apply s1 (Var v :: FE) == apply s2 (Var v))
+                      (map fst s1 `intersect` map fst s2)
+
+mgu :: Monad m => FE -> FE -> m Subst
+mgu (Ap obj1 args1) (Ap obj2 args2) =
+    if obj1 `_eqCDT` obj2
+       then mguList args1 args2
+       else fail "types do not unify"
+mgu (Var u) t = varBind u t
+mgu t (Var u) = varBind u t
+
+mguList :: Monad m => [FE] -> [FE] -> m Subst
+mguList (a:as) (b:bs) =
+    do s1 <- mgu a b
+       s2 <- mguList (apply s1 as) (apply s1 bs)
+       return (s2 @@ s1)
+mguList [] [] = return nullSubst
+mguList _ _   = fail "types do not unify"
+
+match :: Monad m => FE ->  FE -> m Subst
+match (Ap obj1 args1) (Ap obj2 args2) =
+    if obj1 `_eqCDT` obj2
+       then matchList args1 args2
+       else fail "types do not unify"
+match (Var u) t = varBind u t
+match _ _ = fail "types do not unify"
+
+matchList :: Monad m => [FE] -> [FE] -> m Subst
+matchList (a:as) (b:bs) =
+    do s1 <- match a b
+       s2 <- matchList (apply s1 as) (apply s1 bs)
+       return (s2 @@ s1)
+matchList [] [] = return nullSubst
+matchList _ _   = fail "types do not unify"    
+
+varBind :: Monad m => VarId -> FE -> m Subst
+varBind u t | t == Var u    = return nullSubst
+            | u `elem` tv t = fail "occurs check fails"
+            | otherwise     = return (u +-> t)
diff --git a/src/Type.hs b/src/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Type.hs
@@ -0,0 +1,44 @@
+{-# OPTIONS -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Type
+-- Copyright   :  (c) Masahiro Sakai 2006,2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-----------------------------------------------------------------------------
+
+module Type
+    ( GenType (..)
+    , Type
+    , FType (..)
+    ) where
+
+import FE
+import Subst
+import {-# SOURCE #-} CDT (CDT)
+
+import Data.List (nub)
+
+data GenType f
+    = (:->)
+    { dom :: !(GenFE f)
+    , cod :: !(GenFE f)
+    }
+
+type Type = GenType CDT
+
+instance Eq Type where
+    (a :-> b) == (c :-> d) = a==c && b==d
+
+instance FEs Type where
+    apply s (a :-> b) = apply s a :-> apply s b
+    tv (a :-> b)      = nub (tv a ++ tv b)
+
+instance Show Type where
+    show (a :-> b) = show a ++ " -> " ++ show b
+
+data FType = FType !Int [Type] Type
diff --git a/src/Typing.hs b/src/Typing.hs
new file mode 100644
--- /dev/null
+++ b/src/Typing.hs
@@ -0,0 +1,176 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+module Typing
+  ( Typing (..)
+  , inferType
+  , inferType2
+
+  , TI
+  , Env
+  , runTI
+  , getSubst
+  , extSubst
+  , appSubst
+  , unify
+  , newFEVar
+  ) where
+
+import Variance
+import Funct
+import qualified FE
+import qualified CDT
+import Type (GenType (..), Type, FType (..))
+import Subst
+import AExp
+import qualified Exp as E
+
+import Data.List (nub)
+import Control.Monad.Error
+import Control.Monad.RWS
+import qualified Data.Map as Map
+
+----------------------------------------------------------------------------
+
+infix 6 :!
+data Typing = AExp :! Type
+
+tm :: Typing -> AExp
+tm (e :! _) = e
+
+ty :: Typing -> Type
+ty (_ :! t) = t
+
+instance FEs Typing where
+  tv (e :! t)      = nub (tv e ++ tv t)
+  apply s (e :! t) = apply s e :! apply s t
+
+----------------------------------------------------------------------------
+
+-- Type inference monad
+newtype TI a = TI (RWST Env () TIState (Either String) a)
+  deriving (Monad, MonadState TIState, MonadReader Env, MonadError String)
+
+type Env = Map.Map E.Id (Either FType Type)
+type TIState = (Int, Subst)
+
+runTI :: Env -> TI a -> Either String a
+runTI env (TI m) = liftM fst (evalRWST m env initialState)
+  where initialState = (0, nullSubst)
+
+getSubst :: TI Subst
+getSubst = do
+  (_,s) <- get
+  return s
+
+extSubst :: Subst -> TI ()
+extSubst s2 = do
+  (i,s1) <- get
+  put (i, s2@@s1)
+  return ()
+
+appSubst :: (FEs a) => a -> TI a
+appSubst x = do
+  s <- getSubst
+  return (apply s x)
+
+unify :: FE.FE -> FE.FE -> TI ()
+unify a b = do
+  s1 <- getSubst
+  s2 <- mgu (apply s1 a) (apply s1 b)
+  extSubst s2
+
+newFEVar :: TI FE.FE
+newFEVar = do
+  (i,s) <- get
+  put (i+1,s)
+  return $ FE.Var i
+
+----------------------------------------------------------------------------
+
+inferType :: E.Exp -> TI Typing
+inferType E.Identity = iIdentity
+inferType (E.Comp a b) =  do
+  a' <- inferType a
+  b' <- inferType b
+  iComp a' b'
+inferType (E.Nat nat) = iNat nat
+inferType (E.Fact obj args)  = iFact obj  =<< mapM inferType args
+inferType (E.Funct obj args) = iFunct obj =<< mapM inferType args
+inferType (E.Var v args) = iVar v =<< mapM inferType args
+
+inferType2 :: [E.Id] -> E.Exp -> TI ([Type], Typing)
+inferType2 ps e = do
+  ps <- liftM Map.fromList $ forM ps $ \p -> do
+    dom <- newFEVar
+    cod <- newFEVar
+    return (p, dom :-> cod)
+  local (Map.union (Map.map Right ps)) $ do
+    t <- inferType e
+    return (map snd (Map.toList ps), t)
+
+----------------------------------------------------------------------------
+-- introduction rules
+
+iIdentity :: TI Typing
+iIdentity = do
+  v <- newFEVar
+  return $ Identity v :! v :-> v
+
+iComp :: Typing -> Typing -> TI Typing
+iComp (f :! domf :-> codf) (g :! domg :-> codg) = do
+  unify domf codg
+  return $ Comp f g :! domg :-> codf
+
+iNat :: CDT.Nat -> TI Typing
+iNat nat = do
+  annotation <- sequence $ replicate (CDT.natNTypeParams nat) newFEVar
+  return $ Nat nat annotation :! apply (zip [0..] annotation) (CDT.natType nat)
+
+iFact :: CDT.CDT -> [Typing] -> TI Typing
+iFact obj args = do
+  annotation <- sequence $ replicate (CDT.factNTypeParams obj) newFEVar
+  let s = zip [0..] annotation
+  unifyParams (apply s (CDT.factParams obj)) args
+  return $ Fact obj (map tm args) annotation :! apply s (CDT.factDestType obj)
+
+iFunct :: CDT.CDT -> [Typing] -> TI Typing
+iFunct obj args = do
+  (doml,codl) <- unifyParams (variance obj) args
+  return $ Funct obj (map tm args) :! FE.Ap obj doml :-> FE.Ap obj codl
+  where
+    unifyParams [] [] = return ([],[])
+    unifyParams (v:vs) ((_ :! d:->c) : as) = do
+      (doms,cods) <- unifyParams vs as
+      case v of
+        Covariance     -> return (d:doms, c:cods)
+        Contravariance -> return (c:doms, d:cods)
+        FixedVariance  -> unify d c >> return (d:doms, d:cods)
+        FreeVariance   -> do
+          x <- newFEVar
+          y <- newFEVar
+          return (x:doms, y:cods)
+    unifyParams _ _ = throwError "wrong number of arguments"
+
+iVar :: E.Id -> [Typing] -> TI Typing
+iVar v args = do
+  env <- ask
+  case Map.lookup v env of
+    Just (Right t) ->
+      return $ Var v [] [] t :! t
+    Just (Left (FType n typs typ)) -> do
+      annotation <- sequence (replicate n newFEVar)
+      let s = zip [0..] annotation
+      unifyParams (apply s typs) args
+      let t = apply s typ
+      return $ Var v annotation (map tm args) t :! t
+    Nothing -> throwError $ "no such variable: " ++ v
+
+unifyParams :: [Type] -> [Typing] -> TI ()
+unifyParams [] [] = return ()
+unifyParams ((pdom :-> pcod):ps) ((_ :! adom:->acod):as) = do
+  unify pdom adom
+  unify pcod acod
+  unifyParams ps as
+  return ()
+unifyParams _ _ = throwError "wrong number of arguments"
+
+----------------------------------------------------------------------------
diff --git a/src/Variance.hs b/src/Variance.hs
new file mode 100644
--- /dev/null
+++ b/src/Variance.hs
@@ -0,0 +1,75 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Variance
+-- Copyright   :  (c) Masahiro Sakai 2009
+-- License     :  BSD-style
+-- 
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- Variance calculation.
+--
+-----------------------------------------------------------------------------
+
+module Variance
+    ( Variance(..)
+    , top
+    , bottom
+    , join
+    , meet
+    , joinL
+    , meetL
+    , mult
+    , mnemonic
+    ) where
+
+data Variance
+    = Covariance     --- +
+    | Contravariance --- -
+    | FixedVariance  --- T
+    | FreeVariance   --- ⊥
+    deriving (Show,Read,Eq)
+
+mnemonic :: Variance -> String
+mnemonic Covariance     = "+"
+mnemonic Contravariance = "-"
+mnemonic FixedVariance  = "T"
+mnemonic FreeVariance   = "_|_"
+
+bottom, top :: Variance
+bottom = FreeVariance
+top    = FixedVariance
+
+join,meet :: Variance -> Variance -> Variance
+join a b | a==b            = a
+         | a==FreeVariance = b
+         | b==FreeVariance = a
+         | otherwise       = FixedVariance
+meet a b | a==b             = a
+         | a==FixedVariance = b
+         | b==FixedVariance = a
+         | otherwise        = FreeVariance
+
+joinL,meetL :: [Variance] -> Variance
+joinL = foldl join bottom
+meetL = foldl meet top
+
+{-
+
+・|⊥|+ |- |T
+--+--+--+--+--
+⊥|⊥|⊥|⊥|⊥
++ |⊥|+ |- |T
+- |⊥|- |+ |T
+T |⊥|T |T |T
+
+-}
+mult :: Variance -> Variance -> Variance
+mult _ FreeVariance  = FreeVariance
+mult FreeVariance _  = FreeVariance
+mult _ FixedVariance = FixedVariance
+mult FixedVariance _ = FixedVariance
+mult a Covariance    = a
+mult Covariance a    = a
+mult Contravariance Contravariance = Covariance