Copyright | (c) Fumiaki Kinoshita 2015 |
---|---|
License | BSD3 |
Maintainer | Fumiaki Kinoshita <fumiexcel@gmail.com> |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
A bunch of combinators that contains magic
- data Membership xs x
- getMemberId :: Membership xs x -> Word
- mkMembership :: Int -> Q Exp
- runMembership :: Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
- compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
- 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
- data NavHere xs x where
- navigate :: (NavHere xs x -> r) -> (Membership (Half (Tail xs)) x -> r) -> (Membership (Half (Tail (Tail xs))) x -> r) -> Membership xs x -> r
- here :: Membership (x : xs) x
- navNext :: Membership xs y -> Membership (x : xs) y
- navL :: Membership (Half xs) y -> Membership (x : xs) y
- navR :: Membership (Half (Tail xs)) y -> Membership (x : xs) y
- data Nat
- class KnownPosition n where
- type family Succ x :: Nat
- type family Half xs :: [k]
- type family Head xs :: k
- type family Tail xs :: [k]
- type family xs ++ ys :: [k]
- type family Map f xs :: [k]
- type family Merge xs ys :: [k]
- type family Concat xs :: [k]
- module Data.Type.Equality
- module Data.Proxy
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) |
getMemberId :: Membership xs x -> Word Source
mkMembership :: Int -> Q Exp Source
Generates a Membership
that corresponds to the given ordinal (0-origin).
runMembership :: 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.
Member class
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 |
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
Tree navigation
navigate :: (NavHere xs x -> r) -> (Membership (Half (Tail xs)) x -> r) -> (Membership (Half (Tail (Tail xs))) x -> r) -> Membership xs x -> r Source
PRIVILEGED: Navigate a tree.
here :: Membership (x : xs) x Source
The Membership
points the first element
navNext :: Membership xs y -> Membership (x : xs) y Source
The next membership
navL :: Membership (Half xs) y -> Membership (x : xs) y Source
Describes the relation of Membership
within a tree
navR :: Membership (Half (Tail xs)) y -> Membership (x : xs) y Source
Describes the relation of Membership
within a tree
Miscellaneous
Type level binary number
KnownPosition Nat Zero | |
KnownPosition Nat n => KnownPosition Nat (SDNat n) | |
KnownPosition Nat n => KnownPosition Nat (DNat n) |
class KnownPosition n where Source
Converts type naturals into Word
.
KnownPosition Nat Zero | |
KnownPosition Nat n => KnownPosition Nat (SDNat n) | |
KnownPosition Nat n => KnownPosition Nat (DNat n) |
module Data.Type.Equality
module Data.Proxy