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
- getMemberId :: Membership xs x -> Word
- runMembership :: Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
- 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
- data h :* s where
- class LookupTree (Head (Lookup x xs)) xs x => 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 ListIndex n xs :: k
- class LookupTree n xs x | n xs -> x where
- lookupTree :: Functor f => proxy n -> (h x -> f (h x)) -> (h :* xs) -> f (h :* xs)

- type family Succ x :: Nat
- type family MapSucc xs :: [Nat]
- type family Pred n :: Nat
- type family Div2 n :: Nat
- type family Half xs :: [k]
- type family Head 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) |

getMemberId :: Membership xs x -> Word 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

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

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

The extensible product type

Typeable ((k -> *) -> [k] -> *) ((:*) k) | |

WrapForall k * Eq h xs => Eq ((:*) k h xs) | |

(Eq ((:*) k h xs), WrapForall k * Ord h xs) => Ord ((:*) k h xs) | |

WrapForall k * Show h xs => Show ((:*) k h xs) | |

WrapForall k * Monoid h xs => Monoid ((:*) k h xs) | |

WrapForall k * Binary h xs => Binary ((:*) k h xs) |

class LookupTree (Head (Lookup x xs)) xs x => Member xs x where Source

membership :: Membership xs x Source

Type level binary number

Converts type naturals into `Word`

.

class LookupTree n xs x | n xs -> x where Source

lookupTree :: Functor f => proxy n -> (h x -> f (h x)) -> (h :* xs) -> f (h :* xs) Source

LookupTree k Zero ((:) k x xs) x | |

LookupTree k (Pred n) (Half k (Tail k xs)) x => LookupTree k (DNat n) ((:) k t xs) x | |

LookupTree k n (Half k xs) x => LookupTree k (SDNat n) ((:) k t xs) x |

lemmaHalfTail :: proxy xs -> p (x : Half (Tail xs)) -> p (Half (x : xs)) Source

GHC can't prove this

Elaborate the result of `Lookup`

module Data.Type.Equality

module Data.Proxy