WARNING: this is a research program
written as I learn and explore *lambda calculii*:
please understand well by yourself whatever you may take from it;
any question or contribution being welcome :-)

This package implements an *explicitely typed*
(aka. *à la Church*) *lambda calculus*
with: *simples types*, *parametric polymorphism*,
*higher-rank polymorphism* and *constructors of types*
(I have no need for *dependent types* so far,
but it should be straightforward to add them
to allow the full *Calculus of constructions* (CoC)).

This is mainly done by means of:
a common *Algebraic Data Type* (ADT) for terms and types
to build a *Pure Type System* (PTS),
generalized DeBruijn indices
to implement *capture-avoiding substitution* of variables,
and `Typeable`

axioms to embed Haskell types and terms
(the most experimental and tricky part).

The inspiring programs I studied
which explore similar problems:
Simon Peyton Jones and Erik Meijer's
Henk,
Dan Doel's pts,
Gabriel Gonzalez's morte,
Richard Eisenberg's glambda,
Edward Kmett's bound.

See also: the lol-typing package
studying the *type inferencing*.

NOTE: if you are just interested in building
an *Embedded Domain Specific Language* (EDSL)
you may as well study Oleg Kiselyov, Jacques Carette and Chung-chieh Shan's
Typed Tagless Final Interpreters,
which you may find being a much more simple, efficient and robust approach.