Personal tools

Type arithmetic

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(Changed Monad.Reader link refs.)
(22 intermediate revisions by 8 users not shown)
Line 1: Line 1:
'''Type arithmetic''' is calculations on types using fundeps as functions.
+
'''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 is [[Peano numbers]]:
+
A simple example of type-level computation are operations on [[Peano numbers]]:
  
 +
<haskell>
 
  data Zero
 
  data Zero
  
Line 10: 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>
  
However, many other representations of numbers are possible, including binary and balanced base three. Type arithmetic may also include type representations of boolean values and so on.
+
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
 +
[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/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 ==
 +
 
 +
Robert Dockins has gone as far as to write
 +
a [http://article.gmane.org/gmane.comp.lang.haskell.general/13206 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:
 +
 
 +
* {{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 ==
 +
 
 +
Not to be outdone, Oleg Kiselyov has
 +
[http://article.gmane.org/gmane.comp.lang.haskell.general/13223 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
 +
[http://article.gmane.org/gmane.comp.lang.haskell.general/12747 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
 +
[http://en.wikipedia.org/wiki/Curry-Howard 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
 +
[http://www.cs.chalmers.se/~hallgren/Papers/wm01.html Fun with Functional Dependencies].
 +
 
 +
<haskell>
 +
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
 +
</haskell>
 +
 
 +
And we need to be able to run this somehow, in the typechecker. So fire up ghci:
 +
 
 +
<haskell>
 +
> :t listQSort list1
 +
Cons
 +
    (Succ Zero)
 +
    (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]]

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)