Difference between revisions of "Type arithmetic"
m (fix gmane links using archive.fo) 

(25 intermediate revisions by 11 users not shown)  
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]]: 
+  <haskell> 

data Zero 
data Zero 

Line 10:  Line 11:  
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 

+  balanced base tree. Typelevel 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/CurryHoward the CurryHoward isomorphism]. 

+  
+  A [http://okmij.org/ftp/Haskell/numberparameterizedtypes.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 "NumberParameterized 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 {{HackagePackageid=typelevel}} 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://archive.fo/77scn 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: 

+  
+  * {{HackagePackageid=typelevel}} 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. 

+  * {{HackagePackageid=typeleveltf}} Similar to the typelevel package (also in speed) but uses type families instead of functional dependencies and uses the same module names as the typelevel package. Thus module name clashes are warranted if you have to use both packages. 

+  * {{HackagePackageid=typelevelnaturalnumber}} and related packages. A collection of packages where the simplest one is even Haskell2010. 

+  * {{HackagePackageid=tfp}} Decimal representation, Type families, Template Haskell. 

+  * {{HackagePackageid=typical}} Binary numbers and functional dependencies. 

+  * {{HackagePackageid=typeunary}} Unary representation and type families. 

+  * {{HackagePackageid=numtype}}, {{HackagePackageid=numtypetf}} Unary representation and functional dependencies and type families, respectively. 

+  
+  == More type hackery == 

+  
+  Not to be outdone, Oleg Kiselyov has 

+  [http://archive.fo/JwMNI 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://archive.fo/4Ztai 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/CurryHoward the CurryHoward isomorphism] 

+  and then a decision procedure for Intuitionistic Propositional Calculus. 

+  
+  == 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 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 : TypeLevel Lambda Calculus == 

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

+  encoded in the type system (and with nonterminating typechecking fun!) 

+  
+  Below is an example which encodes a strippeddown version of the lambda 

+  calculus (with only one variable): 

+  
+  <haskell> 

+  {# OPTIONS fglasgowexts #} 

+  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 ;) 

+  
+  == Turingcompleteness == 

+  
+  It's possible to embed the Turingcomplete [[Type_SKSK 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 interfacesdatabase management]]) 

+  
+  [[Category:Idioms]] 

+  [[Category:Mathematics]] 

+  [[Category:Typelevel programming]] 
Latest revision as of 19:23, 15 August 2019
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 tree. 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.
A decimal representation was put forward by Oleg Kiselyov in "NumberParameterized Types" in the fifth issue of The Monad Reader. There is an implementation in the typelevel 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:
 typelevel 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.
 typeleveltf Similar to the typelevel package (also in speed) but uses type families instead of functional dependencies and uses the same module names as the typelevel package. Thus module name clashes are warranted if you have to use both packages.
 typelevelnaturalnumber 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.
 typeunary Unary representation and type families.
 numtype, numtypetf Unary representation and functional dependencies and type families, respectively.
More type hackery
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.
Djinn interprets a Haskell type as a logic formula using the CurryHoward isomorphism and then a decision procedure for Intuitionistic Propositional Calculus.
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 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 : TypeLevel Lambda Calculus
Again, thanks to Roman Leshchinskiy, we present a simple lambda calculus encoded in the type system (and with nonterminating typechecking fun!)
Below is an example which encodes a strippeddown version of the lambda calculus (with only one variable):
{# OPTIONS fglasgowexts #}
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 ;)
Turingcompleteness
It's possible to embed the Turingcomplete 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)