Safe Haskell	Safe
Language	Haskell2010

Generics.MRSOP.Util

Contents

Utility Functions and Types
Poly-kind indexed product
Type-level Naturals
Type-level Lists
Type-level List Lookup
Higher-order Eq and Show

Description

Useful utilities we need accross multiple modules.

Synopsis

(&&&) :: Arrow a => a b c -> a b c' -> a b (c, c')
(***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c')
type (:->) f g = forall n. f n -> g n
(<.>) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c
data ((f :: k -> *) :*: (g :: k -> *)) (x :: k) = (f x) :*: (g x)
curry' :: ((f :*: g) x -> a) -> f x -> g x -> a
uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a
delta' :: (f :*: g) x -> (f x, g x)
data Nat
- = S Nat
- | Z
proxyUnsuc :: Proxy (S n) -> Proxy n
data SNat :: Nat -> * where
- SZ :: SNat Z
- SS :: SNat n -> SNat (S n)
snat2int :: SNat n -> Integer
class IsNat (n :: Nat) where
- getSNat :: Proxy n -> SNat n
getNat :: IsNat n => Proxy n -> Integer
getSNat' :: forall (n :: Nat). IsNat n => SNat n
data ListPrf :: [k] -> * where
- Nil :: ListPrf '[]
- Cons :: ListPrf l -> ListPrf (x ': l)
class IsList (xs :: [k]) where
- listPrf :: ListPrf xs
type L1 xs = IsList xs
type L2 xs ys = (IsList xs, IsList ys)
type L3 xs ys zs = (IsList xs, IsList ys, IsList zs)
type L4 xs ys zs as = (IsList xs, IsList ys, IsList zs, IsList as)
type family (txs :: [k]) :++: (tys :: [k]) :: [k] where ...
appendIsListLemma :: ListPrf xs -> ListPrf ys -> ListPrf (xs :++: ys)
type family Lkup (n :: Nat) (ks :: [k]) :: k where ...
type family Idx (ty :: k) (xs :: [k]) :: Nat where ...
data El :: [*] -> Nat -> * where
- El :: IsNat ix => {..} -> El fam ix
getElSNat :: forall ix ls. El ls ix -> SNat ix
into :: forall fam ty ix. (ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix) => ty -> El fam ix
class Eq1 (f :: k -> *) where
- eq1 :: forall k. f k -> f k -> Bool
class Show1 (f :: k -> *) where
- show1 :: forall k. f k -> String

Utility Functions and Types

(&&&) :: Arrow a => a b c -> a b c' -> a b (c, c') infixr 3 #

Fanout: send the input to both argument arrows and combine their output.

The default definition may be overridden with a more efficient version if desired.

(***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c') infixr 3 #

Split the input between the two argument arrows and combine their output. Note that this is in general not a functor.

The default definition may be overridden with a more efficient version if desired.

type (:->) f g = forall n. f n -> g n #

Natural transformations

(<.>) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c infixr 8 #

Kleisli Composition

Poly-kind indexed product

data ((f :: k -> *) :*: (g :: k -> *)) (x :: k) #

Poly-kind-indexed product

Constructors

(f x) :*: (g x)

curry' :: ((f :*: g) x -> a) -> f x -> g x -> a #

Lifted curry

uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a #

Lifted uncurry

delta' :: (f :*: g) x -> (f x, g x) #

Distributes the index over the product

Type-level Naturals

data Nat #

Type-level Peano Naturals

Constructors

S Nat
Z

Instances

Eq Nat #
Instance details Defined in Generics.MRSOP.Util Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Show Nat #
Instance details Defined in Generics.MRSOP.Util Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
TestEquality SNat #
Instance details Defined in Generics.MRSOP.Util Methods testEquality :: SNat a -> SNat b -> Maybe (a :~: b) #
TestEquality (Constr codes :: Nat -> Type) #
Instance details Defined in Generics.MRSOP.Base.Universe Methods testEquality :: Constr codes a -> Constr codes b -> Maybe (a :~: b) #
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 #

proxyUnsuc :: Proxy (S n) -> Proxy n #

data SNat :: Nat -> * where #

Singleton Term-level natural

Constructors

SZ :: SNat Z
SS :: SNat n -> SNat (S n)

Instances

TestEquality SNat #
Instance details Defined in Generics.MRSOP.Util Methods testEquality :: SNat a -> SNat b -> Maybe (a :~: b) #

snat2int :: SNat n -> Integer #

class IsNat (n :: Nat) where #

And their conversion to term-level integers.

Methods

getSNat :: Proxy n -> SNat n #

Instances

IsNat Z #
Instance details Defined in Generics.MRSOP.Util Methods getSNat :: Proxy Z -> SNat Z #
IsNat n => IsNat (S n) #
Instance details Defined in Generics.MRSOP.Util Methods getSNat :: Proxy (S n) -> SNat (S n) #

getNat :: IsNat n => Proxy n -> Integer #

getSNat' :: forall (n :: Nat). IsNat n => SNat n #

Type-level Lists

data ListPrf :: [k] -> * where #

An inhabitant of ListPrf ls is *not* a singleton! It only proves that ls is, in fact, a type level list. This is useful since it enables us to pattern match on type-level lists whenever we see fit.

Constructors

Nil :: ListPrf '[]
Cons :: ListPrf l -> ListPrf (x ': l)

class IsList (xs :: [k]) where #

The IsList class allows us to construct ListPrfs in a straight forward fashion.

Methods

listPrf :: ListPrf xs #

Instances

IsList ([] :: [k]) #
Instance details Defined in Generics.MRSOP.Util Methods listPrf :: ListPrf [] #
IsList xs => IsList (x ': xs :: [k]) #
Instance details Defined in Generics.MRSOP.Util Methods listPrf :: ListPrf (x ': xs) #

type L1 xs = IsList xs #

Convenient constraint synonyms

type L2 xs ys = (IsList xs, IsList ys) #

type L3 xs ys zs = (IsList xs, IsList ys, IsList zs) #

type L4 xs ys zs as = (IsList xs, IsList ys, IsList zs, IsList as) #

type family (txs :: [k]) :++: (tys :: [k]) :: [k] where ... #

Appending type-level lists

Equations

'[] :++: tys = tys
(tx ': txs) :++: tys = tx ': (txs :++: tys)

appendIsListLemma :: ListPrf xs -> ListPrf ys -> ListPrf (xs :++: ys) #

Concatenation of lists is also a list.

Type-level List Lookup

type family Lkup (n :: Nat) (ks :: [k]) :: k where ... #

Type-level list lookup

Equations

Lkup Z (k ': ks) = k
Lkup (S n) (k ': ks) = Lkup n ks
Lkup _ '[] = TypeError (Text "Lkup index too big")

type family Idx (ty :: k) (xs :: [k]) :: Nat where ... #

Type-level list index

Equations

Idx x (x ': ys) = Z
Idx x (y ': ys) = S (Idx x ys)
Idx x '[] = TypeError (Text "Element not found")

data El :: [*] -> Nat -> * where #

Also list lookup, but for kind * only.

Constructors

El
Fields :: IsNat ix => { unEl :: Lkup ix fam } -> El fam ix

getElSNat :: forall ix ls. El ls ix -> SNat ix #

Convenient way to cast an El index to term-level.

into :: forall fam ty ix. (ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix) => ty -> El fam ix #

Smart constructor into El

Higher-order Eq and Show

class Eq1 (f :: k -> *) where #

Higher order version of Eq

Methods

eq1 :: forall k. f k -> f k -> Bool #

Instances

Eq1 Singl #
Instance details Defined in Generics.MRSOP.Opaque Methods eq1 :: Singl k -> Singl k -> Bool #
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 => Eq1 (NS ki :: [k] -> Type) #
Instance details Defined in Generics.MRSOP.Base.NS Methods eq1 :: NS ki k0 -> NS ki k0 -> Bool #
Eq1 ki => Eq1 (NP ki :: [k] -> Type) #
Instance details Defined in Generics.MRSOP.Base.NP Methods eq1 :: NP ki k0 -> NP ki k0 -> Bool #
(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 #

class Show1 (f :: k -> *) where #

Higher order version of Show

Methods

show1 :: forall k. f k -> String #

Instances

Show1 Singl #
Instance details Defined in Generics.MRSOP.Opaque Methods show1 :: Singl k -> String #
Show k2 => Show1 (Const k2 :: k1 -> Type) #
Instance details Defined in Generics.MRSOP.AG Methods show1 :: Const k2 k -> String #
(Show1 f, Show1 g) => Show1 (Product f g :: k -> Type) #
Instance details Defined in Generics.MRSOP.AG Methods show1 :: Product f g k0 -> String #