| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Generics.MRSOP.Util
Contents
Description
Useful utilities we need accross multiple modules.
- (&&&) :: Arrow a => forall b c c'. a b c -> a b c' -> a b (c, c')
- (***) :: Arrow a => forall b c b' c'. 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
- data Nat
- proxyUnsuc :: Proxy (S n) -> Proxy n
- data SNat :: Nat -> * where
- snat2int :: SNat n -> Integer
- class IsNat (n :: Nat) where
- getNat :: IsNat n => Proxy n -> Integer
- getSNat' :: forall (n :: Nat). IsNat n => SNat n
- data ListPrf :: [k] -> * where
- class IsList (xs :: [k]) where
- 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
- 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
- class Show1 (f :: k -> *) where
Utility Functions and Types
(&&&) :: Arrow a => forall b c c'. 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 => forall b c b' c'. 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.
Poly-kind indexed product
data ((f :: k -> *) :*: (g :: k -> *)) (x :: k) Source #
Poly-kind-indexed product
Constructors
| (f x) :*: (g x) |
Type-level Naturals
Type-level Peano Naturals
class IsNat (n :: Nat) where Source #
And their conversion to term-level integers.
Minimal complete definition
Type-level Lists
data ListPrf :: [k] -> * where Source #
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.
class IsList (xs :: [k]) where Source #
The IsList class allows us to construct
ListPrfs in a straight forward fashion.
Minimal complete definition
appendIsListLemma :: ListPrf xs -> ListPrf ys -> ListPrf (xs :++: ys) Source #
Concatenation of lists is also a list.
Type-level List Lookup
getElSNat :: forall ix ls. El ls ix -> SNat ix Source #
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 Source #
Smart constructor into El