merge sort

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, FlexibleInstances, OverlappingInstances #-}
import Prelude (undefined,String,const,putStrLn,($))
 
data Zero = Zero
data Succ n = Succ n
data Yes = Yes
data No = No
data Nil = Nil
data Cons x xs = Cons
 
u = undefined
 
-- (<=)
class Lte a b c | a b -> c where
  lte :: a -> b -> c
  lte = u
instance Lte Zero b Yes
instance Lte (Succ n) Zero No
instance Lte a b c => Lte (Succ a) (Succ b) c
 
class Merge xs ys zs | xs ys -> zs where
  merge :: xs -> ys -> zs
  merge = u
instance Merge xs Nil xs
instance Merge Nil ys ys
instance (Lte x y b, Merge' b x y xs ys r) => Merge (Cons x xs) (Cons y ys) r
-- merge (Cons x xs) (Cons y ys) = merge' (x <= y) x y xs ys
class Merge' b x y xs ys r | b x y xs ys -> r
instance Merge xs (Cons y ys) zs => Merge' Yes x y xs ys (Cons x zs)
instance Merge (Cons x xs) ys zs => Merge' No  x y xs ys (Cons y zs)
-- merge' Yes x y xs ys = Cons x (merge xs (Cons y ys))
-- merge' No  x y xs ys = Cons y (merge (Cons x xs) ys)
 
class Sort xs ys | xs -> ys where
  sort :: xs -> ys
  sort = u
instance Sort Nil Nil
instance Sort (Cons x Nil) (Cons x Nil)
instance (Split xs ys zs, Sort ys ys', Sort zs zs', Merge ys' zs' r) => Sort xs r
-- sort Nil = Nil
-- sort (Cons x Nil) = Cons x Nil
-- sort xs = let (ys,zs) = split xs in merge (sort ys) (sort zs)
 
class Length xs n | xs -> n where
  length :: xs -> n
  length = u
instance Length Nil Zero
instance Length xs n => Length (Cons x xs) (Succ n)
 
class Split xs zs ws | xs -> zs ws where
instance Split' Nil xs zs ws => Split xs zs ws
-- split xs = split' Nil xs
 
class Split' xs ys zs ws | xs ys -> zs ws
instance (Length xs n, Length ys m, Lte m n b, Split'' b xs ys zs ws) => Split' xs ys zs ws
-- split' xs ys = split'' (length ys <= length xs) xs ys
 
class Split'' b xs ys zs ws | b xs ys -> zs ws where
instance Split'' Yes xs ys xs ys
instance Split' (Cons y xs) ys zs ws => Split'' No xs (Cons y ys) zs ws
-- split'' Yes xs ys = xs ys
-- split'' No  xs (Cons y ys) = split' (Cons y xs) ys
 
type One = Succ Zero
one :: One
one = u
type Two = Succ One
two :: Two
two = u
type Three = Succ Two
three :: Three
three = u
type Four = Succ Three
four :: Four
four = u
 
ls :: Cons Four (Cons Two (Cons Three (Cons One Nil)))
ls = u
 
ok :: Cons One (Cons Two (Cons Three (Cons Four Nil))) -> String
ok = const "ok"
 
main = putStrLn $ ok $ sort ls