Difference between revisions of "Type arithmetic"
DonStewart (talk  contribs) (Extend type arithmetic page with full example of typelevel quicksort) 
DonStewart (talk  contribs) (Talk about the various libraries for typelevel computation in Haskell) 

Line 1:  Line 1:  
−  '''Type arithmetic''' 
+  '''Type arithmetic''' (or typelevel computation) are calculations on 
+  the typelevel, often implemented in Haskell using functional 

+  dependencies to represent functions. 

−  A simple example 
+  A simple example of typelevel computation are operations on [[Peano numbers]]: 
data Zero 
data Zero 

Line 11:  Line 11:  
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. Typelevel computation may also include type 

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

+  connected to theorem proving, via the CurryHoward 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, 3place addition, multiplication, 

+  exponentiation relations on typelevel 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 nbase discrete logarithm, nth root, and the 

+  inverse of factorial. The inverting method can work with any 

+  representation of (typelevel) 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 : TypeLevel Quicksort == 
== An Advanced Example : TypeLevel Quicksort == 
Revision as of 06:57, 16 February 2006
Type arithmetic (or typelevel computation) are calculations on the typelevel, often implemented in Haskell using functional dependencies to represent functions.
A simple example of typelevel 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. Typelevel computation may also include type representations of boolean values, lists, trees and so on. It is closely connected to theorem proving, via the CurryHoward 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, 3place addition, multiplication, exponentiation relations on typelevel 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 nbase discrete logarithm, nth root, and the inverse of factorial. The inverting method can work with any representation of (typelevel) 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 : TypeLevel 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)))