quicksort algorithm implemented in the Purity language, see http://typesandotherdistractions.com/

quicksort.p

# empty and unit types

type (Void,,,) = lfix id
type (Unit,MakeUnit,) = Void -> Void
data Unique = MakeUnit id

# natural number type

type (Nat,MakeNat,UnmakeNat,FoldNat) = lfix const Unit + id

data Zero = MakeNat . inl Unique
data Succ = MakeNat . inr
data Pred = <const Zero, id> . UnmakeNat
data Add = FoldNat <const id, f => $f . Succ>

# generic list type

type (List A?,MakeList,UnmakeList,FoldList) = lfix const Unit + const A? . id

data Empty = MakeList . inl Unique
data Cons = curry MakeList . inr

# boolean type

type (Bool,MakeBool,UnmakeBool) = Unit + Unit
data True = MakeBool (inl Unique)
data False = MakeBool (inr Unique)
data IfThenElse = b => t => f => <const $t, const $f> . UnmakeBool $b

# a comparator compares pairs of values

type (Comparator A?,MakeComparator,Compare) = A? -> A? -> Bool

# a comparator for natural numbers

data Leq = MakeComparator (FoldNat <const (<const True, const False> . UnmakeNat), f => $f . Pred>)

# concatenate two lists

data Concat = FoldList <const id, uncurry (x => f => (Cons $x) . $f)>

# split a list into the list of elements less than x and the list greater than x

data Split = c => x => FoldList
                     <
                        (const Empty, const Empty), 
                        uncurry (
                           next => ls => 
                             IfThenElse (Compare $c $x $next)
                               ((curry id) (Cons $next (outl $ls)) (outr $ls))
                               ((curry id) (outl $ls) (Cons $next (outr $ls)))
                        )
                     >

# the quicksort algorithm

data Quicksort = c => FoldList
                    <
                       const Empty, 
                       uncurry (x => 
                          (ls => Concat (outl $ls) (Cons $x (outr $ls))) . (Split $c $x)
                       )
                    >