Safe Haskell | None |
---|---|
Language | Haskell2010 |
- class Extensible f p q t where
- pieceAt :: Membership xs x -> p (h x) (f (h x)) -> q (t h xs) (f (t h xs))
- piece :: (x ∈ xs, Extensible f p q t) => p (h x) (f (h x)) -> q (t h xs) (f (t h xs))
- pieceAssoc :: (Associate k v xs, Extensible f p q t) => p (h (k :> v)) (f (h (k :> v))) -> q (t h xs) (f (t h xs))
- data Membership xs x
- mkMembership :: Int -> Q Exp
- class Member xs x where
- membership :: Membership xs x
- remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r
- type (∈) x xs = Member xs x
- type family FindType x xs :: [Nat]
- data Assoc k v = k :> v
- class Associate k v xs | k xs -> v where
- association :: Membership xs (k :> v)
- type family FindAssoc key xs
- type family Elaborate key xs :: Elaborated k v
- data Elaborated k v
Class
class Extensible f p q t where Source
This class allows us to use pieceAt
for both sums and products.
pieceAt :: Membership xs x -> p (h x) (f (h x)) -> q (t h xs) (f (t h xs)) Source
Functor f => Extensible k * f (->) (->) ((:*) k) | |
(Applicative f, Choice p) => Extensible k * f p p ((:|) k) | |
Extensible k k f (LabelPhantom k * k s) q t |
piece :: (x ∈ xs, Extensible f p q t) => p (h x) (f (h x)) -> q (t h xs) (f (t h xs)) Source
Accessor for an element.
pieceAssoc :: (Associate k v xs, Extensible f p q t) => p (h (k :> v)) (f (h (k :> v))) -> q (t h xs) (f (t h xs)) Source
Like piece
, but reckon membership from its key.
Membership
data Membership xs x Source
The position of x
in the type level set xs
.
Typeable ([k] -> k -> *) (Membership k) | |
Eq (Membership k xs x) | |
Ord (Membership k xs x) | |
Show (Membership k xs x) |
mkMembership :: Int -> Q Exp Source
Generates a Membership
that corresponds to the given ordinal (0-origin).
Member
class Member xs x where Source
membership :: Membership xs x Source
((~) (Elaborated k Nat) (Elaborate k Nat x (FindType k x xs)) (Expecting k Nat pos), KnownPosition Nat pos) => Member k xs x |
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 |
Associate k k1 k2 v xs => Associated (Assoc k k) xs ((:>) k k k v) |
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 xs :: Elaborated k v Source
data Elaborated k v Source