Revision: 20572
Initial Code
Initial URL
Initial Description
Initial Title
Initial Tags
Initial Language
at November 19, 2009 10:38 by keigoi
Initial Code
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE IncoherentInstances #-} -- TypeEq requires incoherent instances -- type-level boolean data T = T data F = F -- type-level type equality class TypeEq' () x y b => TypeEq x y b | x y -> b where type'eq :: x -> y -> b type'eq _ _ = undefined::b class TypeEq' q x y b | q x y -> b class TypeEq'' q x y b | q x y -> b instance TypeEq' () x y b => TypeEq x y b instance b ~ T => TypeEq' () x x b instance TypeEq'' q x y b => TypeEq' q x y b instance TypeEq'' () x y F -- recursion binder and variable data Rec n u = Rec n u deriving Show data Var n = Var n deriving Show -- folding class RecFold m u r | m u -> r where fold' :: m -> u -> r instance RecFold m (Var n) (Var n) where fold' _ v = v instance (TypeEq m n b, RecFoldCont b m n a r) => RecFold m (Rec n a) r where -- fold if m = n fold' m (Rec n a) = fold'cont (type'eq m n) m n a class RecFoldCont b m n a r | b m n a -> r where fold'cont :: b -> m -> n -> a -> r instance RecFoldCont T m n a (Var m) where -- fold fold'cont b m n a = Var m instance (RecFold m a r) => RecFoldCont F m n a (Rec n r) where -- do not fold fold'cont b m n a = Rec n (fold' m a) -- unfolding class RecUnfold m r s u | m r s -> u where unfold' :: m -> r -> s -> u instance (RecFold n s s', RecUnfold m a s' a') => RecUnfold m (Rec n a) s (Rec n a') where unfold' m (Rec n a) s = Rec n (unfold' m a (fold' n s)) instance (TypeEq m n b, RecUnfoldCont b m n s a) => RecUnfold m (Var n) s a where -- unfold if m = n unfold' m (Var n) s = unfoldCont (type'eq m n) m n s class RecUnfoldCont b m n s a | b m n s -> a where unfoldCont :: b -> m -> n -> s -> a instance RecUnfoldCont T m m s (Rec m s) where -- unfold unfoldCont _ m _ s = Rec m s instance RecUnfoldCont F m n s (Var n) where -- do not unfold unfoldCont _ _ n _ = Var n -- type level numerals data Z = Z data S n = S n instance Show Z where show _ = "Z" instance Show n => Show (S n) where show ~(S n) = "(S "++show n++")" -- assign a natural number to each binder class RecNumbering n r instance (RecNumbering (S n) u1, m ~ n) => RecNumbering n (Rec m u1) where instance RecNumbering n (Var m) num :: RecNumbering (S Z) r => Rec Z r -> Rec Z r num = id rec :: (RecFold n u r, RecUnfold n r r u) => u -> Rec n r -- RecUnfold ensures that our fold/unfold is isomorphic rec x = (\n -> Rec n (fold' n x)) undefined unfold :: (RecFold m u r, RecUnfold m r r u) => Rec m r -> u unfold (Rec m r) = unfold' m r r -- å†å¸°ã•ã›ãŸã„åž‹ data A x = A x deriving Show data B x = B x deriving Show data C x y = C x y deriving Show unA (A x) = x; unB (B x) = x; unC1 (C x _) = x; unC2 (C _ y) = y instance RecFold m x x' => RecFold m (A x) (A x') where fold' m (A x) = A (fold' m x) instance RecFold m x x' => RecFold m (B x) (B x') where fold' m (B x) = B (fold' m x) instance (RecFold m x x', RecFold m y y') => RecFold m (C x y) (C x' y') where fold' m (C x y) = C (fold' m x) (fold' m y) instance RecUnfold m u s u' => RecUnfold m (A u) s (A u') where unfold' m (A u) s = A (unfold' m u s) instance RecUnfold m u s u' => RecUnfold m (B u) s (B u') where unfold' m (B u) s = B (unfold' m u s) instance (RecUnfold m u s u', RecUnfold m v s v') => RecUnfold m (C u v) s (C u' v') where unfold' m (C u v) s = C (unfold' m u s) (unfold' m v s) instance RecNumbering n u => RecNumbering n (A u) instance RecNumbering n u => RecNumbering n (B u) instance (RecNumbering n u, RecNumbering n v) => RecNumbering n (C u v) -- *Main> let x = rec (A y) ; y = rec (B (C x y)); _ = num x -- *Main> :t x -- x :: Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z)))))) -- *Main> x -- Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z)))))) -- -- *Main> unfold x -- A (Rec (S Z) (B (C (Rec Z (A (Var (S Z)))) (Var (S Z))))) -- *Main> :t unfold x -- unfold x -- :: A (Rec (S Z) (B (C (Rec Z (A (Var (S Z)))) (Var (S Z))))) -- -- *Main> unC1 $ unB $ unfold $ unA $ unfold x -- Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z)))))) -- *Main> :t unC1 $ unB $ unfold $ unA $ unfold x -- unC1 $ unB $ unfold $ unA $ unfold x -- :: Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))
Initial URL
Initial Description
Initial Title
recursive type representation in type level
Initial Tags
Initial Language
Haskell