Copyright | (c) Fumiaki Kinoshita 2015 |
---|---|
License | BSD3 |
Maintainer | Fumiaki Kinoshita <fumiexcel@gmail.com> |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
A bunch of combinators that contains magic
- data Membership xs x
- runMembership :: Membership (y : xs) x -> Either (x :~: y) (Membership xs x)
- compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
- ord :: Int -> Q Exp
- 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
- class Member xs x where
- membership :: Membership xs x
- type (∈) x xs = Member xs x
- data Nat
- class ToInt n where
- type family Lookup x xs :: [Nat]
- type family Succ x :: Nat
- type family MapSucc xs :: [Nat]
- type family Half xs :: [k]
- type family Tail xs :: [k]
- lemmaHalfTail :: proxy xs -> p (x : Half (Tail xs)) -> p (Half (x : xs))
- lemmaMerging :: p (Merge (Half xs) (Half (Tail xs))) -> p xs
- type family xs ++ ys :: [k]
- type family Map f xs :: [k]
- type family Merge xs ys :: [k]
- type family Concat xs :: [k]
- type family Check x xs
- data Expecting a
- data Missing a
- data Ambiguous a
- module Data.Type.Equality
- module Data.Proxy
Documentation
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) | |
NFData (Membership k xs x) |
runMembership :: Membership (y : xs) x -> Either (x :~: y) (Membership xs x) 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
PRIVILEGED: Compare two Membership
s.
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
navNext :: Membership xs y -> Membership (x : xs) y Source
navL :: Membership (Half xs) y -> Membership (x : xs) y Source
navR :: Membership (Half (Tail xs)) y -> Membership (x : xs) y Source
class Member xs x where Source
Member x xs
or x ∈ xs
indicates that x
is an element of xs
.
membership :: Membership xs x Source
lemmaHalfTail :: proxy xs -> p (x : Half (Tail xs)) -> p (Half (x : xs)) Source
GHC can't prove this
module Data.Type.Equality
module Data.Proxy