| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
Type.Membership.Internal
Synopsis
- data Membership (xs :: [k]) (x :: k)
- getMemberId :: Membership xs x -> Int
- mkMembership :: Int -> Q Exp
- leadership :: Membership (x ': xs) x
- nextMembership :: Membership xs y -> Membership (x ': xs) y
- testMembership :: Membership (y ': xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
- compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
- impossibleMembership :: Membership '[] x -> r
- reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r
- class Member xs x where
- membership :: Membership xs x
- type (∈) x xs = Member xs x
- type family FindType (x :: k) (xs :: [k]) :: [Nat] where ...
- data Assoc k v = k :> v
- type (>:) = (:>)
- class Lookup xs k v | k xs -> v where
- association :: Membership xs (k :> v)
- type family FindAssoc (n :: Nat) (key :: k) (xs :: [Assoc k v]) where ...
- type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where ...
- data Elaborated k v
- data HList (h :: k -> *) (xs :: [k]) where
- hfoldrWithIndex :: forall h r xs. (forall x. Membership xs x -> h x -> r -> r) -> r -> HList h xs -> r
- htraverseWithIndex :: forall f g h xs. Applicative f => (forall x. Membership xs x -> g x -> f (h x)) -> HList g xs -> f (HList h xs)
- module Data.Type.Equality
- module Data.Proxy
Membership
data Membership (xs :: [k]) (x :: k) Source #
A witness that of x is a member of a type level set xs.
Instances
getMemberId :: Membership xs x -> Int Source #
get the position as an Int.
mkMembership :: Int -> Q Exp Source #
Generates a Membership that corresponds to the given ordinal (0-origin).
leadership :: Membership (x ': xs) x Source #
This Membership points to the first element
nextMembership :: Membership xs y -> Membership (x ': xs) y Source #
The next membership
testMembership :: Membership (y ': xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r Source #
Embodies a type equivalence to ensure that the Membership points the first element.
compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y) Source #
Compare two Memberships.
impossibleMembership :: Membership '[] x -> r Source #
There is no Membership of an empty list.
reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r Source #
Make up a Membership from an integer.
Member class
class Member xs x where Source #
x is a member of xs
Methods
membership :: Membership xs x Source #
Instances
| (Elaborate x (FindType x xs) ~ (Expecting pos :: Elaborated k Nat), KnownNat pos) => Member (xs :: [k]) (x :: k) Source # | |
Defined in Type.Membership.Internal Methods membership :: Membership xs x Source # | |
Association
class Lookup xs k v | k xs -> v where Source #
Lookup xs k v(k :> v) ∈ xs
, but the type v is inferred from k and xs.
Methods
association :: Membership xs (k :> v) Source #
Instances
| (Elaborate k2 (FindAssoc 0 k2 xs) ~ (Expecting (n :> v2) :: Elaborated k1 (Assoc Nat v1)), KnownNat n) => Lookup (xs :: [Assoc k1 v1]) (k2 :: k1) (v2 :: v1) Source # | |
Defined in Type.Membership.Internal Methods association :: Membership xs (k2 :> v2) Source # | |
type family FindAssoc (n :: Nat) (key :: k) (xs :: [Assoc k v]) where ... Source #
Find a type associated to the specified key.
Sugar
type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where ... Source #
Make the result more readable
data Elaborated k v Source #
A readable type search result
HList
hfoldrWithIndex :: forall h r xs. (forall x. Membership xs x -> h x -> r -> r) -> r -> HList h xs -> r Source #
htraverseWithIndex :: forall f g h xs. Applicative f => (forall x. Membership xs x -> g x -> f (h x)) -> HList g xs -> f (HList h xs) Source #
Miscellaneous
module Data.Type.Equality
module Data.Proxy