# Difference between revisions of "Type arithmetic"

DonStewart (talk | contribs) m (Mention Curry-Howard is behind Djinn) |
m (fix gmane links using archive.fo) |
||

(19 intermediate revisions by 9 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]. |
||

− | 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-Parameterized 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 == |
||

Robert Dockins has gone as far as to write |
Robert Dockins has gone as far as to write |
||

− | a [http:// |
+ | a [http://archive.fo/77scn library] |

for type level arithmetic, supporting the following operations on type |
for type level arithmetic, supporting the following operations on type |
||

level naturals: addition, subtraction, multiplication, division, |
level naturals: addition, subtraction, multiplication, division, |
||

Line 32: | Line 34: | ||

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 == |
||

Not to be outdone, Oleg Kiselyov has |
Not to be outdone, Oleg Kiselyov has |
||

− | [http:// |
+ | [http://archive.fo/JwMNI written] |

on invertible, terminating, 3-place addition, multiplication, |
on invertible, terminating, 3-place addition, multiplication, |
||

exponentiation relations on type-level Peano numerals, where any two |
exponentiation relations on type-level Peano numerals, where any two |
||

Line 50: | Line 62: | ||

Somewhat related is Lennart Augustsson's tool |
Somewhat related is Lennart Augustsson's tool |
||

− | [http:// |
+ | [http://archive.fo/4Ztai Djinn], a theorem |

prover/coding wizard, that generates Haskell code from a given Haskell |
prover/coding wizard, that generates Haskell code from a given Haskell |
||

type declaration. |
type declaration. |
||

Line 64: | Line 76: | ||

Here is a complete example of advanced type level computation, kindly |
Here is a complete example of advanced type level computation, kindly |
||

provided by Roman Leshchinskiy. For further information consult Thomas |
provided by Roman Leshchinskiy. For further information consult Thomas |
||

− | Hallgren's |
+ | Hallgren's 2001 paper |

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

+ | <haskell> |
||

module Sort where |
module Sort where |
||

Line 174: | Line 187: | ||

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> |
||

− | / _ \ /\ /\/ __(_) |
||

⚫ | |||

− | / /_\// /_/ / / | | GHC Interactive, version 5.04, for Haskell 98. |
||

− | / /_\\/ __ / /___| | http://www.haskell.org/ghc/ |
||

− | \____/\/ /_/\____/|_| Type :? for help. |
||

− | |||

− | Loading package base ... linking ... done. |
||

− | Loading package haskell98 ... linking ... done. |
||

− | Prelude> :l Sort |
||

− | Compiling Sort ( Sort.hs, interpreted ) |
||

− | Ok, modules loaded: Sort. |
||

⚫ | |||

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 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): |
||

+ | |||

+ | <haskell> |
||

+ | {-# 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 |
||

+ | </haskell> |
||

+ | |||

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

+ | |||

+ | <haskell> |
||

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

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

+ | </haskell> |
||

+ | |||

+ | Ok good, and: |
||

+ | |||

+ | <haskell> |
||

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

+ | ^CInterrupted. |
||

+ | </haskell> |
||

+ | |||

+ | 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]] |

## Latest revision as of 19:23, 15 August 2019

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

## Contents

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