module Data.MGeneric
( (:$:)
, Un(..)
, Field(..)
, In(..)
, InField(..)
, ExpandField
, ExpandFields
, MGeneric(..)
)
where
import Data.Nat
type family (f :: k) :$: (as :: [*]) :: * where
f :$: '[] = f
f :$: (a ': as) = f a :$: as
data Un s = UV
| UT
| UF (Field s)
| Un s :**: Un s
| Un s :++: Un s
data Field s = FK s
| FP Nat
| forall k. k :@: [Field s]
data In (u :: Un *) (ps :: [*]) :: * where
InT :: In UT ps
InF :: InField f ps -> In (UF f) ps
InL :: In u ps -> In (u :++: v) ps
InR :: In v ps -> In (u :++: v) ps
(:*:) :: In u ps -> In v ps -> In (u :**: v) ps
infixr 5 :*:
data InField (f :: Field *) (ps :: [*]) :: * where
InK :: a -> InField (FK a) ps
InP :: ps :!: n -> InField (FP n) ps
InA :: f :$: ExpandFields as ps -> InField (f :@: as) ps
type family ExpandField (f :: Field *) (ps :: [*]) :: * where
ExpandField (FK a) ps = a
ExpandField (FP n) ps = ps :!: n
ExpandField (f :@: as) ps = f :$: ExpandFields as ps
type family ExpandFields (f :: [Field *]) (ps :: [*]) :: [*] where
ExpandFields '[] ps = '[]
ExpandFields (FK a ': fs) ps = a ': ExpandFields fs ps
ExpandFields (FP n ': fs) ps = (ps :!: n) ': ExpandFields fs ps
ExpandFields ((f :@: as) ': fs) ps = (f :$: ExpandFields as ps) ': ExpandFields fs ps
class MGeneric (a :: *) where
type Rep a :: Un *
type Pars a :: [*]
from :: a -> In (Rep a) (Pars a)
to :: In (Rep a) (Pars a) -> a