typerbole: A typesystems library with exaggerated claims

[ ast, bsd3, educational, lambda-cube, library, type-theory, typechecking, typesystems ] [ Propose Tags ]
This version is deprecated.

Please see README.md


[Skip to Readme]

Downloads

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.0.0.1, 0.0.0.2, 0.0.0.3, 0.0.0.4, 0.0.0.5 (info)
Dependencies base (>=4.7 && <5), bifunctors (>=5), containers (>=0.5 && <0.6), data-ordlist, either, fgl (>=5.5 && <5.6), generic-random (==0.1.1.0), lens, megaparsec, mtl, QuickCheck, safe, semigroups, syb, template-haskell, th-lift [details]
License BSD-3-Clause
Copyright 2016 Fionan Haralddottir
Author Fionan Haralddottir
Maintainer ma302fh@gold.ac.uk
Revised Revision 1 made by Lokidottir at 2016-07-27T16:43:32Z
Category Typesystems , Typechecking , Type Theory , Educational , Lambda Cube , AST
Home page https://github.com/Lokidottir/typerbole
Bug tracker https://github.com/Lokidottir/typerbole/issues
Source repo head: git clone https://github.com/Lokidottir/typerbole
Uploaded by Lokidottir at 2016-07-27T15:55:23Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 2117 total (12 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2016-07-27 [all 1 reports]

Readme for typerbole-0.0.0.5

[back to package description]

typerbole hackage

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

  • Simply-typed lambda calculus
  • Polymorphic lambda calculus
  • Higher-order lambda calculus
  • 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.