Difference between revisions of "Type arithmetic"
DonStewart (talk | contribs) (Extend type arithmetic page with full example of type-level quicksort) |
DonStewart (talk | contribs) (Talk about the various libraries for type-level computation in Haskell) |
||
Line 1: | Line 1: | ||
− | '''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 |
+ | A simple example of type-level computation are operations on [[Peano numbers]]: |
data Zero |
data Zero |
||
Line 11: | Line 13: | ||
instance (Add a b ab) => Add (Succ a) b (Succ ab) |
instance (Add a b ab) => Add (Succ a) b (Succ ab) |
||
− | + | Many other representations of numbers are possible, including binary and |
|
+ | balanced base three. 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. |
||
+ | |||
+ | == 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 |
||
+ | # < |
||
+ | # > |
||
+ | # <= |
||
+ | # >= |
||
+ | |||
+ | 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. |
||
+ | |||
+ | 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. |
||
== An Advanced Example : Type-Level Quicksort == |
== An Advanced Example : Type-Level Quicksort == |
Revision as of 06:57, 16 February 2006
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 three. 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.
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 # < # > # <= # >=
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.
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.
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 2000 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:
___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | 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. *Sort> :t listQSort list1 Cons (Succ Zero) (Cons (Succ One) (Cons (Succ Two) (Cons (Succ Three) Nil)))