Copyright | (c) Fumiaki Kinoshita 2018 |
---|---|

License | BSD3 |

Maintainer | Fumiaki Kinoshita <fumiexcel@gmail.com> |

Safe Haskell | Trustworthy |

Language | Haskell2010 |

A bunch of combinators that contains magic

- data Membership (xs :: [k]) (x :: k)
- 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 (n :: Nat) (key :: k) (xs :: [Assoc k v]) where ...
- type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where ...
- data Elaborated k v
- 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 :: [k]) (x :: k) 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 # | |

Lift (Membership k xs x) Source # | |

Hashable (Membership k xs x) Source # | |

NFData (Membership k xs x) Source # | |

Pretty (Membership k xs x) Source # | |

getMemberId :: Membership xs x -> Int Source #

get the position as an `Int`

.

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 #

Make up a `Membership`

from an integer.

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 #

type family FindAssoc (n :: Nat) (key :: k) (xs :: [Assoc k v]) where ... Source #

Find a type associated to the specified key.

# Sugar

type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where ... Source #

Make the result more readable

# Miscellaneous

module Data.Type.Equality

module Data.Proxy