Copyright	(c) Fumiaki Kinoshita 2018
License	BSD3
Maintainer	Fumiaki Kinoshita <fumiexcel@gmail.com>
Safe Haskell	Trustworthy
Language	Haskell2010

Data.Extensible.Internal

Contents

Membership
Member class
Association
Sugar
Miscellaneous

Description

A bunch of combinators that contains magic

Synopsis

data Membership (xs :: [k]) (x :: k)
getMemberId :: Membership xs x -> Int
mkMembership :: Int -> Q Exp
reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r
leadership :: 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
here :: Membership (x ': xs) x
navNext :: Membership xs y -> Membership (x ': xs) y
class Member xs x where
- membership :: Membership xs x
remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r
type (∈) x xs = Member xs x
type family FindType (x :: k) (xs :: [k]) :: [Nat] where ...
data Assoc k v = k :> v
type (>:) = (:>)
class Associate k v xs | k xs -> v where
- association :: Membership xs (k :> v)
type family FindAssoc (n :: Nat) (key :: k) (xs :: [Assoc k v]) where ...
type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where ...
data Elaborated k v
- = Expecting v
- | Missing k
- | Duplicate k
type family Head (xs :: [k]) :: k where ...
type family Last (x :: [k]) :: k where ...
module Data.Type.Equality
module Data.Proxy

Membership

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

The position of x in the type level set xs.

Instances

Eq (Membership xs x) Source #
Instance details Defined in Data.Extensible.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 Data.Extensible.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 Data.Extensible.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 Data.Extensible.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 Data.Extensible.Internal Methods lift :: Membership xs x -> Q Exp #
Hashable (Membership xs x) Source #
Instance details Defined in Data.Extensible.Internal Methods hashWithSalt :: Int -> Membership xs x -> Int # hash :: Membership xs x -> Int #
NFData (Membership xs x) Source #
Instance details Defined in Data.Extensible.Internal Methods rnf :: Membership xs x -> () #
Pretty (Membership xs x) Source #
Instance details Defined in Data.Extensible.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).

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

Make up a Membership from an integer.

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

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

The Membership points the first element

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

The next membership

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 Data.Extensible.Internal Methods membership :: Membership xs x Source #

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

Remember that Member xs x from Membership.

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 ': 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

Instances

Wrapper h => Wrapper (Field h :: Assoc k v -> Type) Source #
Instance details Defined in Data.Extensible.Field Associated Types type Repr (Field h) v :: Type Source # Methods _Wrapper :: (Functor f, Profunctor p) => Optic' p f (Field h v0) (Repr (Field h) v0) Source # wrap :: Repr (Field h) v0 -> Field h v0 Source # unwrap :: Field h v0 -> Repr (Field h) v0 Source #
Forall (KeyValue KnownSymbol (Instance1 ToJSON h)) xs => ToJSON (Nullable (Field h :: Assoc Symbol v -> Type) :* xs) Source #
Instance details Defined in Data.Extensible.Dictionary Methods toJSON :: (Nullable (Field h) :* xs) -> Value # toEncoding :: (Nullable (Field h) :* xs) -> Encoding # toJSONList :: [Nullable (Field h) :* xs] -> Value # toEncodingList :: [Nullable (Field h) :* xs] -> Encoding #
Forall (KeyValue KnownSymbol (Instance1 ToJSON h)) xs => ToJSON ((Field h :: Assoc Symbol v -> Type) :* xs) Source #
Instance details Defined in Data.Extensible.Dictionary Methods toJSON :: (Field h :* xs) -> Value # toEncoding :: (Field h :* xs) -> Encoding # toJSONList :: [Field h :* xs] -> Value # toEncodingList :: [Field h :* xs] -> Encoding #
Forall (KeyValue KnownSymbol (Instance1 FromJSON h)) xs => FromJSON (Nullable (Field h :: Assoc Symbol v -> Type) :* xs) Source #
Instance details Defined in Data.Extensible.Dictionary Methods parseJSON :: Value -> Parser (Nullable (Field h) :* xs) # parseJSONList :: Value -> Parser [Nullable (Field h) :* xs] #
Forall (KeyValue KnownSymbol (Instance1 FromJSON h)) xs => FromJSON ((Field h :: Assoc Symbol v -> Type) :* xs) Source #	`parseJSON Null` is called for missing fields.
Instance details Defined in Data.Extensible.Dictionary Methods parseJSON :: Value -> Parser (Field h :* xs) # parseJSONList :: Value -> Parser [Field h :* xs] #
Forall (KeyValue KnownSymbol (Instance1 FromField h)) xs => FromNamedRecord ((Field h :: Assoc Symbol v -> Type) :* xs) Source #
Instance details Defined in Data.Extensible.Dictionary Methods parseNamedRecord :: NamedRecord -> Parser (Field h :* xs) #
Forall (KeyValue KnownSymbol (Instance1 ToField h)) xs => ToNamedRecord ((Field h :: Assoc Symbol v -> Type) :* xs) Source #
Instance details Defined in Data.Extensible.Dictionary Methods toNamedRecord :: (Field h :* xs) -> NamedRecord #
type Repr (Field h :: Assoc k v -> Type) (kv :: Assoc k v) Source #
Instance details Defined in Data.Extensible.Field type Repr (Field h :: Assoc k v -> Type) (kv :: Assoc k v) = Repr h (AssocValue kv)

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

A synonym for (:>)

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

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

Instances

(Elaborate k2 (FindAssoc 0 k2 xs) ~ (Expecting (n :> v2) :: Elaborated k1 (Assoc Nat v1)), KnownNat n) => Associate (k2 :: k1) (v2 :: v1) (xs :: [Assoc k1 v1]) Source #
Instance details Defined in Data.Extensible.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

Miscellaneous

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

First element

Equations

Head (x ': xs) = x

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

Last element

Equations

Last '[x] = x
Last (x ': xs) = Last xs

module Data.Type.Equality

module Data.Proxy