Copyright | (c) Fumiaki Kinoshita 2018 |
---|---|

License | BSD3 |

Maintainer | Fumiaki Kinoshita <fumiexcel@gmail.com> |

Safe Haskell | None |

Language | Haskell2010 |

## Synopsis

- class (Functor f, Profunctor p) => Extensible f p (t :: [k] -> (k -> Type) -> Type) where
- type ExtensibleConstr t (xs :: [k]) (h :: k -> Type) (x :: k) :: Constraint
- pieceAt :: ExtensibleConstr t xs h x => Membership xs x -> Optic' p f (t xs h) (h x)

- piece :: (x ∈ xs, Extensible f p t, ExtensibleConstr t xs h x) => Optic' p f (t xs h) (h x)
- pieceAssoc :: (Lookup xs k v, Extensible f p t, ExtensibleConstr t xs h (k :> v)) => Optic' p f (t xs h) (h (k :> v))
- itemAt :: (Wrapper h, Extensible f p t, ExtensibleConstr t xs h x) => Membership xs x -> Optic' p f (t xs h) (Repr h x)
- item :: (Wrapper h, Extensible f p t, x ∈ xs, ExtensibleConstr t xs h x) => proxy x -> Optic' p f (t xs h) (Repr h x)
- itemAssoc :: (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t xs h (k :> v)) => proxy k -> Optic' p f (t xs h) (Repr h (k :> v))
- itemKey :: forall k v xs h f p t. (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t xs h (k :> v)) => Optic' p f (t xs h) (Repr h (k :> v))
- data Membership (xs :: [k]) (x :: k) :: forall k. [k] -> k -> Type
- mkMembership :: Int -> Q Exp
- getMemberId :: Membership xs x -> Int
- compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
- leadership :: Membership (x ': xs) x
- class Member (xs :: [k]) (x :: k) where
- membership :: Membership xs x

- type (∈) (x :: k) (xs :: [k]) = Member xs x
- type family FindType (x :: k) (xs :: [k]) :: [Nat] where ...
- class Generate (xs :: [k]) where
- henumerate :: (forall (x :: k). Membership xs x -> r -> r) -> r -> r
- hcount :: proxy xs -> Int
- hgenerateList :: Applicative f => (forall (x :: k). 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 :: k). c x => Membership xs x -> r -> r) -> r -> r
- hgenerateListFor :: Applicative f => proxy c -> (forall (x :: k). c x => Membership xs x -> f (h x)) -> f (HList h xs)

- type family ForallF (c :: k -> Constraint) (xs :: [k]) :: Constraint where ...
- data Assoc k v = k :> v
- type (>:) = ((:>) :: k -> v -> Assoc k v)
- class Lookup (xs :: [Assoc k v]) (k1 :: k) (v1 :: v) | k1 xs -> v1 where
- association :: Membership xs (k1 :> v1)

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

# Class

class (Functor f, Profunctor p) => Extensible f p (t :: [k] -> (k -> Type) -> Type) where Source #

This class allows us to use `pieceAt`

for both sums and products.

type ExtensibleConstr t (xs :: [k]) (h :: k -> Type) (x :: k) :: Constraint Source #

pieceAt :: ExtensibleConstr t xs h x => Membership xs x -> Optic' p f (t xs h) (h x) Source #

## Instances

piece :: (x ∈ xs, Extensible f p t, ExtensibleConstr t xs h x) => Optic' p f (t xs h) (h x) Source #

Accessor for an element.

pieceAssoc :: (Lookup xs k v, Extensible f p t, ExtensibleConstr t xs h (k :> v)) => Optic' p f (t xs h) (h (k :> v)) Source #

Like `piece`

, but reckon membership from its key.

itemAt :: (Wrapper h, Extensible f p t, ExtensibleConstr t xs h x) => Membership xs x -> Optic' p f (t xs h) (Repr h x) Source #

