Personal tools

Type arithmetic

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(Extend type arithmetic page with full example of type-level quicksort)
(Talk about the various libraries for type-level computation in Haskell)
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]]:
  
 
  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)
  
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 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.

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

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

2 Djinn

Somewhat related is Lennart Augustsson's tool Djinn, a theorem prover/coding wizard, that generates Haskell code from a given Haskell type declaration.

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