module Data.Yoko.Representation
(
Void(..), N(..), (:+:)(..),
C(..),
U(..), (:*:)(..),
T0(..), T1(..), T2(..), Variety(..),
Par1(..), Par0(..),
Rep, Generic(..),
unC, foldC, mapC,
WN(..),
unN0, foldN0, mapN0,
unN1, foldN1, mapN1,
unN2, foldN2, mapN2,
foldPlus, FoldPlusW'(..), mapPlus,
foldTimes, mapTimes,
unT0, mapT0,
unT1, mapT1,
unT2, mapT2,
unPar0, mapPar0,
unPar1, mapPar1,
DistMaybePlus
) where
import Data.Yoko.W
import Data.Yoko.TypeBasics
data Variety = Rec Nat | Dep
newtype C dc r (p1 :: *) (p0 :: *) = C (r p1 p0)
data U (p1 :: *) (p0 :: *) = U
infixr 6 :*:
data (:*:) a b (p1 :: *) (p0 :: *) = a p1 p0 :*: b p1 p0
data Void (p1 :: *) (p0 :: *)
data family N (dc :: k) :: * -> * -> *
newtype instance N dc (p1 :: *) (p0 :: *) = N0 dc
newtype instance N dc (p1 :: *) (p0 :: *) = N1 (dc p0)
newtype instance N dc (p1 :: *) (p0 :: *) = N2 (dc p1 p0)
infixl 6 :+:
data (:+:) a b (p1 :: *) (p0 :: *) = L (a p1 p0) | R (b p1 p0) deriving (Eq, Show, Ord, Read)
newtype Par1 (p1 :: *) (p0 :: *) = Par1 p1
newtype Par0 (p1 :: *) (p0 :: *) = Par0 p0
newtype T0 (v :: Variety) t (p1 :: *) (p0 :: *) = T0 t
newtype T1 (v :: Variety) (t :: * -> *) a (p1 :: *) (p0 :: *) = T1 (t (a p1 p0))
newtype T2 (v :: Variety) (t :: * -> * -> *) b a (p1 :: *) (p0 :: *) = T2 (t (b p1 p0) (a p1 p0))
type family Rep (t :: k) :: * -> * -> *
class Generic dc where
rep :: W dc (Rep dc) p1 p0; obj :: W' dc (Rep dc) p1 p0
class ComposeW dc => WN dc where
nN :: W dc (N dc) p1 p0
unN :: W' dc (N dc) p1 p0
instance WN (dc :: *) where nN = W0 N0; unN = W'0 unN0
instance WN (dc :: * -> *) where nN = W1 N1; unN = W'1 unN1
instance WN (dc :: * -> * -> *) where nN = W2 N2; unN = W'2 unN2
unT0 (T0 x) = x
mapT0 f (T0 x) = T0 (f x)
unT1 (T1 x) = x
mapT1 f (T1 x) = T1 (f x)
unT2 (T2 x) = x
mapT2 f (T2 x) = T2 (f x)
unPar0 (Par0 x) = x
mapPar0 f (Par0 x) = Par0 (f x)
unPar1 (Par1 x) = x
mapPar1 f (Par1 x) = Par1 (f x)
unC (C x) = x
foldC f = f . unC
mapC f = foldC (C . f)
unN0 (N0 x) = x
foldN0 f = f . unN0
unN1 (N1 x) = x
foldN1 f = f . unN1
unN2 (N2 x) = x
foldN2 f = f . unN2
mapN0 f = N0 . foldN0 f
mapN1 f = N1 . foldN1 f
mapN2 f = N2 . foldN2 f
foldPlus f g x = case x of
L x -> f x ; R x -> g x
class FoldPlusW' (s :: k) where
foldPlusW' :: W' s l p1 p0 -> W' s r p1 p0 -> W' s (l :+: r) p1 p0
instance FoldPlusW' (s :: *) where foldPlusW' (W'0 f) (W'0 g) = W'0 $ foldPlus f g
instance FoldPlusW' (s :: * -> *) where foldPlusW' (W'1 f) (W'1 g) = W'1 $ foldPlus f g
instance FoldPlusW' (s :: * -> * -> *) where foldPlusW' (W'2 f) (W'2 g) = W'2 $ foldPlus f g
mapPlus f g = foldPlus (L . f) (R . g)
mapTimes f g (a :*: b) = f a :*: g b
foldTimes comb f g (a :*: b) = comb (f a) (g b)
type family DistMaybePlus (a :: Maybe (* -> * -> *)) (b :: Maybe (* -> * -> *)) :: Maybe (* -> * -> *)
type instance DistMaybePlus Nothing b = b
type instance DistMaybePlus (Just a) Nothing = Just a
type instance DistMaybePlus (Just a) (Just b) = Just (a :+: b)
concat `fmap` mapM derive_data [''Variety, ''T0, ''T1, ''T2, ''Par1, ''Par0, ''C, ''U, ''(:*:), ''N, ''(:+:)]
concat `fmap` mapM derive_pro ['Rec, 'Dep, 'Z, 'S]