Type arithmetic

Type arithmetic (or type-level computation) are calculations on the type-level, often implemented in Haskell using functional dependencies to represent functions.

A simple example of type-level computation are operations on Peano numbers:

 data Zero

 data Succ a

 class Add a b ab | a b -> ab, a ab -> b
 instance Add Zero b b
 instance (Add a b ab) => Add (Succ a) b (Succ ab)

Many other representations of numbers are possible, including binary and balanced base tree. Type-level computation may also include type representations of boolean values, lists, trees and so on. It is closely connected to theorem proving, via the Curry-Howard isomorphism.

A decimal representation was put forward by Oleg Kiselyov in "Number-Parameterized Types" in the fifth issue of The Monad Reader. There is an implementation in the type-level package, but unfortunately the arithmetic is really slow, because in fact it simulates Peano arithmetic with decimal numbers.

Library support

Robert Dockins has gone as far as to write a library for type level arithmetic, supporting the following operations on type level naturals: addition, subtraction, multiplication, division, remainder, GCD, and also contains the following predicates: test for zero, test for equality and < > <= >=

This library uses a binary representation and can handle numbers at the order of 10^15 (at least). It also contains a test suite to help validate the somewhat unintuitive algorithms.

More libraries:

• type-level Natural numbers in decimal representation using functional dependencies and Template Haskell. However arithmetic is performed in a unary way and thus it is quite slow.
• type-level-tf Similar to the type-level package (also in speed) but uses type families instead of functional dependencies and uses the same module names as the type-level package. Thus module name clashes are warranted if you have to use both packages.
• type-level-natural-number and related packages. A collection of packages where the simplest one is even Haskell2010.
• tfp Decimal representation, Type families, Template Haskell.
• typical Binary numbers and functional dependencies.
• type-unary Unary representation and type families.
• numtype, numtype-tf Unary representation and functional dependencies and type families, respectively.

More type hackery

Not to be outdone, Oleg Kiselyov has written on invertible, terminating, 3-place addition, multiplication, exponentiation relations on type-level Peano numerals, where any two operands determine the third. He also shows the invertible factorial relation. Thus providing all common arithmetic operations on Peano numerals, including n-base discrete logarithm, n-th root, and the inverse of factorial. The inverting method can work with any representation of (type-level) numerals, binary or decimal.

Oleg says, "The implementation of RSA on the type level is left for future work".

Djinn

Somewhat related is Lennart Augustsson's tool Djinn, a theorem prover/coding wizard, that generates Haskell code from a given Haskell type declaration.

Djinn interprets a Haskell type as a logic formula using the Curry-Howard isomorphism and then a decision procedure for Intuitionistic Propositional Calculus.

An Advanced Example : Type-Level Quicksort

An advanced example: quicksort on the type level.

