Collatz in Type Level
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

80 lines
1.6KB

  1. {-# OPTIONS_GHC -fno-warn-missing-methods #-}
  2. {-# LANGUAGE MultiParamTypeClasses #-}
  3. {-# LANGUAGE FunctionalDependencies #-}
  4. {-# LANGUAGE FlexibleInstances #-}
  5. {-# LANGUAGE UndecidableInstances #-}
  6. nil = undefined
  7. data True
  8. data False
  9. data S n
  10. data Z
  11. data Nil
  12. data Cons h t
  13. class Equal a b t | a b -> t
  14. instance Equal Z Z True
  15. instance Equal (S a) Z False
  16. instance Equal Z (S b) False
  17. instance (Equal a b t)
  18. => Equal (S a) (S b) t
  19. class Add x y r | x y -> r
  20. instance Add x Z x
  21. instance (Add (S x) n r)
  22. => Add x (S n) r
  23. class Mul x y a r | x y a -> r
  24. instance Mul x Z a a
  25. instance Mul Z y a a
  26. instance (Add x a n, Mul x y n t)
  27. => Mul x (S y) a t
  28. class Half x a r | x a -> r
  29. instance Half Z a a
  30. instance Half (S Z) a a
  31. instance (Half n (S a) r)
  32. => Half (S (S n)) a r
  33. class ThreeEnPlusOne x v | x -> v
  34. instance (Mul (S (S (S Z))) x Z i)
  35. => ThreeEnPlusOne x (S i)
  36. class EqOne x r | x -> r
  37. instance (Equal x (S Z) b)
  38. => EqOne x b
  39. class IsEven a b | a -> b
  40. instance IsEven Z True
  41. instance IsEven (S Z) False
  42. instance (IsEven n r)
  43. => IsEven (S (S n)) r
  44. class Branch b h n | b h -> n
  45. instance (Half h Z r)
  46. => Branch True h r
  47. instance (ThreeEnPlusOne h r)
  48. => Branch False h r
  49. class RunChain b h t r | b h t -> r
  50. instance RunChain True h xs xs
  51. instance ( IsEven h e
  52. , EqOne h b
  53. , Branch e h v
  54. , RunChain b v (Cons h t) r
  55. )
  56. => RunChain False h t r
  57. class Reverse i l r | i l -> r
  58. instance Reverse i Nil i
  59. instance (Reverse (Cons x i) xs r)
  60. => Reverse i (Cons x xs) r
  61. class Solution n r | n -> r
  62. where solution :: n -> r
  63. instance (RunChain False n Nil o, Reverse Nil o a)
  64. => Solution n a where solution = nil