Type arithmetic

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