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
- reifyMembership :: Word -> (forall x. Membership xs x -> r) -> r
- runMembership :: 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
- 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 Last x :: 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`

.

Eq (Membership k xs x) Source | |

Ord (Membership k xs x) Source | |

Show (Membership k xs x) Source |

getMemberId :: Membership xs x -> Word Source

mkMembership :: Int -> Q Exp Source

Generates a `Membership`

that corresponds to the given ordinal (0-origin).

reifyMembership :: Word -> (forall x. Membership xs x -> r) -> r Source

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.

impossibleMembership :: Membership `[]` x -> r Source

# Member class

class Member xs x where Source

membership :: Membership xs x Source

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 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