Safe Haskell	Safe
Language	Haskell2010

Generics.MRSOP.Base.Universe

Contents

Universe of Codes
- Map, Elim and Zip
Representation of Codes
- Map, Elim and Zip
SOP functionality
Least Fixpoints

Description

Wraps the definitions of NP and NS into Representations (Rep), essentially providing the universe view over sums-of-products.

Synopsis

data Atom kon
- = K kon
- | I Nat
data NA :: (kon -> *) -> (Nat -> *) -> Atom kon -> * where
- NA_I :: IsNat k => phi k -> NA ki phi (I k)
- NA_K :: ki k -> NA ki phi (K k)
mapNA :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> NA ki f a -> NA kj g a
mapNAM :: Monad m => (forall k. ki k -> m (kj k)) -> (forall ix. IsNat ix => f ix -> m (g ix)) -> NA ki f a -> m (NA kj g a)
elimNA :: (forall k. ki k -> b) -> (forall k. IsNat k => phi k -> b) -> NA ki phi a -> b
zipNA :: NA ki f a -> NA kj g a -> NA (ki :*: kj) (f :*: g) a
eqNA :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> NA ki fam l -> NA ki fam l -> Bool
newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]]) = Rep {
- unRep :: NS (PoA ki phi) code
}
type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)
mapRep :: (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep ki g c
mapRepM :: Monad m => (forall ix. IsNat ix => f ix -> m (g ix)) -> Rep ki f c -> m (Rep ki g c)
bimapRep :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep kj g c
bimapRepM :: Monad m => (forall k. ki k -> m (kj k)) -> (forall ix. IsNat ix => f ix -> m (g ix)) -> Rep ki f c -> m (Rep kj g c)
zipRep :: MonadPlus m => Rep ki f c -> Rep kj g c -> m (Rep (ki :*: kj) (f :*: g) c)
elimRepM :: Monad m => (forall k. ki k -> m a) -> (forall k. IsNat k => f k -> m a) -> ([a] -> m b) -> Rep ki f c -> m b
elimRep :: (forall k. ki k -> a) -> (forall k. IsNat k => f k -> a) -> ([a] -> b) -> Rep ki f c -> b
eqRep :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> Rep ki fam c -> Rep ki fam c -> Bool
data Constr :: [k] -> Nat -> * where
- CS :: Constr xs n -> Constr (x ': xs) (S n)
- CZ :: Constr (x ': xs) Z
injNS :: Constr sum n -> PoA ki fam (Lkup n sum) -> NS (NP (NA ki fam)) sum
inj :: Constr sum n -> PoA ki fam (Lkup n sum) -> Rep ki fam sum
matchNS :: Constr sum c -> NS (NP (NA ki fam)) sum -> Maybe (PoA ki fam (Lkup c sum))
match :: Constr sum c -> Rep ki fam sum -> Maybe (PoA ki fam (Lkup c sum))
data View :: (kon -> *) -> (Nat -> *) -> [[Atom kon]] -> * where
- Tag :: IsNat n => Constr sum n -> PoA ki fam (Lkup n sum) -> View ki fam sum
sop :: Rep ki fam sum -> View ki fam sum
fromView :: View ki fam sum -> Rep ki fam sum
data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (phi :: Nat -> *) (n :: Nat) = AnnFix (phi n) (Rep ki (AnnFix ki codes phi) (Lkup n codes))
type Fix ki codes = AnnFix ki codes (Const ())
pattern Fix :: forall kon (ki :: kon -> Type) (codes :: [[[Atom kon]]]) (n :: Nat). Rep ki (AnnFix ki codes (Const () :: Nat -> Type)) (Lkup n codes) -> AnnFix ki codes (Const () :: Nat -> Type) n
unFix :: Fix ki codes ix -> Rep ki (Fix ki codes) (Lkup ix codes)
cata :: IsNat ix => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -> Fix ki codes ix -> phi ix
getAnn :: AnnFix ki codes ann ix -> ann ix
annCata :: (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -> AnnFix ki codes chi ix -> phi ix
forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix
proxyFixIdx :: phi ix -> Proxy ix
sNatFixIdx :: IsNat ix => phi ix -> SNat ix
mapFixM :: Monad m => (forall k. ki k -> m (kj k)) -> Fix ki fam ix -> m (Fix kj fam ix)
eqFix :: (forall k. ki k -> ki k -> Bool) -> Fix ki fam ix -> Fix ki fam ix -> Bool
heqFixIx :: (IsNat ix, IsNat ix') => Fix ki fam ix -> Fix ki fam ix' -> Maybe (ix :~: ix')

Universe of Codes

We will use nested lists to represent the Sums-of-Products structure. The atoms, however, will be parametrized by a kind used to index what are the types that are opaque to the library.

data Atom kon #

Atoms can be either opaque types, kon, or type variables, Nat.

Constructors

K kon
I Nat

Instances

Family Singl FamRoseInt CodesRoseInt #
Instance details Defined in Generics.MRSOP.Examples.RoseTreeTH Methods sfrom' :: SNat ix -> El FamRoseInt ix -> Rep Singl (El FamRoseInt) (Lkup ix CodesRoseInt) # sto' :: SNat ix -> Rep Singl (El FamRoseInt) (Lkup ix CodesRoseInt) -> El FamRoseInt ix #
Family Singl FamRose CodesRose #
Instance details Defined in Generics.MRSOP.Examples.RoseTree Methods sfrom' :: SNat ix -> El FamRose ix -> Rep Singl (El FamRose) (Lkup ix CodesRose) # sto' :: SNat ix -> Rep Singl (El FamRose) (Lkup ix CodesRose) -> El FamRose ix #
Family Singl FamTerm CodesTerm #
Instance details Defined in Generics.MRSOP.Examples.LambdaAlphaEqTH Methods sfrom' :: SNat ix -> El FamTerm ix -> Rep Singl (El FamTerm) (Lkup ix CodesTerm) # sto' :: SNat ix -> Rep Singl (El FamTerm) (Lkup ix CodesTerm) -> El FamTerm ix #
Family Singl FamStmtString CodesStmtString #
Instance details Defined in Generics.MRSOP.Examples.SimpTH Methods sfrom' :: SNat ix -> El FamStmtString ix -> Rep Singl (El FamStmtString) (Lkup ix CodesStmtString) # sto' :: SNat ix -> Rep Singl (El FamStmtString) (Lkup ix CodesStmtString) -> El FamStmtString ix #
HasDatatypeInfo Singl FamRoseInt CodesRoseInt #
Instance details Defined in Generics.MRSOP.Examples.RoseTreeTH Methods datatypeInfo :: Proxy FamRoseInt -> SNat ix -> DatatypeInfo (Lkup ix CodesRoseInt) #
HasDatatypeInfo Singl FamRose CodesRose #
Instance details Defined in Generics.MRSOP.Examples.RoseTree Methods datatypeInfo :: Proxy FamRose -> SNat ix -> DatatypeInfo (Lkup ix CodesRose) #
HasDatatypeInfo Singl FamTerm CodesTerm #
Instance details Defined in Generics.MRSOP.Examples.LambdaAlphaEqTH Methods datatypeInfo :: Proxy FamTerm -> SNat ix -> DatatypeInfo (Lkup ix CodesTerm) #
HasDatatypeInfo Singl FamStmtString CodesStmtString #
Instance details Defined in Generics.MRSOP.Examples.SimpTH Methods datatypeInfo :: Proxy FamStmtString -> SNat ix -> DatatypeInfo (Lkup ix CodesStmtString) #
Eq kon => Eq (Atom kon) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods (==) :: Atom kon -> Atom kon -> Bool # (/=) :: Atom kon -> Atom kon -> Bool #
Show kon => Show (Atom kon) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods showsPrec :: Int -> Atom kon -> ShowS # show :: Atom kon -> String # showList :: [Atom kon] -> ShowS #
TestEquality ki => TestEquality (NA ki phi :: Atom kon -> Type) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods testEquality :: NA ki phi a -> NA ki phi b -> Maybe (a :~: b) #
(Eq1 phi, Eq1 ki) => Eq1 (Rep ki phi :: [[Atom kon]] -> Type) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods eq1 :: Rep ki phi k -> Rep ki phi k -> Bool #
(Eq1 phi, Eq1 ki) => Eq1 (NA ki phi :: Atom kon -> Type) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods eq1 :: NA ki phi k -> NA ki phi k -> Bool #
Show (NP (ConstructorInfo :: [Atom kon] -> Type) code) #
Instance details Defined in Generics.MRSOP.Base.Metadata Methods showsPrec :: Int -> NP ConstructorInfo code -> ShowS # show :: NP ConstructorInfo code -> String # showList :: [NP ConstructorInfo code] -> ShowS #
Show (NP (FieldInfo :: Atom kon -> Type) code) #
Instance details Defined in Generics.MRSOP.Base.Metadata Methods showsPrec :: Int -> NP FieldInfo code -> ShowS # show :: NP FieldInfo code -> String # showList :: [NP FieldInfo code] -> ShowS #
(Show1 phi, Show1 ki) => Show (PoA ki (AnnFix ki codes phi) xs) #
Instance details Defined in Generics.MRSOP.Base.Show Methods showsPrec :: Int -> PoA ki (AnnFix ki codes phi) xs -> ShowS # show :: PoA ki (AnnFix ki codes phi) xs -> String # showList :: [PoA ki (AnnFix ki codes phi) xs] -> ShowS #

data NA :: (kon -> *) -> (Nat -> *) -> Atom kon -> * where #

NA ki phi a provides an interpretation for an atom a, using either ki or phi to interpret the type variable or opaque type.

Constructors

NA_I :: IsNat k => phi k -> NA ki phi (I k)
NA_K :: ki k -> NA ki phi (K k)

Instances

TestEquality ki => TestEquality (NA ki phi :: Atom kon -> Type) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods testEquality :: NA ki phi a -> NA ki phi b -> Maybe (a :~: b) #
(Eq1 phi, Eq1 ki) => Eq1 (NA ki phi :: Atom kon -> Type) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods eq1 :: NA ki phi k -> NA ki phi k -> Bool #
(Show1 phi, Show1 ki) => Show (PoA ki (AnnFix ki codes phi) xs) #
Instance details Defined in Generics.MRSOP.Base.Show Methods showsPrec :: Int -> PoA ki (AnnFix ki codes phi) xs -> ShowS # show :: PoA ki (AnnFix ki codes phi) xs -> String # showList :: [PoA ki (AnnFix ki codes phi) xs] -> ShowS #
(Show1 phi, Show1 ki) => Show (NA ki (AnnFix ki codes phi) a) #
Instance details Defined in Generics.MRSOP.Base.Show Methods showsPrec :: Int -> NA ki (AnnFix ki codes phi) a -> ShowS # show :: NA ki (AnnFix ki codes phi) a -> String # showList :: [NA ki (AnnFix ki codes phi) a] -> ShowS #

Map, Elim and Zip

mapNA :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> NA ki f a -> NA kj g a #

Maps a natural transformation over an atom interpretation

mapNAM :: Monad m => (forall k. ki k -> m (kj k)) -> (forall ix. IsNat ix => f ix -> m (g ix)) -> NA ki f a -> m (NA kj g a) #

Maps a monadic natural transformation over an atom interpretation

elimNA :: (forall k. ki k -> b) -> (forall k. IsNat k => phi k -> b) -> NA ki phi a -> b #

Eliminates an atom interpretation

zipNA :: NA ki f a -> NA kj g a -> NA (ki :*: kj) (f :*: g) a #

Combines two atoms into one

eqNA :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> NA ki fam l -> NA ki fam l -> Bool #

Compares atoms provided we know how to compare the leaves, both recursive and constant.

Representation of Codes

Codes are represented using the Rep newtype, which wraps an n-ary sum of n-ary products. Note it receives two functors: ki and phi, to interpret opaque types and type variables respectively.

newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]]) #

Representation of codes.

Constructors

Rep
Fields unRep :: NS (PoA ki phi) code

Instances

(Eq1 phi, Eq1 ki) => Eq1 (Rep ki phi :: [[Atom kon]] -> Type) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods eq1 :: Rep ki phi k -> Rep ki phi k -> Bool #
(Show1 phi, Show1 ki) => Show (Rep ki (AnnFix ki codes phi) xs) #
Instance details Defined in Generics.MRSOP.Base.Show Methods showsPrec :: Int -> Rep ki (AnnFix ki codes phi) xs -> ShowS # show :: Rep ki (AnnFix ki codes phi) xs -> String # showList :: [Rep ki (AnnFix ki codes phi) xs] -> ShowS #

type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi) #

Product of Atoms is a handy synonym to have.

Map, Elim and Zip

Just like for NS, NP and NA, we provide a couple convenient functions working over a Rep. These are just the cannonical combination of their homonym versions in NS, NP or NA.

mapRep :: (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep ki g c #

Maps over a representation.

mapRepM :: Monad m => (forall ix. IsNat ix => f ix -> m (g ix)) -> Rep ki f c -> m (Rep ki g c) #

Maps a monadic function over a representation.

bimapRep :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep kj g c #

Maps over both indexes of a representation.

bimapRepM :: Monad m => (forall k. ki k -> m (kj k)) -> (forall ix. IsNat ix => f ix -> m (g ix)) -> Rep ki f c -> m (Rep kj g c) #

Monadic version of bimapRep

zipRep :: MonadPlus m => Rep ki f c -> Rep kj g c -> m (Rep (ki :*: kj) (f :*: g) c) #

Zip two representations together, in case they are made with the same constructor.

zipRep (Here (NA_I x :* NP0)) (Here (NA_I y :* NP0))
  = return $ Here (NA_I (x :*: y) :* NP0)

zipRep (Here (NA_I x :* NP0)) (There (Here ...))
  = mzero

elimRepM :: Monad m => (forall k. ki k -> m a) -> (forall k. IsNat k => f k -> m a) -> ([a] -> m b) -> Rep ki f c -> m b #

Monadic eliminator; This is just the cannonical combination of elimNS, elimNPM and elimNA.

elimRep :: (forall k. ki k -> a) -> (forall k. IsNat k => f k -> a) -> ([a] -> b) -> Rep ki f c -> b #

Pure eliminator.

eqRep :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> Rep ki fam c -> Rep ki fam c -> Bool #

Compares two Rep for equality; again, cannonical combination of eqNS, eqNP and eqNA

SOP functionality

It is often more convenient to view a value of Rep as a constructor and its fields, instead of having to traverse the inner NS structure.

data Constr :: [k] -> Nat -> * where #

A value c :: Constr ks n specifies a position in a type-level list. It is, in fact, isomorphic to Fin (length ks).

Constructors

CS :: Constr xs n -> Constr (x ': xs) (S n)
CZ :: Constr (x ': xs) Z

Instances

TestEquality (Constr codes :: Nat -> Type) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods testEquality :: Constr codes a -> Constr codes b -> Maybe (a :~: b) #
IsNat n => Show (Constr xs n) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods showsPrec :: Int -> Constr xs n -> ShowS # show :: Constr xs n -> String # showList :: [Constr xs n] -> ShowS #

injNS :: Constr sum n -> PoA ki fam (Lkup n sum) -> NS (NP (NA ki fam)) sum #

We can define injections into an n-ary sum from its Constructors

inj :: Constr sum n -> PoA ki fam (Lkup n sum) -> Rep ki fam sum #

Wrap it in a Rep for convenience.

matchNS :: Constr sum c -> NS (NP (NA ki fam)) sum -> Maybe (PoA ki fam (Lkup c sum)) #

Inverse of injNS. Given some Constructor, see if Rep is of this constructor

match :: Constr sum c -> Rep ki fam sum -> Maybe (PoA ki fam (Lkup c sum)) #

Inverse of inj. Given some Constructor, see if Rep is of this constructor

data View :: (kon -> *) -> (Nat -> *) -> [[Atom kon]] -> * where #

Finally, we can view a sum-of-products as a constructor and a product-of-atoms.

Constructors

Tag :: IsNat n => Constr sum n -> PoA ki fam (Lkup n sum) -> View ki fam sum

sop :: Rep ki fam sum -> View ki fam sum #

Unwraps a Rep into a View

fromView :: View ki fam sum -> Rep ki fam sum #

Wraps a View into a Rep

Least Fixpoints

Finally we tie the recursive knot. Given an interpretation for the constant types, a family of sums-of-products and an index ix into such family, we take the least fixpoint of the representation of the code indexed by ix

data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (phi :: Nat -> *) (n :: Nat) #

Indexed least fixpoints

Annotated version of Fix. This is basically the Cofree datatype, but for n-ary functors

Constructors

AnnFix (phi n) (Rep ki (AnnFix ki codes phi) (Lkup n codes))

Instances

Eq1 ki => Eq1 (Fix ki codes :: Nat -> Type) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods eq1 :: Fix ki codes k -> Fix ki codes k -> Bool #
Eq1 ki => Eq (Fix ki codes ix) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods (==) :: Fix ki codes ix -> Fix ki codes ix -> Bool # (/=) :: Fix ki codes ix -> Fix ki codes ix -> Bool #
(Show1 phi, Show1 ki) => Show (PoA ki (AnnFix ki codes phi) xs) #
Instance details Defined in Generics.MRSOP.Base.Show Methods showsPrec :: Int -> PoA ki (AnnFix ki codes phi) xs -> ShowS # show :: PoA ki (AnnFix ki codes phi) xs -> String # showList :: [PoA ki (AnnFix ki codes phi) xs] -> ShowS #
(Show1 phi, Show1 ki) => Show (Rep ki (AnnFix ki codes phi) xs) #
Instance details Defined in Generics.MRSOP.Base.Show Methods showsPrec :: Int -> Rep ki (AnnFix ki codes phi) xs -> ShowS # show :: Rep ki (AnnFix ki codes phi) xs -> String # showList :: [Rep ki (AnnFix ki codes phi) xs] -> ShowS #
(Show1 phi, Show1 ki) => Show (NA ki (AnnFix ki codes phi) a) #
Instance details Defined in Generics.MRSOP.Base.Show Methods showsPrec :: Int -> NA ki (AnnFix ki codes phi) a -> ShowS # show :: NA ki (AnnFix ki codes phi) a -> String # showList :: [NA ki (AnnFix ki codes phi) a] -> ShowS #
(Show1 phi, Show1 ki) => Show (AnnFix ki codes phi ix) #
Instance details Defined in Generics.MRSOP.Base.Show Methods showsPrec :: Int -> AnnFix ki codes phi ix -> ShowS # show :: AnnFix ki codes phi ix -> String # showList :: [AnnFix ki codes phi ix] -> ShowS #

type Fix ki codes = AnnFix ki codes (Const ()) #

pattern Fix :: forall kon (ki :: kon -> Type) (codes :: [[[Atom kon]]]) (n :: Nat). Rep ki (AnnFix ki codes (Const () :: Nat -> Type)) (Lkup n codes) -> AnnFix ki codes (Const () :: Nat -> Type) n #

unFix :: Fix ki codes ix -> Rep ki (Fix ki codes) (Lkup ix codes) #

cata :: IsNat ix => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -> Fix ki codes ix -> phi ix #

Catamorphism over fixpoints

getAnn :: AnnFix ki codes ann ix -> ann ix #

annCata :: (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -> AnnFix ki codes chi ix -> phi ix #

forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix #

Forget the annotations

proxyFixIdx :: phi ix -> Proxy ix #

Retrieves the index of a Fix

sNatFixIdx :: IsNat ix => phi ix -> SNat ix #

mapFixM :: Monad m => (forall k. ki k -> m (kj k)) -> Fix ki fam ix -> m (Fix kj fam ix) #

Maps over the values of opaque types within the fixpoint.

eqFix :: (forall k. ki k -> ki k -> Bool) -> Fix ki fam ix -> Fix ki fam ix -> Bool #

Compare two values of a same fixpoint for equality.

heqFixIx :: (IsNat ix, IsNat ix') => Fix ki fam ix -> Fix ki fam ix' -> Maybe (ix :~: ix') #

Compare two indexes of two fixpoints Note we can't use a testEquality instance because of the IsNat constraint.