Copyright	(c) Fumiaki Kinoshita 2015
License	BSD3
Maintainer	Fumiaki Kinoshita <fumiexcel@gmail.com>
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Extensible.Internal

Description

A bunch of combinators that contains magic

Synopsis

Documentation

data Membership xs x Source

The position of x in the type level set xs.

Instances

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 -> ((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 Memberships.

ord :: Int -> Q Exp Source

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

data NavHere xs x where Source

Ensure that the first element of xs is x

Constructors

Here :: NavHere (x : xs) x

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

class Member xs x where Source

Member x xs or x ∈ xs indicates that x is an element of xs.

Methods

membership :: Membership xs x Source

Instances

((~) * (Check k1 Nat x (Lookup k1 x xs)) (Expecting k one), ToInt k one) => Member k xs x

type (∈) x xs = Member xs x Source

Unicode flipped alias for Member

data Nat Source

Type level binary number

Constructors

Zero
DNat Nat
SDNat Nat

Instances

ToInt Nat Zero
ToInt Nat n => ToInt Nat (SDNat n)
ToInt Nat n => ToInt Nat (DNat n)

class ToInt n where Source

Converts type naturals into Word.

Methods

theInt :: proxy n -> Word Source

Instances

ToInt Nat Zero
ToInt Nat n => ToInt Nat (SDNat n)
ToInt Nat n => ToInt Nat (DNat n)

type family Lookup x xs :: [Nat] Source

Lookup types

Equations

Lookup x (x : xs) = Zero : Lookup x xs
Lookup x (y : ys) = MapSucc (Lookup x ys)
Lookup x [] = []

type family Succ x :: Nat Source

The successor of the number

Equations

Succ Zero = SDNat Zero
Succ (DNat n) = SDNat n
Succ (SDNat n) = DNat (Succ n)

type family MapSucc xs :: [Nat] Source

Ideally, it will be 'Map Succ'

Equations

MapSucc [] = []
MapSucc (x : xs) = Succ x : MapSucc xs

type family Half xs :: [k] Source

Interleaved list

Equations

Half [] = []
Half (x : (y : zs)) = x : Half zs
Half (x : []) = `[x]`

type family Tail xs :: [k] Source

Type-level tail

Equations

Tail (x : xs) = xs
Tail [] = []

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

GHC can't prove this

lemmaMerging :: p (Merge (Half xs) (Half (Tail xs))) -> p xs Source

GHC can't prove this

type family xs ++ ys :: [k] infixr 5 Source

Type level ++

Equations

[] ++ ys = ys
(x : xs) ++ ys = x : (xs ++ ys)

type family Map f xs :: [k] Source

Type level map

Equations

Map f [] = []
Map f (x : xs) = f x : Map f xs

type family Merge xs ys :: [k] Source

Type level merging

Equations

Merge (x : xs) (y : ys) = x : (y : Merge xs ys)
Merge xs [] = xs
Merge [] ys = ys

type family Concat xs :: [k] Source

Type level concat

Equations

Concat [] = []
Concat (x : xs) = x ++ Concat xs

type family Check x xs Source

Elaborate the result of Lookup

Equations

Check x `[n]` = Expecting n
Check x [] = Missing x
Check x xs = Ambiguous x

data Expecting a Source

A type sugar to make type error more readable.

data Missing a Source

A type sugar to make type error more readable.

data Ambiguous a Source

A type sugar to make type error more readable.

module Data.Type.Equality

module Data.Proxy