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

Eq (Membership k xs x)

Methods

(==) :: Membership k xs x -> Membership k xs x -> Bool

(/=) :: Membership k xs x -> Membership k xs x -> Bool

Ord (Membership k xs x)

Methods

compare :: Membership k xs x -> Membership k xs x -> Ordering

(<) :: Membership k xs x -> Membership k xs x -> Bool

(<=) :: Membership k xs x -> Membership k xs x -> Bool

(>) :: Membership k xs x -> Membership k xs x -> Bool

(>=) :: Membership k xs x -> Membership k xs x -> Bool

max :: Membership k xs x -> Membership k xs x -> Membership k xs x

min :: Membership k xs x -> Membership k xs x -> Membership k xs x

Show (Membership k xs x)

Methods

showsPrec :: Int -> Membership k xs x -> ShowS

show :: Membership k xs x -> String

showList :: [Membership k xs x] -> ShowS

Semigroup (Membership k xs x)

Methods

(<>) :: Membership k xs x -> Membership k xs x -> Membership k xs x

sconcat :: NonEmpty (Membership k xs x) -> Membership k xs x

stimes :: Integral b => b -> Membership k xs x -> Membership k xs x

NFData (Membership k xs x)

Methods

rnf :: Membership k xs x -> ()

Hashable (Membership k xs x)

Methods

hashWithSalt :: Int -> Membership k xs x -> Int

hash :: Membership k xs x -> Int

getMemberId :: Membership xs x -> Int

mkMembership :: Int -> Q Exp

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

reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r

leadership :: 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.

impossibleMembership :: Membership '[] x -> r

There is no Membership of an empty list.

here :: Membership (x ': xs) x

The Membership points the first element

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

The next membership

Member class

class Member xs x where

x is a member of xs

Minimal complete definition

membership

Methods

membership :: Membership xs x

Instances

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

Methods

membership :: Membership xs x 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 :: k) (xs :: [k]) :: [Nat] where ...

FindType types

Equations

FindType x (x ': xs) = 0 ': 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

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

Associated Types

type Repr (Field k v h) (h :: Field k v h -> *) (v :: Field k v h) :: *

Methods

_Wrapper :: (Functor f, Profunctor p) => Optic' * * p f (h v) (Repr (Field k v h) h v)

type Repr (Assoc k v) (Field k v h) kv

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

type (>:) = (:>)

A synonym for (:>)

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.

Minimal complete definition

association

Methods

association :: Membership xs (k :> v)

Instances

((~) (Elaborated k (Assoc Nat v)) (Elaborate (Assoc Nat v) k k1 (FindAssoc v k 0 k1 xs)) (Expecting k (Assoc Nat v) ((:>) Nat v n v1)), KnownNat n) => Associate v k k1 v1 xs

Methods

association :: Membership (Assoc v1 k1) xs ((v1 :> k1) xs v)

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

Equations

FindAssoc n k ((k :> v) ': xs) = (n :> v) ': FindAssoc (1 + n) k xs

FindAssoc n k ((k' :> v) ': xs) = FindAssoc (1 + n) k xs

FindAssoc n k '[] = '[]

Sugar

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

Equations

Elaborate k '[] = Missing k

Elaborate k '[x] = Expecting x

Elaborate k xs = Duplicate k

data Elaborated k v

A readable type search result

Constructors

Expecting v

Missing k

Duplicate k

Miscellaneous

type family Head (xs :: [k]) :: k where ...

Equations

Head (x ': xs) = x

type family Last (x :: [k]) :: k where ...

Equations

Last '[x] = x

Last (x ': xs) = Last xs

module Data.Type.Equality

module Data.Proxy