Safe Haskell	Safe-Inferred
Language	Haskell2010

Type.Membership

Contents

Membership
Association
Enumeration
Reexports

Synopsis

data Membership (xs :: [k]) (x :: k)
getMemberId :: Membership xs x -> Int
mkMembership :: Int -> Q Exp
leadership :: Membership (x ': xs) x
nextMembership :: Membership xs y -> Membership (x ': xs) y
testMembership :: Membership (y ': xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
impossibleMembership :: Membership '[] x -> r
reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r
class Member xs x
data Assoc k v = k :> v
type (>:) = '(:>)
class Lookup xs k v | k xs -> v where
- association :: Membership xs (k :> v)
type family KeyOf (kv :: Assoc k v) :: k where ...
class pk (KeyOf kv) => KeyIs pk kv
proxyKeyOf :: proxy kv -> Proxy (KeyOf kv)
stringKeyOf :: (IsString a, KnownSymbol (KeyOf kv)) => proxy kv -> a
type family TargetOf (kv :: Assoc k v) :: v where ...
proxyTargetOf :: proxy kv -> Proxy (TargetOf kv)
class pv (TargetOf kv) => TargetIs pv kv
class (pk (KeyOf kv), pv (TargetOf kv)) => KeyTargetAre pk pv kv
class Generate (xs :: [k]) where
- henumerate :: (forall x. Membership xs x -> r -> r) -> r -> r
- hcount :: proxy xs -> Int
- hgenerateList :: Applicative f => (forall x. Membership xs x -> f (h x)) -> f (HList h xs)
class (ForallF c xs, Generate xs) => Forall (c :: k -> Constraint) (xs :: [k]) where
- henumerateFor :: proxy c -> proxy' xs -> (forall x. c x => Membership xs x -> r -> r) -> r -> r
- hgenerateListFor :: Applicative f => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (HList h xs)
type family ForallF (c :: k -> Constraint) (xs :: [k]) :: Constraint where ...
data Proxy (t :: k) = Proxy

Membership

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

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

Instances

Instances details

Lift (Membership xs x :: Type) Source #
Instance details Defined in Type.Membership.Internal Methods lift :: Membership xs x -> Q Exp # liftTyped :: Membership xs x -> Q (TExp (Membership xs x)) #
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 #
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.

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

Compare two Memberships.

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.

class Member xs x Source #

x is a member of xs

Minimal complete definition

membership

Instances

Instances details

(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 #

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

Instances details

(Elaborate k3 (FindAssoc 0 k3 xs) ~ ('Expecting (n :> v) :: Elaborated k1 (Assoc Nat k2)), KnownNat n) => Lookup (xs :: [Assoc k1 k2]) (k3 :: k1) (v :: k2) Source #
Instance details Defined in Type.Membership.Internal Methods association :: Membership xs (k3 :> v) Source #

type family KeyOf (kv :: Assoc k v) :: k where ... Source #

Take the type of the key

Equations

KeyOf (k :> v) = k

class pk (KeyOf kv) => KeyIs pk kv Source #

Constraint applied to KeyOf

Instances

Instances details

pk k2 => KeyIs (pk :: k1 -> Constraint) (k2 :> v2 :: Assoc k1 v1) Source #
Instance details Defined in Type.Membership

proxyKeyOf :: proxy kv -> Proxy (KeyOf kv) Source #

Proxy-level KeyOf. This is useful when using symbolVal.

stringKeyOf :: (IsString a, KnownSymbol (KeyOf kv)) => proxy kv -> a Source #

Get a string from a proxy of Assoc Symbol v.

type family TargetOf (kv :: Assoc k v) :: v where ... Source #

Take the type of the value

Equations

TargetOf (k :> v) = v

proxyTargetOf :: proxy kv -> Proxy (TargetOf kv) Source #

Proxy-level TargetOf.

class pv (TargetOf kv) => TargetIs pv kv Source #

Constraint applied to TargetOf

Instances

Instances details

pv v2 => TargetIs (pv :: v1 -> Constraint) (k2 :> v2 :: Assoc k1 v1) Source #
Instance details Defined in Type.Membership

class (pk (KeyOf kv), pv (TargetOf kv)) => KeyTargetAre pk pv kv Source #

Combined constraint for Assoc

Instances

Instances details

(pk k2, pv v2) => KeyTargetAre (pk :: k1 -> Constraint) (pv :: v1 -> Constraint) (k2 :> v2 :: Assoc k1 v1) Source #
Instance details Defined in Type.Membership

Enumeration

class Generate (xs :: [k]) where Source #

Every type-level list is an instance of Generate.

Methods

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

Enumerate all possible Memberships of xs.

hcount :: proxy xs -> Int Source #

Count the number of memberships.

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

Enumerate Memberships and construct an HList.

Instances

Instances details

Generate ('[] :: [k]) Source #
Instance details Defined in Type.Membership Methods henumerate :: (forall (x :: k0). Membership '[] x -> r -> r) -> r -> r Source # hcount :: proxy '[] -> Int Source # hgenerateList :: Applicative f => (forall (x :: k0). Membership '[] x -> f (h x)) -> f (HList h '[]) Source #
Generate xs => Generate (x ': xs :: [k]) Source #
Instance details Defined in Type.Membership Methods henumerate :: (forall (x0 :: k0). Membership (x ': xs) x0 -> r -> r) -> r -> r Source # hcount :: proxy (x ': xs) -> Int Source # hgenerateList :: Applicative f => (forall (x0 :: k0). Membership (x ': xs) x0 -> f (h x0)) -> f (HList h (x ': xs)) Source #

class (ForallF c xs, Generate xs) => Forall (c :: k -> Constraint) (xs :: [k]) where Source #

Every element in xs satisfies c

Methods

henumerateFor :: proxy c -> proxy' xs -> (forall x. c x => Membership xs x -> r -> r) -> r -> r Source #

Enumerate all possible Memberships of xs with an additional context.

hgenerateListFor :: Applicative f => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (HList h xs) Source #

Instances

Instances details

Forall (c :: k -> Constraint) ('[] :: [k]) Source #
Instance details Defined in Type.Membership Methods henumerateFor :: proxy c -> proxy' '[] -> (forall (x :: k0). c x => Membership '[] x -> r -> r) -> r -> r Source # hgenerateListFor :: Applicative f => proxy c -> (forall (x :: k0). c x => Membership '[] x -> f (h x)) -> f (HList h '[]) Source #
(c x, Forall c xs) => Forall (c :: a -> Constraint) (x ': xs :: [a]) Source #
Instance details Defined in Type.Membership Methods henumerateFor :: proxy c -> proxy' (x ': xs) -> (forall (x0 :: k). c x0 => Membership (x ': xs) x0 -> r -> r) -> r -> r Source # hgenerateListFor :: Applicative f => proxy c -> (forall (x0 :: k). c x0 => Membership (x ': xs) x0 -> f (h x0)) -> f (HList h (x ': xs)) Source #

type family ForallF (c :: k -> Constraint) (xs :: [k]) :: Constraint where ... Source #

HACK: Without this, the constraints are not propagated well.

Equations

ForallF c '[] = ()
ForallF c (x ': xs) = (c x, Forall c xs)

Reexports

data Proxy (t :: k) #

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the undefined :: a idiom.

>>> Proxy :: Proxy (Void, Int -> Int)
Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy Either
Proxy

>>> Proxy :: Proxy Functor
Proxy

>>> Proxy :: Proxy complicatedStructure
Proxy

Constructors

Proxy

Instances

Instances details

Generic1 (Proxy :: k -> Type)	Since: base-4.6.0.0
Instance details Defined in GHC.Generics Associated Types type Rep1 Proxy :: k -> Type # Methods from1 :: forall (a :: k0). Proxy a -> Rep1 Proxy a # to1 :: forall (a :: k0). Rep1 Proxy a -> Proxy a #
Monad (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods (>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b # (>>) :: Proxy a -> Proxy b -> Proxy b # return :: a -> Proxy a #
Functor (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods fmap :: (a -> b) -> Proxy a -> Proxy b # (<$) :: a -> Proxy b -> Proxy a #
Applicative (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods pure :: a -> Proxy a # (<>) :: Proxy (a -> b) -> Proxy a -> Proxy b # liftA2 :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c # (>) :: Proxy a -> Proxy b -> Proxy b # (<*) :: Proxy a -> Proxy b -> Proxy a #
Foldable (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Foldable Methods fold :: Monoid m => Proxy m -> m # foldMap :: Monoid m => (a -> m) -> Proxy a -> m # foldMap' :: Monoid m => (a -> m) -> Proxy a -> m # foldr :: (a -> b -> b) -> b -> Proxy a -> b # foldr' :: (a -> b -> b) -> b -> Proxy a -> b # foldl :: (b -> a -> b) -> b -> Proxy a -> b # foldl' :: (b -> a -> b) -> b -> Proxy a -> b # foldr1 :: (a -> a -> a) -> Proxy a -> a # foldl1 :: (a -> a -> a) -> Proxy a -> a # toList :: Proxy a -> [a] # null :: Proxy a -> Bool # length :: Proxy a -> Int # elem :: Eq a => a -> Proxy a -> Bool # maximum :: Ord a => Proxy a -> a # minimum :: Ord a => Proxy a -> a # sum :: Num a => Proxy a -> a # product :: Num a => Proxy a -> a #
Traversable (Proxy :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Traversable Methods traverse :: Applicative f => (a -> f b) -> Proxy a -> f (Proxy b) # sequenceA :: Applicative f => Proxy (f a) -> f (Proxy a) # mapM :: Monad m => (a -> m b) -> Proxy a -> m (Proxy b) # sequence :: Monad m => Proxy (m a) -> m (Proxy a) #
Alternative (Proxy :: Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods empty :: Proxy a # (<\|>) :: Proxy a -> Proxy a -> Proxy a # some :: Proxy a -> Proxy [a] # many :: Proxy a -> Proxy [a] #
MonadPlus (Proxy :: Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods mzero :: Proxy a # mplus :: Proxy a -> Proxy a -> Proxy a #
NFData1 (Proxy :: Type -> Type)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a -> ()) -> Proxy a -> () #
Hashable1 (Proxy :: Type -> Type)
Instance details Defined in Data.Hashable.Class Methods liftHashWithSalt :: (Int -> a -> Int) -> Int -> Proxy a -> Int #
Bounded (Proxy t)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods minBound :: Proxy t # maxBound :: Proxy t #
Enum (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods succ :: Proxy s -> Proxy s # pred :: Proxy s -> Proxy s # toEnum :: Int -> Proxy s # fromEnum :: Proxy s -> Int # enumFrom :: Proxy s -> [Proxy s] # enumFromThen :: Proxy s -> Proxy s -> [Proxy s] # enumFromTo :: Proxy s -> Proxy s -> [Proxy s] # enumFromThenTo :: Proxy s -> Proxy s -> Proxy s -> [Proxy s] #
Eq (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods (==) :: Proxy s -> Proxy s -> Bool # (/=) :: Proxy s -> Proxy s -> Bool #
Ord (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods compare :: Proxy s -> Proxy s -> Ordering # (<) :: Proxy s -> Proxy s -> Bool # (<=) :: Proxy s -> Proxy s -> Bool # (>) :: Proxy s -> Proxy s -> Bool # (>=) :: Proxy s -> Proxy s -> Bool # max :: Proxy s -> Proxy s -> Proxy s # min :: Proxy s -> Proxy s -> Proxy s #
Read (Proxy t)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods readsPrec :: Int -> ReadS (Proxy t) # readList :: ReadS [Proxy t] # readPrec :: ReadPrec (Proxy t) # readListPrec :: ReadPrec [Proxy t] #
Show (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods showsPrec :: Int -> Proxy s -> ShowS # show :: Proxy s -> String # showList :: [Proxy s] -> ShowS #
Ix (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods range :: (Proxy s, Proxy s) -> [Proxy s] # index :: (Proxy s, Proxy s) -> Proxy s -> Int # unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int # inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool # rangeSize :: (Proxy s, Proxy s) -> Int # unsafeRangeSize :: (Proxy s, Proxy s) -> Int #
Generic (Proxy t)	Since: base-4.6.0.0
Instance details Defined in GHC.Generics Associated Types type Rep (Proxy t) :: Type -> Type # Methods from :: Proxy t -> Rep (Proxy t) x # to :: Rep (Proxy t) x -> Proxy t #
Semigroup (Proxy s)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods (<>) :: Proxy s -> Proxy s -> Proxy s # sconcat :: NonEmpty (Proxy s) -> Proxy s # stimes :: Integral b => b -> Proxy s -> Proxy s #
Monoid (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods mempty :: Proxy s # mappend :: Proxy s -> Proxy s -> Proxy s # mconcat :: [Proxy s] -> Proxy s #
NFData (Proxy a)	Since: deepseq-1.4.0.0
Instance details Defined in Control.DeepSeq Methods rnf :: Proxy a -> () #
Hashable (Proxy a)
Instance details Defined in Data.Hashable.Class Methods hashWithSalt :: Int -> Proxy a -> Int # hash :: Proxy a -> Int #
type Rep1 (Proxy :: k -> Type)
Instance details Defined in GHC.Generics type Rep1 (Proxy :: k -> Type) = D1 ('MetaData "Proxy" "Data.Proxy" "base" 'False) (C1 ('MetaCons "Proxy" 'PrefixI 'False) (U1 :: k -> Type))
type Rep (Proxy t)
Instance details Defined in GHC.Generics type Rep (Proxy t) = D1 ('MetaData "Proxy" "Data.Proxy" "base" 'False) (C1 ('MetaCons "Proxy" 'PrefixI 'False) (U1 :: Type -> Type))