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

Language | Haskell2010 |

- data Nat
- class NatToInt (n :: Nat) where
- class IndexWitnesses (is :: [Nat]) where
- 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 ts :: Constraint where ...
- type family AllSatisfied cs t :: Constraint where ...
- type family AllAllSat cs ts :: Constraint where ...

# Documentation

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

corresponds to the actual natural numbers.

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

indexWitnesses :: [Int] Source #

IndexWitnesses ([] Nat) Source # | |

(IndexWitnesses is, NatToInt i) => IndexWitnesses ((:) Nat i is) 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 occurence 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 ts :: 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) |

type family AllSatisfied cs t :: Constraint where ... Source #

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

AllSatisfied '[] t = () | |

AllSatisfied (c ': cs) t = (c t, AllSatisfied cs t) |

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