# 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 simply-typed 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 lambda-cube axies

- [x] Simply-typed lambda calculus
- [x] Polymorphic lambda calculus
- [x] Higher-order lambda calculus
- [x] Dependently-typed lambda calculus (dubiously, not got a implemented typesystem to back it up)

### TODOs

- [ ] Give
`Calculi.Lambda.Cube.Polymorphic.Unification`

better documentation (incl. diagrams for graph-related 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.
- [ ] Subhask-style automated test writing.
- [ ] Explore homotopy type theory
- [ ] Remove all extensions that aren't light syntactic sugar from
`default-extensions`

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 Hindley-Milner type inference algorithm, Dr Jeff Vaughan (x)

Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism, Dr. Gergő Érdi (x)

Many wikipedia pages on type theory.