# Posted By

keigoi on 11/19/09

# Statistics

Viewed 289 times
Favorited by 1 user(s)

# recursive type representation in type level

`{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}{-# LANGUAGE FlexibleInstances #-}{-# LANGUAGE FlexibleContexts #-}{-# LANGUAGE UndecidableInstances #-}{-# LANGUAGE TypeFamilies #-}{-# LANGUAGE IncoherentInstances #-} -- TypeEq requires incoherent instances -- type-level booleandata T = Tdata F = F -- type-level type equalityclass TypeEq' () x y b => TypeEq x y b | x y -> b where  type'eq :: x -> y -> b  type'eq _ _ = undefined::bclass TypeEq' q x y b | q x y -> bclass TypeEq'' q x y b | q x y -> binstance TypeEq' () x y b => TypeEq x y binstance b ~ T => TypeEq' () x x binstance TypeEq'' q x y b => TypeEq' q x y binstance TypeEq'' () x y F -- recursion binder and variabledata Rec n u = Rec n u deriving Showdata Var n = Var n deriving Show -- foldingclass RecFold m u r | m u -> r  where fold' :: m -> u -> rinstance 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 -> rinstance RecFoldCont T m n a (Var m) where -- fold   fold'cont b m n a = Var minstance (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)  -- unfoldingclass RecUnfold m r s u | m r s -> u where  unfold' :: m -> r -> s -> uinstance (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 -> ainstance RecUnfoldCont T m m s (Rec m s) where -- unfold  unfoldCont _ m _ s = Rec m sinstance RecUnfoldCont F m n s (Var n) where -- do not unfold  unfoldCont _ _ n _ = Var n -- type level numeralsdata Z = Zdata S n = S ninstance Show Z where show _ = "Z"instance Show n => Show (S n) where show ~(S n) = "(S "++show n++")" -- assign a natural number to each binderclass RecNumbering n rinstance (RecNumbering (S n) u1, m ~ n) => RecNumbering n (Rec m u1) whereinstance RecNumbering n (Var m) num :: RecNumbering (S Z) r => Rec Z r -> Rec Z rnum = id rec :: (RecFold n u r, RecUnfold n r r u) => u -> Rec n r -- RecUnfold ensures that our fold/unfold is isomorphicrec x = (\n -> Rec n (fold' n x)) undefined unfold :: (RecFold m u r, RecUnfold m r r u) => Rec m r -> uunfold (Rec m r) = unfold' m r r  -- å†å¸°ã•ã›ãŸã„åž‹data A x = A x deriving Showdata B x = B x deriving Showdata C x y = C x y deriving ShowunA (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))))))`