membership-0: Indices for type level lists

Safe HaskellTrustworthy
LanguageHaskell2010

Type.Membership.Internal

Contents

Synopsis

Membership

data Membership (xs :: [k]) (x :: k) Source #

A witness that of x is a member of a type level set xs.

Instances
Eq (Membership xs x) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

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

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

Ord (Membership xs x) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

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

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

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

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

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

max :: Membership xs x -> Membership xs x -> Membership xs x #

min :: Membership xs x -> Membership xs x -> Membership xs x #

Show (Membership xs x) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

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

show :: Membership xs x -> String #

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

Semigroup (Membership xs x) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

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

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

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

Lift (Membership xs x) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

lift :: Membership xs x -> Q Exp #

NFData (Membership xs x) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

rnf :: Membership xs x -> () #

Hashable (Membership xs x) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

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

hash :: Membership xs x -> Int #

Pretty (Membership xs x) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

pretty :: Membership xs x -> Doc ann #

prettyList :: [Membership xs x] -> Doc ann #

getMemberId :: Membership xs x -> Int Source #

get the position as an Int.

mkMembership :: Int -> Q Exp Source #

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

leadership :: Membership (x ': xs) x Source #

This Membership points to the first element

nextMembership :: Membership xs y -> Membership (x ': xs) y Source #

The next membership

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

impossibleMembership :: Membership '[] x -> r Source #

There is no Membership of an empty list.

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

Make up a Membership from an integer.

Member class

class Member xs x where Source #

x is a member of xs

Methods

membership :: Membership xs x Source #

Instances
(Elaborate x (FindType x xs) ~ (Expecting pos :: Elaborated k Nat), KnownNat pos) => Member (xs :: [k]) (x :: k) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

membership :: Membership xs x Source #

type (∈) x xs = Member xs x Source #

Unicode flipped alias for Member

type family FindType (x :: k) (xs :: [k]) :: [Nat] where ... Source #

FindType types

Equations

FindType x (x ': xs) = 0 ': MapSucc (FindType x xs) 
FindType x (y ': ys) = MapSucc (FindType x ys) 
FindType x '[] = '[] 

Association

data Assoc k v Source #

The kind of key-value pairs

Constructors

k :> v infix 0 

type (>:) = (:>) Source #

A synonym for (:>)

class Lookup xs k v | k xs -> v where Source #

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

Methods

association :: Membership xs (k :> v) Source #

Instances
(Elaborate k2 (FindAssoc 0 k2 xs) ~ (Expecting (n :> v2) :: Elaborated k1 (Assoc Nat v1)), KnownNat n) => Lookup (xs :: [Assoc k1 v1]) (k2 :: k1) (v2 :: v1) Source # 
Instance details

Defined in Type.Membership.Internal

Methods

association :: Membership xs (k2 :> v2) Source #

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

Find a type associated to the specified key.

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 ... Source #

Make the result more readable

Equations

Elaborate k '[] = Missing k 
Elaborate k '[x] = Expecting x 
Elaborate k xs = Duplicate k 

data Elaborated k v Source #

A readable type search result

Constructors

Expecting v 
Missing k 
Duplicate k 

HList

data HList (h :: k -> *) (xs :: [k]) where Source #

Constructors

HNil :: HList h '[] 
HCons :: h x -> HList h xs -> HList h (x ': xs) infixr 5 

hfoldrWithIndex :: forall h r xs. (forall x. Membership xs x -> h x -> r -> r) -> r -> HList h xs -> r Source #

htraverseWithIndex :: forall f g h xs. Applicative f => (forall x. Membership xs x -> g x -> f (h x)) -> HList g xs -> f (HList h xs) Source #

Miscellaneous

module Data.Proxy