Posted By

eagletmt on 08/27/09


Tagged


Versions (?)

Who likes this?

1 person have marked this snippet as a favorite

keigoi


merge sort


 / Published in: Haskell
 

  1. {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, FlexibleInstances, OverlappingInstances #-}
  2.  
  3. data Zero = Zero
  4. data Succ n = Succ n
  5. data Yes = Yes
  6. data No = No
  7. data Nil = Nil
  8. data Cons x xs = Cons
  9.  
  10.  
  11. -- (<=)
  12. class Lte a b c | a b -> c where
  13. lte :: a -> b -> c
  14. lte = u
  15. instance Lte Zero b Yes
  16. instance Lte (Succ n) Zero No
  17. instance Lte a b c => Lte (Succ a) (Succ b) c
  18.  
  19. class Merge xs ys zs | xs ys -> zs where
  20. merge :: xs -> ys -> zs
  21. merge = u
  22. instance Merge xs Nil xs
  23. instance Merge Nil ys ys
  24. instance (Lte x y b, Merge' b x y xs ys r) => Merge (Cons x xs) (Cons y ys) r
  25. -- merge (Cons x xs) (Cons y ys) = merge' (x <= y) x y xs ys
  26. class Merge' b x y xs ys r | b x y xs ys -> r
  27. instance Merge xs (Cons y ys) zs => Merge' Yes x y xs ys (Cons x zs)
  28. instance Merge (Cons x xs) ys zs => Merge' No x y xs ys (Cons y zs)
  29. -- merge' Yes x y xs ys = Cons x (merge xs (Cons y ys))
  30. -- merge' No x y xs ys = Cons y (merge (Cons x xs) ys)
  31.  
  32. class Sort xs ys | xs -> ys where
  33. sort :: xs -> ys
  34. sort = u
  35. instance Sort Nil Nil
  36. instance Sort (Cons x Nil) (Cons x Nil)
  37. instance (Split xs ys zs, Sort ys ys', Sort zs zs', Merge ys' zs' r) => Sort xs r
  38. -- sort Nil = Nil
  39. -- sort (Cons x Nil) = Cons x Nil
  40. -- sort xs = let (ys,zs) = split xs in merge (sort ys) (sort zs)
  41.  
  42. class Length xs n | xs -> n where
  43. length :: xs -> n
  44. length = u
  45. instance Length Nil Zero
  46. instance Length xs n => Length (Cons x xs) (Succ n)
  47.  
  48. class Split xs zs ws | xs -> zs ws where
  49. instance Split' Nil xs zs ws => Split xs zs ws
  50. -- split xs = split' Nil xs
  51.  
  52. class Split' xs ys zs ws | xs ys -> zs ws
  53. instance (Length xs n, Length ys m, Lte m n b, Split'' b xs ys zs ws) => Split' xs ys zs ws
  54. -- split' xs ys = split'' (length ys <= length xs) xs ys
  55.  
  56. class Split'' b xs ys zs ws | b xs ys -> zs ws where
  57. instance Split'' Yes xs ys xs ys
  58. instance Split' (Cons y xs) ys zs ws => Split'' No xs (Cons y ys) zs ws
  59. -- split'' Yes xs ys = xs ys
  60. -- split'' No xs (Cons y ys) = split' (Cons y xs) ys
  61.  
  62. type One = Succ Zero
  63. one :: One
  64. one = u
  65. type Two = Succ One
  66. two :: Two
  67. two = u
  68. type Three = Succ Two
  69. three :: Three
  70. three = u
  71. type Four = Succ Three
  72. four :: Four
  73. four = u
  74.  
  75. ls :: Cons Four (Cons Two (Cons Three (Cons One Nil)))
  76. ls = u
  77.  
  78. ok :: Cons One (Cons Two (Cons Three (Cons Four Nil))) -> String
  79. ok = const "ok"
  80.  
  81. main = putStrLn $ ok $ sort ls

Report this snippet  

Comments

RSS Icon Subscribe to comments
Posted By: keigoi on August 27, 2009

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

You need to login to post a comment.