# Type arithmetic

### From HaskellWiki

DonStewart (Talk | contribs) (Roman provides a lambda calculus encoded on the type level, with Y combinators and all) |
(Changed Monad.Reader link refs.) |
||

(14 intermediate revisions by 7 users not shown) | |||

Line 5: | Line 5: | ||

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

+ | <haskell> | ||

data Zero | data Zero | ||

Line 12: | Line 13: | ||

instance Add Zero b b | instance Add Zero b b | ||

instance (Add a b ab) => Add (Succ a) b (Succ ab) | instance (Add a b ab) => Add (Succ a) b (Succ ab) | ||

+ | </haskell> | ||

Many other representations of numbers are possible, including binary and | Many other representations of numbers are possible, including binary and | ||

− | balanced base | + | balanced base tree. Type-level computation may also include type |

representations of boolean values, lists, trees and so on. It is closely | representations of boolean values, lists, trees and so on. It is closely | ||

connected to theorem proving, via | connected to theorem proving, via | ||

[http://en.wikipedia.org/wiki/Curry-Howard the Curry-Howard isomorphism]. | [http://en.wikipedia.org/wiki/Curry-Howard the Curry-Howard isomorphism]. | ||

− | A [http://okmij.org/ftp/Haskell/number-parameterized-types.html decimal representation] was put forward by [http://okmij.org/ftp/ Oleg Kiselyov] in [http://www.haskell.org/ | + | A [http://okmij.org/ftp/Haskell/number-parameterized-types.html decimal representation] was put forward by [http://okmij.org/ftp/ Oleg Kiselyov] in [http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Types "Number-Paramterized Types"] in the [http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5 fifth issue] of [http://themonadreader.wordpress.com/ The Monad Reader]. |

+ | There is an implementation in the {{HackagePackage|id=type-level}} package, but unfortunately the arithmetic is really slow, because in fact it simulates Peano arithmetic with decimal numbers. | ||

== Library support == | == Library support == | ||

Line 33: | Line 36: | ||

the order of 10^15 (at least). It also contains a test suite to help | the order of 10^15 (at least). It also contains a test suite to help | ||

validate the somewhat unintuitive algorithms. | validate the somewhat unintuitive algorithms. | ||

+ | |||

+ | More libraries: | ||

+ | |||

+ | * {{HackagePackage|id=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. | ||

+ | * {{HackagePackage|id=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. | ||

+ | * {{HackagePackage|id=type-level-natural-number}} and related packages. A collection of packages where the simplest one is even Haskell2010. | ||

+ | * {{HackagePackage|id=tfp}} Decimal representation, Type families, Template Haskell. | ||

+ | * {{HackagePackage|id=typical}} Binary numbers and functional dependencies. | ||

+ | * {{HackagePackage|id=type-unary}} Unary representation and type families. | ||

+ | * {{HackagePackage|id=numtype}}, {{HackagePackage|id=numtype-tf}} Unary representation and functional dependencies and type families, respectively. | ||

== More type hackery == | == More type hackery == | ||

Line 68: | Line 81: | ||

[http://www.cs.chalmers.se/~hallgren/Papers/wm01.html Fun with Functional Dependencies]. | [http://www.cs.chalmers.se/~hallgren/Papers/wm01.html Fun with Functional Dependencies]. | ||

+ | <haskell> | ||

module Sort where | module Sort where | ||

Line 176: | Line 190: | ||

listQSort :: QSort xs ys => xs -> ys | listQSort :: QSort xs ys => xs -> ys | ||

listQSort = const undefined | listQSort = const undefined | ||

+ | </haskell> | ||

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

+ | <haskell> | ||

> :t listQSort list1 | > :t listQSort list1 | ||

Cons | Cons | ||

(Succ Zero) | (Succ Zero) | ||

(Cons (Succ One) (Cons (Succ Two) (Cons (Succ Three) Nil))) | (Cons (Succ One) (Cons (Succ Two) (Cons (Succ Three) Nil))) | ||

+ | </haskell> | ||

− | = | + | == A Really Advanced Example : Type-Level Lambda Calculus == |

− | Again, thanks to Roman Leshchinskiy, we present | + | Again, thanks to Roman Leshchinskiy, we present a simple lambda calculus |

− | + | encoded in the type system (and with non-terminating typechecking fun!) | |

− | typechecking fun!) | + | |

Below is an example which encodes a stripped-down version of the lambda | Below is an example which encodes a stripped-down version of the lambda | ||

calculus (with only one variable): | calculus (with only one variable): | ||

+ | <haskell> | ||

{-# OPTIONS -fglasgow-exts #-} | {-# OPTIONS -fglasgow-exts #-} | ||

data X | data X | ||

Line 210: | Line 227: | ||

instance Eval (Lam t) (Lam t) | instance Eval (Lam t) (Lam t) | ||

instance (Eval s s', Apply s' t u) => Eval (App s t) u | instance (Eval s s', Apply s' t u) => Eval (App s t) u | ||

+ | </haskell> | ||

Now, lets evaluate some lambda expressions: | Now, lets evaluate some lambda expressions: | ||

+ | <haskell> | ||

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

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

+ | </haskell> | ||

Ok good, and: | Ok good, and: | ||

+ | <haskell> | ||

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

^CInterrupted. | ^CInterrupted. | ||

+ | </haskell> | ||

diverges ;) | diverges ;) | ||

+ | |||

+ | == Turing-completeness == | ||

+ | |||

+ | It's possible to embed the Turing-complete [[Type_SK|SK combinator calculus]] at the type level. | ||

+ | |||

+ | == Theory == | ||

+ | |||

+ | See also [[dependent type]] theory. | ||

+ | |||

+ | == Practice == | ||

+ | |||

+ | [[Extensible record]]s (which are used e.g. in type safe, declarative [[relational algebra]] approaches to [[Libraries and tools/Database interfaces|database management]]) | ||

[[Category:Idioms]] | [[Category:Idioms]] | ||

+ | [[Category:Mathematics]] | ||

+ | [[Category:Type-level programming]] |

## Revision as of 16:26, 19 July 2012

**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-Paramterized 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.

## Contents |

## 1 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.

## 2 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".

## 3 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.

## 4 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)))

## 5 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 ;)

## 6 Turing-completeness

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

## 7 Theory

See also dependent type theory.

## 8 Practice

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