Data.Extensible.Internal

A bunch of combinators that contains magic

Documentation

data Membership xs x

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)

getMemberId :: Membership xs x -> Word

runMembership :: Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r

Embodies a type equivalence to ensure that the Membership points the first element.

compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)

PRIVILEGED: Compare two Memberships.

ord :: Int -> Q Exp

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

data NavHere xs x where

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

PRIVILEGED: Navigate a tree.

here :: Membership (x : xs) x

The Membership points the first element

navNext :: Membership xs y -> Membership (x : xs) y

The next membership

navL :: Membership (Half xs) y -> Membership (x : xs) y

Describes the relation of Membership within a tree

navR :: Membership (Half (Tail xs)) y -> Membership (x : xs) y

Describes the relation of Membership within a tree

data h :* s where

The extensible product type

Constructors

Nil :: h :* []

Tree :: !(h x) -> (h :* Half xs) -> (h :* Half (Tail xs)) -> h :* (x : xs)

Instances

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

Methods

membership :: Membership xs x

Instances

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

type (∈) x xs = Member xs x

Unicode flipped alias for Member

data Nat

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

Converts type naturals into Word.

Methods

theInt :: proxy n -> Word

Instances

ToInt Nat Zero

ToInt Nat n => ToInt Nat (SDNat n)

ToInt Nat n => ToInt Nat (DNat n)

type family Lookup x xs :: [Nat]

Lookup types

Equations

Lookup x (x : xs) = Zero : Lookup x xs

Lookup x (y : ys) = MapSucc (Lookup x ys)

Lookup x [] = []

type family ListIndex n xs :: k

Lookup types

Equations

ListIndex Zero (x : xs) = x

ListIndex (SDNat n) (y : xs) = ListIndex n (Half xs)

ListIndex (DNat n) xs = ListIndex n (Half xs)

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

Methods

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

Instances

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

type family Succ x :: Nat

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]

Ideally, it will be 'Map Succ'

Equations

MapSucc [] = []

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

type family Pred n :: Nat

Equations

Pred (SDNat Zero) = Zero

Pred (SDNat n) = DNat n

Pred (DNat n) = SDNat (Pred n)

Pred Zero = Zero

type family Div2 n :: Nat

Equations

Div2 (SDNat n) = n

Div2 (DNat n) = n

Div2 Zero = Zero

type family Half xs :: [k]

Interleaved list

Equations

Half [] = []

Half (x : (y : zs)) = x : Half zs

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

type family Head xs :: k

Equations

Head (x : xs) = x

type family Tail xs :: [k]

Type-level tail

Equations

Tail (x : xs) = xs

Tail [] = []

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

GHC can't prove this

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

GHC can't prove this

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

Type level ++

Equations

[] ++ ys = ys

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

type family Map f xs :: [k]

Type level map

Equations

Map f [] = []

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

type family Merge xs ys :: [k]

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]

Type level concat

Equations

Concat [] = []

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

type family Check x xs

Elaborate the result of Lookup

Equations

Check x `[n]` = Expecting n

Check x [] = Missing x

Check x xs = Ambiguous x

data Expecting a

A type sugar to make type error more readable.

data Missing a

A type sugar to make type error more readable.

data Ambiguous a

A type sugar to make type error more readable.

module Data.Type.Equality

module Data.Proxy