| Copyright | (C) 2017 Alexey Vagarenko |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Alexey Vagarenko (vagarenko@gmail.com) |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Type.List
Description
- class KnownNats (ns :: [Nat]) where
- type family MkCtx (kx :: Type) (kctx :: Type) (ctx :: kctx) (x :: kx) :: Constraint where ...
- class DemoteWith (kx :: Type) (kctx :: Type) (ctx :: kctx) (xs :: [kx]) where
Documentation
class KnownNats (ns :: [Nat]) where Source #
Demote type-level list of Nat.
Minimal complete definition
type family MkCtx (kx :: Type) (kctx :: Type) (ctx :: kctx) (x :: kx) :: Constraint where ... Source #
Make a constraint for type x :: kx from TyFun, or partially applied constraint, or make an empty constraint.
Equations
| MkCtx kx (kx ~> Constraint) ctx x = Apply ctx x | |
| MkCtx kx (kx -> Constraint) ctx x = ctx x | |
| MkCtx _ Constraint () _ = () | |
| MkCtx _ Type () _ = () |
class DemoteWith (kx :: Type) (kctx :: Type) (ctx :: kctx) (xs :: [kx]) where Source #
Demote a type-level list to value-level list with a type-indexed function.
The function takes list element as type parameter x and applies constraints ctx for that element.
Minimal complete definition
Methods
demoteWith :: (forall (x :: kx). MkCtx kx kctx ctx x => Proxy x -> a) -> [a] Source #
Instances
| DemoteWith kx kctx ctxs ([] kx) Source # | |
| (DemoteWith kx kctx ctx xs, MkCtx kx kctx ctx x) => DemoteWith kx kctx ctx ((:) kx x xs) Source # | |