Difference between revisions of "Type arithmetic"
Jump to navigation
Jump to search
DonStewart (talk | contribs) (Extend type arithmetic page with full example of type-level quicksort) |
|||
Line 12: | Line 12: | ||
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. |
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. |
||
+ | |||
+ | == 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))) |
||
[[Category:Idioms]] |
[[Category:Idioms]] |
Revision as of 06:26, 16 February 2006
Type arithmetic is calculations on types using fundeps as functions.
A simple example is 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)
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.
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)))