Copyright | (c) Fumiaki Kinoshita 2017 |
---|---|
License | BSD3 |
Maintainer | Fumiaki Kinoshita <fumiexcel@gmail.com> |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
A bunch of combinators that contains magic
- data Membership xs x
- getMemberId :: Membership xs x -> Int
- mkMembership :: Int -> Q Exp
- reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r
- leadership :: 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
- here :: Membership (x ': xs) x
- navNext :: Membership xs y -> Membership (x ': xs) y
- class Member xs x where
- remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r
- type (∈) x xs = Member xs x
- type family FindType (x :: k) (xs :: [k]) :: [Nat] where ...
- data Assoc k v = k :> v
- type (>:) = (:>)
- class Associate k v xs | k xs -> v where
- type family FindAssoc (key :: k) (xs :: [Assoc k v]) where ...
- type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where ...
- data Elaborated k v
- data Nat
- class KnownPosition n where
- type family Succ (x :: Nat) :: Nat where ...
- type family Head (xs :: [k]) :: k where ...
- type family Last (x :: [k]) :: k where ...
- module Data.Type.Equality
- module Data.Proxy
Membership
data Membership xs x Source #
The position of x
in the type level set xs
.
Eq (Membership k xs x) Source # | |
Ord (Membership k xs x) Source # | |
Show (Membership k xs x) Source # | |
Semigroup (Membership k xs x) Source # | |
NFData (Membership k xs x) Source # | |
getMemberId :: Membership xs x -> Int Source #
mkMembership :: Int -> Q Exp Source #
Generates a Membership
that corresponds to the given ordinal (0-origin).
reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r Source #
leadership :: 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 Membership
s.
impossibleMembership :: Membership '[] x -> r Source #
There is no Membership
of an empty list.
here :: Membership (x ': xs) x Source #
The Membership
points the first element
navNext :: Membership xs y -> Membership (x ': xs) y Source #
The next membership
Member class
remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r Source #
Remember that Member xs x
from Membership
.
Association
The kind of key-value pairs
k :> v infix 0 |
class Associate k v xs | k xs -> v where Source #
is essentially identical to Associate
k v xs(k :> v) ∈ xs
, but the type v
is inferred from k
and xs
.
association :: Membership xs (k :> v) Source #
Sugar
type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where ... Source #
Miscellaneous
Type level binary number
KnownPosition Nat Zero Source # | |
KnownPosition Nat n => KnownPosition Nat (DNat n) Source # | |
KnownPosition Nat n => KnownPosition Nat (SDNat n) Source # | |
class KnownPosition n where Source #
Converts type naturals into Word
.
KnownPosition Nat Zero Source # | |
KnownPosition Nat n => KnownPosition Nat (DNat n) Source # | |
KnownPosition Nat n => KnownPosition Nat (SDNat n) Source # | |
module Data.Type.Equality
module Data.Proxy