Portability | see LANGUAGE pragmas (... GHC) |
---|---|
Stability | experimental |
Maintainer | nicolas.frisby@gmail.com |
Operators for the type-sums from Type.Yoko.Sum.
- type Inu t = Exists (:=: t)
- newtype Uni ts t = Uni (Inu t ts)
- type family PrimUni ts :: * -> *
- primUni :: Uni ts t -> PrimUni ts t
- primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) t
- type family Inhabitants u
- class Finite u where
- toUni :: u t -> Uni (Inhabitants u) t
- finiteNP :: Finite u => NP u f -> NP (Uni (Inhabitants u)) f
- class Finite u => Etinif u where
- frUni :: Uni (Inhabitants u) t -> u t
- eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v) => u a -> v b -> Maybe (a :=: b)
- type family Norm c
- type family NormW c acc
- type Each ts = NT (Uni ts)
- none :: String -> Each V f
- one_ :: Proxy (KTSS f) -> Unwrap f t -> Each (N t) f
- one :: Unwrap f t -> Each (N t) f
- oneF :: Wrapper f => f t -> Each (N t) f
- both, (|||) :: Each ts f -> Each us f -> Each (ts :+ us) f
- (.|.) :: Wrapper f => Unwrap f t -> Unwrap f s -> Each (N t :+ N s) f
- (||.) :: Wrapper f => Each ts f -> Unwrap f t -> Each (ts :+ N t) f
- (.||) :: Wrapper f => Unwrap f t -> Each ts f -> Each (N t :+ ts) f
- each :: forall u v f. ((Inhabitants v) ::: (All u), Finite v) => Proxy (KTSS u) -> (forall a. u a -> Unwrap f a) -> NT v f
- eachF :: forall u v f. (Wrapper f, (Inhabitants v) ::: (All u), Finite v) => Proxy (KTSS u) -> (forall a. u a -> f a) -> NT v f
- eachF_ :: forall f v. (Wrapper f, (Inhabitants v) ::: (All NoneU), Finite v) => (forall a. f a) -> NT v f
- prjEach :: Uni ts t -> Each ts f -> Unwrap f t
- prjEachF :: Wrapper f => Uni ts t -> Each ts f -> f t
- eachOrNT :: forall u v f w. ((Inhabitants v) ::: (All (u :|| w)), Finite v) => NT u f -> NT w f -> NT v f
Documentation
Uni ts
is a universe containing the types in the type-sum ts
.
type family Inhabitants u Source
Finite universes can be represented as type-sums.
toUni :: u t -> Uni (Inhabitants u) tSource
class Finite u => Etinif u whereSource
frUni
sometimes requires a stronger context than does toUni
, so we
separate the two methods.
frUni :: Uni (Inhabitants u) t -> u tSource
eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v) => u a -> v b -> Maybe (a :=: b)Source
Any finite universe can be used to determine type equality.
type family NormW c acc Source
NormW
combines two type-sums into a right-associated type-sum containing
no duplicates.
each :: forall u v f. ((Inhabitants v) ::: (All u), Finite v) => Proxy (KTSS u) -> (forall a. u a -> Unwrap f a) -> NT v fSource
each
is the principal means of defining an Each
value.
eachF :: forall u v f. (Wrapper f, (Inhabitants v) ::: (All u), Finite v) => Proxy (KTSS u) -> (forall a. u a -> f a) -> NT v fSource