Posted By

keigoi on 11/19/09


Tagged

haskell typelevel typeclass fundeps


Versions (?)

Who likes this?

1 person have marked this snippet as a favorite

keigoi


recursive type representation in type level


 / Published in: Haskell
 

  1. {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
  2. {-# LANGUAGE FlexibleInstances #-}
  3. {-# LANGUAGE FlexibleContexts #-}
  4. {-# LANGUAGE UndecidableInstances #-}
  5. {-# LANGUAGE TypeFamilies #-}
  6. {-# LANGUAGE IncoherentInstances #-} -- TypeEq requires incoherent instances
  7.  
  8. -- type-level boolean
  9. data T = T
  10. data F = F
  11.  
  12. -- type-level type equality
  13. class TypeEq' () x y b => TypeEq x y b | x y -> b where
  14. type'eq :: x -> y -> b
  15. type'eq _ _ = undefined::b
  16. class TypeEq' q x y b | q x y -> b
  17. class TypeEq'' q x y b | q x y -> b
  18. instance TypeEq' () x y b => TypeEq x y b
  19. instance b ~ T => TypeEq' () x x b
  20. instance TypeEq'' q x y b => TypeEq' q x y b
  21. instance TypeEq'' () x y F
  22.  
  23. -- recursion binder and variable
  24. data Rec n u = Rec n u deriving Show
  25. data Var n = Var n deriving Show
  26.  
  27. -- folding
  28. class RecFold m u r | m u -> r where fold' :: m -> u -> r
  29. instance RecFold m (Var n) (Var n) where fold' _ v = v
  30. instance (TypeEq m n b, RecFoldCont b m n a r) => RecFold m (Rec n a) r where -- fold if m = n
  31. fold' m (Rec n a) = fold'cont (type'eq m n) m n a
  32.  
  33. class RecFoldCont b m n a r | b m n a -> r where
  34. fold'cont :: b -> m -> n -> a -> r
  35. instance RecFoldCont T m n a (Var m) where -- fold
  36. fold'cont b m n a = Var m
  37. instance (RecFold m a r)
  38. => RecFoldCont F m n a (Rec n r) where -- do not fold
  39. fold'cont b m n a = Rec n (fold' m a)
  40.  
  41.  
  42. -- unfolding
  43. class RecUnfold m r s u | m r s -> u where
  44. unfold' :: m -> r -> s -> u
  45. instance (RecFold n s s', RecUnfold m a s' a') => RecUnfold m (Rec n a) s (Rec n a') where
  46. unfold' m (Rec n a) s = Rec n (unfold' m a (fold' n s))
  47. instance (TypeEq m n b, RecUnfoldCont b m n s a) => RecUnfold m (Var n) s a where -- unfold if m = n
  48. unfold' m (Var n) s = unfoldCont (type'eq m n) m n s
  49.  
  50. class RecUnfoldCont b m n s a | b m n s -> a where
  51. unfoldCont :: b -> m -> n -> s -> a
  52. instance RecUnfoldCont T m m s (Rec m s) where -- unfold
  53. unfoldCont _ m _ s = Rec m s
  54. instance RecUnfoldCont F m n s (Var n) where -- do not unfold
  55. unfoldCont _ _ n _ = Var n
  56.  
  57. -- type level numerals
  58. data Z = Z
  59. data S n = S n
  60. instance Show Z where show _ = "Z"
  61. instance Show n => Show (S n) where show ~(S n) = "(S "++show n++")"
  62.  
  63. -- assign a natural number to each binder
  64. class RecNumbering n r
  65. instance (RecNumbering (S n) u1, m ~ n) => RecNumbering n (Rec m u1) where
  66. instance RecNumbering n (Var m)
  67.  
  68. num :: RecNumbering (S Z) r => Rec Z r -> Rec Z r
  69. num = id
  70.  
  71. rec :: (RecFold n u r, RecUnfold n r r u) => u -> Rec n r -- RecUnfold ensures that our fold/unfold is isomorphic
  72. rec x = (\n -> Rec n (fold' n x)) undefined
  73.  
  74. unfold :: (RecFold m u r, RecUnfold m r r u) => Rec m r -> u
  75. unfold (Rec m r) = unfold' m r r
  76.  
  77. -- 再帰させたい型
  78. data A x = A x deriving Show
  79. data B x = B x deriving Show
  80. data C x y = C x y deriving Show
  81. unA (A x) = x; unB (B x) = x; unC1 (C x _) = x; unC2 (C _ y) = y
  82.  
  83. instance RecFold m x x' => RecFold m (A x) (A x') where
  84. fold' m (A x) = A (fold' m x)
  85. instance RecFold m x x' => RecFold m (B x) (B x') where
  86. fold' m (B x) = B (fold' m x)
  87. instance (RecFold m x x', RecFold m y y') => RecFold m (C x y) (C x' y') where
  88. fold' m (C x y) = C (fold' m x) (fold' m y)
  89. instance RecUnfold m u s u' => RecUnfold m (A u) s (A u') where
  90. unfold' m (A u) s = A (unfold' m u s)
  91. instance RecUnfold m u s u' => RecUnfold m (B u) s (B u') where
  92. unfold' m (B u) s = B (unfold' m u s)
  93. instance (RecUnfold m u s u', RecUnfold m v s v') => RecUnfold m (C u v) s (C u' v') where
  94. unfold' m (C u v) s = C (unfold' m u s) (unfold' m v s)
  95. instance RecNumbering n u => RecNumbering n (A u)
  96. instance RecNumbering n u => RecNumbering n (B u)
  97. instance (RecNumbering n u, RecNumbering n v) => RecNumbering n (C u v)
  98.  
  99.  
  100.  
  101. -- *Main> let x = rec (A y) ; y = rec (B (C x y)); _ = num x
  102. -- *Main> :t x
  103. -- x :: Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))
  104. -- *Main> x
  105. -- Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))
  106. --
  107. -- *Main> unfold x
  108. -- A (Rec (S Z) (B (C (Rec Z (A (Var (S Z)))) (Var (S Z)))))
  109. -- *Main> :t unfold x
  110. -- unfold x
  111. -- :: A (Rec (S Z) (B (C (Rec Z (A (Var (S Z)))) (Var (S Z)))))
  112. --
  113. -- *Main> unC1 $ unB $ unfold $ unA $ unfold x
  114. -- Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))
  115. -- *Main> :t unC1 $ unB $ unfold $ unA $ unfold x
  116. -- unC1 $ unB $ unfold $ unA $ unfold x
  117. -- :: Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))

Report this snippet  

You need to login to post a comment.