Here is a complete example of advanced type level computation, kindly provided by Roman Leshchinskiy. For further information consult Thomas Hallgren's 2001 paper Fun with Functional Dependencies.

 module Sort where
 
 -- natural numbers
 data Zero
 data Succ a
 
 -- booleans
 data True
 data False
 
 -- lists
 data Nil
 data Cons a b
 
 -- shortcuts
 type One   = Succ Zero
 type Two   = Succ One
 type Three = Succ Two
 type Four  = Succ Three
 
 -- example list
 list1 :: Cons Three (Cons Two (Cons Four (Cons One Nil)))
 list1 = undefined
 
 -- utilities
 numPred :: Succ a -> a
 numPred = const undefined
 
 class Number a where
   numValue :: a -> Int
 
 instance Number Zero where
   numValue = const 0
 instance Number x => Number (Succ x) where
   numValue x = numValue (numPred x) + 1
 
 numlHead :: Cons a b -> a
 numlHead = const undefined
 
 numlTail :: Cons a b -> b
 numlTail = const undefined
 
 class NumList l where
   listValue :: l -> [Int]
 
 instance NumList Nil where
   listValue = const []
 instance (Number x, NumList xs) => NumList (Cons x xs) where
   listValue l = numValue (numlHead l) : listValue (numlTail l)
 
 -- comparisons
 data Less
 data Equal
 data Greater
 
 class Cmp x y c | x y -> c
 
 instance Cmp Zero Zero     Equal
 instance Cmp Zero (Succ x) Less
 instance Cmp (Succ x) Zero Greater
 instance Cmp x y c => Cmp (Succ x) (Succ y) c
 
 -- put a value into one of three lists according to a pivot element
 class Pick c x ls eqs gs ls' eqs' gs' | c x ls eqs gs -> ls' eqs' gs'
 instance Pick Less    x ls eqs gs (Cons x ls) eqs gs
 instance Pick Equal   x ls eqs gs ls (Cons x eqs) gs
 instance Pick Greater x ls eqs gs ls eqs (Cons x gs)
 
 -- split a list into three parts according to a pivot element
 class Split n xs ls eqs gs | n xs -> ls eqs gs
 instance Split n Nil Nil Nil Nil
 instance (Split n xs ls' eqs' gs',
           Cmp x n c,
 	  Pick c x ls' eqs' gs' ls eqs gs) =>
          Split n (Cons x xs) ls eqs gs
 
 listSplit :: Split n xs ls eqs gs => (n, xs) -> (ls, eqs, gs)
 listSplit = const (undefined, undefined, undefined)
 
 -- zs = xs ++ ys
 class App xs ys zs | xs ys -> zs
 instance App Nil ys ys
 instance App xs ys zs => App (Cons x xs) ys (Cons x zs)
 
 -- zs = xs ++ [n] ++ ys
 -- this is needed because
 --
 -- class CCons x xs xss | x xs -> xss
 -- instance CCons x xs (Cons x xs)
 --
 -- doesn't work
 
 class App' xs n ys zs | xs n ys -> zs
 instance App' Nil n ys (Cons n ys)
 instance (App' xs n ys zs) => App' (Cons x xs) n ys (Cons x zs)
 
 -- quicksort
 class QSort xs ys | xs -> ys
 instance QSort Nil Nil
 instance (Split x xs ls eqs gs,
           QSort ls ls',
 	  QSort gs gs',
 	  App eqs gs' geqs,
 	  App' ls' x geqs ys) =>
          QSort (Cons x xs) ys
 
 listQSort :: QSort xs ys => xs -> ys
 listQSort = const undefined

And we need to be able to run this somehow, in the typechecker. So fire up ghci:

 > :t listQSort list1
 Cons
     (Succ Zero)
     (Cons (Succ One) (Cons (Succ Two) (Cons (Succ Three) Nil)))

A Really Advanced Example : Type-Level Lambda Calculus

Again, thanks to Roman Leshchinskiy, we present a simple lambda calculus encoded in the type system (and with non-terminating typechecking fun!)

Below is an example which encodes a stripped-down version of the lambda calculus (with only one variable):

 {-# OPTIONS -fglasgow-exts #-}
 data X
 data App t u
 data Lam t

 class Subst s t u | s t -> u
 instance Subst X u u
 instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t')
 instance Subst (Lam t) u (Lam t)

 class Apply s t u | s t -> u
 instance (Subst s t u, Eval u u') => Apply (Lam s) t u'

 class Eval t u | t -> u
 instance Eval X X
 instance Eval (Lam t) (Lam t)
 instance (Eval s s', Apply s' t u) => Eval (App s t) u

Now, lets evaluate some lambda expressions:

 > :t undefined :: Eval (App (Lam X) X) u => u
 undefined :: Eval (App (Lam X) X) u => u :: X

Ok good, and:

 > :t undefined :: Eval (App (Lam (App X X)) (Lam (App X X)) ) u => u
 ^CInterrupted.

diverges ;)

Turing-completeness

It's possible to embed the Turing-complete SK combinator calculus at the type level.

Theory

See also dependent type theory.

Practice

Extensible records (which are used e.g. in type safe, declarative relational algebra approaches to database management)