Access a specified element through a wrapper.

item :: (Wrapper h, Extensible f p t, x ∈ xs, ExtensibleConstr t xs h x) => proxy x -> Optic' p f (t xs h) (Repr h x) Source #

Access an element through a wrapper.

itemAssoc :: (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t xs h (k :> v)) => proxy k -> Optic' p f (t xs h) (Repr h (k :> v)) Source #

Access an element specified by the key type through a wrapper.

itemKey :: forall k v xs h f p t. (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t xs h (k :> v)) => Optic' p f (t xs h) (Repr h (k :> v)) Source #

Access an element specified by the key type through a wrapper.

# Membership

data Membership (xs :: [k]) (x :: k) :: forall k. [k] -> k -> Type #

A witness that of `x`

is a member of a type level set `xs`

.

## Instances

mkMembership :: Int -> Q Exp #

Generates a `Membership`

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

getMemberId :: Membership xs x -> Int #

get the position as an `Int`

.

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

Compare two `Membership`

s.

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

This `Membership`

points to the first element

# Member

class Member (xs :: [k]) (x :: k) where #

`x`

is a member of `xs`

membership :: Membership xs x #

## Instances

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

Defined in Type.Membership.Internal membership :: Membership xs x # |

# Generation

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

Every type-level list is an instance of `Generate`

.

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

Enumerate all possible `Membership`

s of `xs`

.

Count the number of memberships.

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

Enumerate `Membership`

s and construct an `HList`

.

## Instances

Generate ([] :: [k]) | |

Defined in Type.Membership henumerate :: (forall (x :: k0). Membership [] x -> r -> r) -> r -> r # hgenerateList :: Applicative f => (forall (x :: k0). Membership [] x -> f (h x)) -> f (HList h []) # | |

Generate xs => Generate (x ': xs :: [k]) | |

Defined in Type.Membership henumerate :: (forall (x0 :: k0). Membership (x ': xs) x0 -> r -> r) -> r -> r # hcount :: proxy (x ': xs) -> Int # hgenerateList :: Applicative f => (forall (x0 :: k0). Membership (x ': xs) x0 -> f (h x0)) -> f (HList h (x ': xs)) # |

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

Every element in `xs`

satisfies `c`

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

Enumerate all possible `Membership`

s of `xs`

with an additional context.

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

## Instances

Forall (c :: k -> Constraint) ([] :: [k]) | |

Defined in Type.Membership henumerateFor :: proxy c -> proxy' [] -> (forall (x :: k0). c x => Membership [] x -> r -> r) -> r -> r # hgenerateListFor :: Applicative f => proxy c -> (forall (x :: k0). c x => Membership [] x -> f (h x)) -> f (HList h []) # | |

(c x, Forall c xs) => Forall (c :: a -> Constraint) (x ': xs :: [a]) | |

Defined in Type.Membership henumerateFor :: proxy c -> proxy' (x ': xs) -> (forall (x0 :: k). c x0 => Membership (x ': xs) x0 -> r -> r) -> r -> r # hgenerateListFor :: Applicative f => proxy c -> (forall (x0 :: k). c x0 => Membership (x ': xs) x0 -> f (h x0)) -> f (HList h (x ': xs)) # |

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

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

ForallF (c :: k -> Constraint) ([] :: [k]) = () | |

ForallF (c :: k -> Constraint) (x ': xs :: [k]) = (c x, Forall c xs) |

# Association

The kind of key-value pairs

k :> v infix 0 |

## Instances

class Lookup (xs :: [Assoc k v]) (k1 :: k) (v1 :: v) | k1 xs -> v1 where #

is essentially identical to `Lookup`

xs k v`(k :> v) ∈ xs`

, but the type `v`

is inferred from `k`

and `xs`

.

association :: Membership xs (k1 :> v1) #

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

Defined in Type.Membership.Internal association :: Membership xs (k2 :> v2) # |