typerbole
Parameterized typesystems, lambda cube typeclasses, and typechecking interfaces.
Parameterized Typesystems
Like how datatypes such as List a
([a]
), Set a
, Tree a
etc. in haskell have a parameter for a contained type, this library is based on the idea that a datatype that represents expressions can have a parameter for a typesystem.
An Example: The Lambda Calculus
As an example, we can put together a datatype that represents the syntax for the Lambda Calculus:
data LambdaTerm c v t =
Variable v  a variable bound by a lambda abstraction
 Constant c  a constant defined outside of the term
 Apply (LambdaTerm c v t) (LambdaTerm c v t)  an application of one term to another
 Lambda (v, t) (LambdaTerm c v t)  A lambda abstraction
This datatype has 3 parameters. The first two parameters represent constants and variables respectively, what's important is the final parameter t
which is the parameter for the typesystem being used.
We can use the typesystem SimplyTyped
in Compiler.Typesystem.SimplyTyped
as the typesystem to make this a simplytyped lambda calculus, or we could slot in SystemF
, SystemFOmega
, Hask
, to change the typesystem associcated with with it.
Sadly there's no magic that builds typecheckers for these (yet). Instead, using the language extensions MultiParamTypeClasses
and FlexibleInstances
and the Typecheckable
typeclass from Control.Typecheckable
we write a typechecker for each of these occurences.
instance (...) => Typecheckable (LambdaTerm c v) (SimplyTyped m) where
...
instance (...) => Typecheckable (LambdaTerm c v) (SystemF m p) where
...
instance (...) => Typecheckable (LambdaTerm c v) (SystemFOmega m p k) where
...
 and so on.
Or we can just ignore it all and turn it into an untyped lambda calculus:
type UntypedLambdaTerm c v = LambdaTerm c v ()
The Lambda Cube
The lambda cube describes the properties of a number of typesystems, an overview can be found here. It is the basis for the library's classification of typesystems, a typeclass hierarchy where each axis is represented by a typeclass whose methods and associated types are indicitive of the properties of the axis.
Supported lambdacube axies
 [x] Simplytyped lambda calculus
 [x] Polymorphic lambda calculus
 [x] Higherorder lambda calculus
 [x] Dependentlytyped lambda calculus (dubiously, not got a implemented typesystem to back it up)
TODOs
 [ ] Give
Calculi.Lambda.Cube.Polymorphic.Unification
better documentation (incl. diagrams for graphrelated functions/anything that'll benefit).
 [ ] Finish the
Typecheckable
& Inferable
instances for the typesystems in Compiler.Typesystem.*
 [ ] Put together a working travis file.
 [ ] Implement a Calculus of Constructions typesystem.
 [ ] Document the type expression psudocode
 [ ] Design a typeclass for typesystems with constraints (
Num a => ...
, a ~ T
etc).
 [ ] Provide a default way of evaluating lambda expressions.
 [ ] Make the quasiquoters use the lambda cube typeclasses instead of specific typesystem implementations.
 [ ] Subhaskstyle automated test writing.
 [ ] Explore homotopy type theory
 [ ] Remove all extensions that aren't light syntactic sugar from
defaultextensions
and declare them explicitly in the modules they're used.
 [ ] Listen to
Wall
 [ ] Move
Control.Typecheckable
to it's own package.
 [ ] Elaborate on the
Typecheck
type. Maybe make it a typeclass.
Papers, Sites and Books read during development

Introduction to generalized type systems, Dr Henk Barendregt (Journal of Functional Programming, April 1991)

A Modern Perspective on Type Theory (x)

A proof of correctness for the HindleyMilner type inference algorithm, Dr Jeff Vaughan (x)

Compositional Type Checking for HindleyMilner Type Systems with Adhoc Polymorphism, Dr. Gergő Érdi (x)

Many wikipedia pages on type theory.