Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- data Nat
- class NatToInt (n :: Nat) where
- class IndexWitnesses (is :: [Nat]) where
- indexWitnesses :: [Int]

- type family Fst (a :: (k1, k2)) where ...
- type family Snd (a :: (k1, k2)) where ...
- type family RLength xs where ...
- type family RIndex (r :: k) (rs :: [k]) :: Nat where ...
- type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where ...
- type family RDelete r rs where ...
- type family RecAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constraint where ...
- type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...
- type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint where ...
- class AllSatisfied cs t
- type family AllAllSat cs ts :: Constraint where ...
- type family ApplyToField (t :: Type -> Type) (a :: k1) = (r :: k1) | r -> t a where ...
- type family MapTyCon t xs = r | r -> xs where ...
- class Coercible (f x) (g x) => Similar f g (x :: k)

# Documentation

A mere approximation of the natural numbers. And their image as lifted by
`-XDataKinds`

corresponds to the actual natural numbers.

#### Instances

RecSubset (Rec :: (k -> Type) -> [k] -> Type) ('[] :: [k]) (ss :: [k]) ('[] :: [Nat]) Source # | |

Defined in Data.Vinyl.Lens type RecSubsetFCtx Rec f Source # rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f '[] -> g (Rec f '[])) -> Rec f ss -> g (Rec f ss) Source # rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f '[] Source # rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f '[] -> Rec f ss -> Rec f ss Source # | |

(RElem r ss i, RSubset rs ss is) => RecSubset (Rec :: (k -> Type) -> [k] -> Type) (r ': rs :: [k]) (ss :: [k]) (i ': is) Source # | |

Defined in Data.Vinyl.Lens type RecSubsetFCtx Rec f Source # rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss) Source # rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f (r ': rs) Source # rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f (r ': rs) -> Rec f ss -> Rec f ss Source # | |

IndexWitnesses ('[] :: [Nat]) Source # | |

Defined in Data.Vinyl.TypeLevel indexWitnesses :: [Int] Source # | |

(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) Source # | |

Defined in Data.Vinyl.TypeLevel indexWitnesses :: [Int] Source # |

class IndexWitnesses (is :: [Nat]) where Source #

indexWitnesses :: [Int] Source #

#### Instances

IndexWitnesses ('[] :: [Nat]) Source # | |

Defined in Data.Vinyl.TypeLevel indexWitnesses :: [Int] Source # | |

(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) Source # | |

Defined in Data.Vinyl.TypeLevel indexWitnesses :: [Int] Source # |

type family Fst (a :: (k1, k2)) where ... Source #

Project the first component of a type-level tuple.

Fst '(x, y) = x |

type family Snd (a :: (k1, k2)) where ... Source #

Project the second component of a type-level tuple.

Snd '(x, y) = y |

type family RIndex (r :: k) (rs :: [k]) :: Nat where ... Source #

A partial relation that gives the index of a value in a list.

type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where ... Source #

A partial relation that gives the indices of a sublist in a larger list.

type family RDelete r rs where ... Source #

Remove the first occurrence of a type from a type-level list.

type family RecAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constraint where ... Source #

A constraint-former which applies to every field in a record.

type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint where ... Source #

Constraint that all types in a type-level list satisfy a constraint.

AllConstrained c '[] = () | |

AllConstrained c (t ': ts) = (c t, AllConstrained c ts) |

class AllSatisfied cs t Source #

Constraint that each Constraint in a type-level list is satisfied by a particular type.

#### Instances

AllSatisfied ('[] :: [k2]) (t :: k1) Source # | |

Defined in Data.Vinyl.TypeLevel | |

(c t, AllSatisfied cs t) => AllSatisfied (c ': cs :: [k -> Constraint]) (t :: k) Source # | |

Defined in Data.Vinyl.TypeLevel |

type family AllAllSat cs ts :: Constraint where ... Source #

Constraint that all types in a type-level list satisfy each constraint from a list of constraints.

`AllAllSat cs ts`

should be equivalent to ```
AllConstrained
(AllSatisfied cs) ts
```

if partial application of type families were
legal.

AllAllSat cs '[] = () | |

AllAllSat cs (t ': ts) = (AllSatisfied cs t, AllAllSat cs ts) |

type family ApplyToField (t :: Type -> Type) (a :: k1) = (r :: k1) | r -> t a where ... Source #

Apply a type constructor to a record index. Record indexes are
either `Type`

or `(`

. In the latter case, the type
constructor is applied to the second component of the tuple.`Symbol`

, `Type`

)

ApplyToField t '(s, x) = '(s, t x) | |

ApplyToField t x = t x |