型レベルクイックソート > :t qsort (n4 ~: n3 ~: n2 ~: n1 ~: Null) => (Cons N1 (Cons N2 (Cons N3 (Cons N4 Null))))

type-level-quicksort.hs

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
import Prelude

{- 数値の定義 -}
data Zero = Zero
data Succ a = Succ a

type N0 = Zero
type N1 = Succ N0
type N2 = Succ N1
type N3 = Succ N2
type N4 = Succ N3
type N5 = Succ N4
type N6 = Succ N5
type N7 = Succ N6
type N8 = Succ N7
type N9 = Succ N8
type N10 = Succ N9

n0 = undefined::N0
n1 = undefined::N1
n2 = undefined::N2
n3 = undefined::N3
n4 = undefined::N4
n5 = undefined::N5
n6 = undefined::N6
n7 = undefined::N7
n8 = undefined::N8
n9 = undefined::N9
n10 = undefined::N10

decl::Succ a->a
decl = const undefined

instance (Show a)=>Show (Succ a) where
    show = show . (+1) . read . show . decl

instance Show Zero where
    show _ = "0"

{- Add a b-}
class Add a b ab | a b -> ab
instance Add Zero b b
instance Add a b ab => Add (Succ a) b (Succ ab)

add::Add a b c => a -> b -> c
add = const undefined

{- Boolの定義 -}
data TTrue  = TTrue
data TFalse = TFalse

instance Show TTrue where
    show _ = "true"

instance Show TFalse where
    show _ = "false"

{- Equal a b -}
class Equal a b ab | a b -> ab
instance Equal Zero     Zero     TTrue
instance Equal Zero     (Succ b) TFalse
instance Equal (Succ a) Zero     TFalse
instance Equal a        b        ab     => Equal (Succ a) (Succ b) ab

equals::Equal a b ab=>a->b->ab
equals = const undefined

{- Not a -}
class Not a a' | a -> a'
instance Not TTrue  TFalse
instance Not TFalse TTrue

complement::Not a a'=>a->a'
complement = const undefined

{- And a b -}
class And a b ab | a b -> ab
instance And TTrue  TTrue  TTrue
instance And TFalse TTrue  TFalse
instance And TTrue  TFalse TFalse
instance And TFalse TFalse TFalse

tand::And a b ab=>a->b->ab
tand = const undefined

{- And a b -}
class Or a b ab | a b -> ab
instance Or TTrue  TTrue  TTrue
instance Or TFalse TTrue  TTrue
instance Or TTrue  TFalse TTrue
instance Or TFalse TFalse TFalse

tor::Or a b ab=>a->b->ab
tor = const undefined

{- Compareの定義 -}
data TGT = TGT
data TLT = TLT
data TEQ = TEQ

class Compare a b ab | a b -> ab
instance Compare Zero     Zero     TEQ
instance Compare Zero     (Succ b) TLT
instance Compare (Succ a) Zero     TGT
instance Compare a        b        ab  => Compare (Succ a) (Succ b) ab

instance Equal TEQ TEQ TTrue
instance Equal TEQ TLT TFalse
instance Equal TEQ TGT TFalse
instance Equal TLT TEQ TFalse
instance Equal TLT TLT TTrue
instance Equal TLT TGT TFalse
instance Equal TGT TEQ TFalse
instance Equal TGT TLT TFalse
instance Equal TGT TGT TTrue

cmp::Compare a b ab=>a->b->ab
cmp = const undefined

{- If a b c -}
class If a b c bc | a b c -> bc
instance If TTrue  b c b
instance If TFalse b c c

select::If a b c bc=>a->b->c->bc
select = const undefined

{- -}
data Null = Null
data Cons a b = Cons

thead::Cons a b->a
thead = const undefined

tlast::Cons a b->b
tlast = const undefined

instance (Show a, Show b)=>Show (Cons a b) where
    show x = ("(" ++ a ++ ", " ++ b ++ ")")
             where
               a = show $ thead $ x
               b = show $ tlast $x

instance Show Null where
    show _ = "[]"

infixr 5 ~:
(~:)::a->b->Cons a b
(~:) = const undefined

instance Equal Null        Null        TTrue
instance Equal Null        (Cons a b)  TFalse
instance Equal (Cons a b)  Null        TFalse
instance (Equal a b ab, Equal xa xb xab, And ab xab c)=>
    Equal (Cons a xa) (Cons b xb) c

{- concat -}
class Concat a b c | a b->c
instance Concat Null b b
instance Concat xa   b c => Concat (Cons a xa) b (Cons a c)

join::Concat a b c=>a->b->c
join = const undefined

{- qsort -}
class FilterLess a n r | a->r
instance FilterLess Null n Null
instance (FilterLess b n b', Compare a n cret, 
          Equal cret TLT eret, If eret (Cons a b') b' ret) =>
    FilterLess (Cons a b) n ret

class FilterGreater a n r | a->r
instance FilterGreater Null n Null
instance (FilterGreater b n b', Compare a n cret,
          Equal cret TGT eret, If eret (Cons a b') b' ret) =>
    FilterGreater (Cons a b) n ret

class Qsort a r | a->r
instance Qsort Null Null
instance (FilterLess b a l, FilterGreater b a r,
          Qsort l lsorted,  Qsort r rsorted,
          Concat (Cons a Null) rsorted tmp, Concat lsorted tmp ret)
    => Qsort (Cons a b) ret

qsort::Qsort a r=>a->r
qsort = const undefined