inch
Inch is a typechecker for a subset of Haskell (plus some GHC extensions) with the addition of integer constraints. After successfully typechecking a source file, it outputs an operationally equivalent version with the typelevel integers erased, so it can be used as a preprocessor in order to compile programs.
This is a very rough and ready prototype. Many Haskell features are missing or poorly implemented.
Installation
cabal install inch
Features

A new kind Integer
for typelevel integers, together with a synonym Nat
for integers constrained to be nonnegative

Typelevel addition, subtraction, multiplication and exponentiation operations (plus a few more)

Contexts contain numeric equality and inequality constraints

Πtypes (dependent functions from integers) inspired by the SHE preprocessor, which erase to the corresponding nondependent functions

Guards can test numeric constraints and make this information available for typechecking (as in plan
below)

Powerful type inference using a novel approach to equational unification (though type signatures are needed for GADT pattern matches and polymorphic recursion)
Example
The following program defines a type of vectors (lists indexed by their length) and some functions using them.
{# OPTIONS_GHC F pgmF inch #}
{# LANGUAGE RankNTypes, GADTs, KindSignatures, ScopedTypeVariables, NPlusKPatterns #}
data Vec :: * > Nat > * where
VNil :: Vec a 0
VCons :: forall a (n :: Nat) . a > Vec a n > Vec a (n+1)
deriving Show
vreverse :: forall (n :: Nat) a . Vec a n > Vec a n
vreverse xs = vrevapp xs VNil
where
vrevapp :: forall (m n :: Nat) a . Vec a m > Vec a n > Vec a (m+n)
vrevapp VNil ys = ys
vrevapp (VCons x xs) ys = vrevapp xs (VCons x ys)
vec :: pi (n :: Nat) . a > Vec a n
vec {0} a = VNil
vec {n+1} a = VCons a (vec {n} a)
vlookup :: forall (n :: Nat) a . pi (m :: Nat) . m < n => Vec a n > a
vlookup {0} (VCons x _) = x
vlookup {k+1} (VCons _ xs) = vlookup {k} xs
plan :: pi (n :: Nat) . Vec Integer n
plan {0} = VNil
plan {m}  {m > 0} = VCons m (plan {m1})
After typechecking and preprocecessing with inch
, the resulting file is as follows.
{# LANGUAGE RankNTypes, GADTs, KindSignatures, ScopedTypeVariables, NPlusKPatterns #}
data Vec :: * > * where
VNil :: Vec a
VCons :: a > Vec a > Vec a
deriving Show
vreverse :: Vec a > Vec a
vreverse xs = vrevapp xs VNil
where
vrevapp :: Vec a > Vec a > Vec a
vrevapp VNil ys = ys
vrevapp (VCons x xs) ys = vrevapp xs (VCons x ys)
vec :: Integer > a > Vec a n
vec 0 a = VNil
vec (n+1) a = VCons a (vec n a)
vlookup :: Integer > Vec a n > a
vlookup 0 (VCons x _) = x
vlookup (k+1) (VCons _ xs) = vlookup k xs
plan :: Integer > Vec Integer
plan 0 = VNil
plan m  m > 0 = VCons m (plan (m1))
For more examples, look in the examples directory of the source distribution. These include:

More fun with vectors

Merge sort that maintains length and ordering invariants

Redblack tree insertion and deletion with ordering, colour and black height invariants guaranteed by types

Time complexity annotations showing that redblack tree insert/delete are linear in the black height, plus a few other examples

Units of measure with good type inference properties and (morally) no runtime overhead
Known limitations

Lots of Haskell features are unsupported, notably list comprehensions, do
notation, if
expressions, newtypes, field labels, ...

The parser is somewhat idiosyncratic; look at the examples to figure out what syntax it accepts. Data types must be defined in GADT syntax, using a kind signature rather than a list of variables. Parsing of infix operators is almost but not entirely nonexistent, so they must usually be written prefix.

Modules are poorly supported. A .inch
file is generated when preprocessing a module, listing the identifiers it defines, and this file is looked up when the module is imported. Because preprocessing happens in reverse dependency order, manual intervention may be required to generate .inch
files before they are needed (by loading dependencies in GHCi). Qualified names are not supported, so there will be problems if multiple modules bring the same name into scope.

Type classes are not completely implemented: ambiguity checking and defaulting are lacking, superclasses are not taken into consideration when solving constraints, and the constraint solver is untested.

No kind inference is performed, so type variables must be annotated with their kind if it is not *
. This means explicit forall
bindings must be used in some type signatures. Type variables in instance declarations cannot be annotated, so they may only have kind *
(at the moment).

Only GADTs involving typelevel numeric equalities are supported, not more general equations between types.

Support for higherrank types is limited.
Outstanding design issues

Metavariables are solved using equational unification in the abelian group of integers with addition, which works well, but a better story about ambiguity is needed.

Constraint solving is based on normalisation and a solver for Presburger arithmetic, so only linear constraints are guaranteed to be solved. Hard constraints can be dealt with by the user invoking higherrank functions that add facts to the context. A better characterisation of solvable constraints would be nice.

Exponentiation by a negative integer is possible but makes no sense.

At the moment, Nat
is just Integer
(with a positivity constraint added when it is used in a type signature). Kind polymorphism and subkinding might allow more precise kinds to be given to arithmetic operations, including a correct kind for exponentiation.

n+k
patterns provide quite a nice syntax for defining dependent numeric functions, but they have been deprecated and removed from Haskell 2010, so perhaps an alternative should be found.

Erasure for type classes involving numeric kinds is not yet properly specified.
Iavor Diatchki is working on TypeNats, an extension to GHC that aims to support typelevel natural numbers. He also implemented the presburger package, which inch
uses for constraint solving.
Conor McBride's Strathclyde Haskell Enhancement is a preprocessor that supports Πtypes and allows lifting algebraic data types (but not numeric types) to kinds. SHE inspired the braces syntax used in inch
. These ideas (and more, including kind polymorphism) are being implemented in GHC: see Giving Haskell a Promotion by Brent Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones and Dimitrios Vytiniotis.
Max Bolingbroke has implemented the new Constraint kind in GHC. This kind is supported by inch
but not erased, so it will only work if GHC support is present.
This work is inspired by Hongwei Xi's Dependent ML and its successor ATS, which support typelevel Presburger arithmetic.
Adam Gundry, adam.gundry@strath.ac.uk