Data.Extensible.Internal

A bunch of combinators that contains magic

Membership

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)

getMemberId :: Membership xs x -> Word

mkMembership :: Int -> Q Exp

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

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)

Compare two Memberships.

Member class

class Member xs x where

Methods

membership :: Membership xs x

Instances

((~) (Elaborated k Nat) (Elaborate k Nat x (FindType k x xs)) (Expecting k Nat pos), KnownPosition Nat pos) => Member k xs x

remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r

Remember that Member xs x from Membership.

type (∈) x xs = Member xs x

Unicode flipped alias for Member

type family FindType x xs :: [Nat]

FindType types

Equations

FindType x (x : xs) = Zero : FindType x xs

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

FindType x [] = []

Association

data Assoc k v

The kind of key-value pairs

Constructors

k :> v infix 0

Instances

Associate k k1 k2 v xs => Associated (Assoc k k) xs ((:>) k k k v)

Wrapper k h => Wrapper (Assoc k k) (Field k k h)

type Repr (Assoc k1 k) (Field k k1 h) kv = Repr k h (AssocValue k k1 kv)

class Associate k v xs | k xs -> v where

Associate k v xs is essentially identical to (k :> v) ∈ xs , but the type v is inferred from k and xs.

Methods

association :: Membership xs (k :> v)

Instances

((~) (Elaborated k (Assoc Nat k1)) (Elaborate k (Assoc Nat k1) k2 (FindAssoc k1 k k1 k2 xs)) (Expecting k (Assoc Nat k1) ((:>) Nat k1 n v)), KnownPosition Nat n) => Associate k k k v xs

type family FindAssoc key xs

Equations

FindAssoc k ((k :> v) : xs) = (Zero :> v) : MapSuccKey (FindAssoc k xs)

FindAssoc k ((k' :> v) : xs) = MapSuccKey (FindAssoc k xs)

FindAssoc k [] = []

Sugar

type family Elaborate key xs :: Elaborated k v

Equations

Elaborate k [] = Missing k

Elaborate k `[x]` = Expecting x

Elaborate k xs = Duplicate k

data Elaborated k v

Constructors

Expecting v

Missing k

Duplicate k

Tree navigation

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

Miscellaneous

data Nat

Type level binary number

Constructors

Zero

DNat Nat

SDNat Nat

Instances

KnownPosition Nat Zero

KnownPosition Nat n => KnownPosition Nat (SDNat n)

KnownPosition Nat n => KnownPosition Nat (DNat n)

class KnownPosition n where

Converts type naturals into Word.

Methods

theInt :: proxy n -> Word

Instances

KnownPosition Nat Zero

KnownPosition Nat n => KnownPosition Nat (SDNat n)

KnownPosition Nat n => KnownPosition Nat (DNat n)

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 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 [] = []

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

module Data.Type.Equality

module Data.Proxy