/ Published in: Haskell

Expand |
Embed | Plain Text

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, FlexibleInstances, OverlappingInstances #-} 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 = 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

## Comments

Subscribe to commentsYou need to login to post a comment.

great!!! very good instance of type-level programming in Haskell.