| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.TypeLevel
Synopsis
- type family All (p :: k -> Constraint) (as :: [k]) where ...
- type family If (b :: Bool) (l :: k) (r :: k) :: k where ...
- type family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l where ...
- type family Foldr' (c :: Function k (Function l l -> Type) -> Type) (n :: l) (as :: [k]) :: l where ...
- type family Map (f :: Function k l -> Type) (as :: [k]) :: [l] where ...
- data ConsMap0 (a :: Function k l -> Type) (b :: Function k (Function [l] [l] -> Type))
- data ConsMap1 (a :: Function k l -> Type) (b :: k) (c :: Function [l] [l])
- type family Constant (b :: l) (as :: [k]) :: [l] where ...
- type Arrows (as :: [Type]) r = Foldr (->) r as
- type Products (as :: [Type]) = Foldr (,) () as
- data StrictPair a b = Pair a b
- type StrictProducts (as :: [Type]) = Foldr StrictPair () as
- strictCurry :: (StrictPair a b -> c) -> a -> b -> c
- strictUncurry :: (a -> b -> c) -> StrictPair a b -> c
- type family IsBase t :: Bool where ...
- type family Domains t :: [Type] where ...
- type family Domains' t :: [Type] where ...
- type family CoDomain t where ...
- type family CoDomain' t where ...
- class Currying (as :: [Type]) b where
- class StrictCurrying (as :: [Type]) b where
- strictUncurrys :: Proxy as -> Proxy b -> Arrows as b -> StrictProducts as -> b
- strictCurrys :: Proxy as -> Proxy b -> (StrictProducts as -> b) -> Arrows as b
- data Function a b
- data Constant0 (c :: Function a (Function b a -> Type))
- data Constant1 c (d :: Function b a)
- type family Apply (t :: Function k l -> Type) (u :: k) :: l
Documentation
type family All (p :: k -> Constraint) (as :: [k]) where ... Source #
All p as ensures that the constraint p is satisfied by
all the types in as.
(Types is between scare-quotes here because the code is
actually kind polymorphic)
Equations
| All (p :: k -> Constraint) ('[] :: [k]) = () | |
| All (p :: k -> Constraint) (a ': as :: [k]) = (p a, All p as) |
type family Foldr' (c :: Function k (Function l l -> Type) -> Type) (n :: l) (as :: [k]) :: l where ... Source #
Version of Foldr taking a defunctionalised argument so
that we can use partially applied functions.
type Arrows (as :: [Type]) r = Foldr (->) r as Source #
Arrows [a1,..,an] r corresponds to a1 -> .. -> an -> r
| Products [a1,..,an] corresponds to (a1, (..,( an, ())..))
data StrictPair a b Source #
Constructors
| Pair a b |
type StrictProducts (as :: [Type]) = Foldr StrictPair () as Source #
strictCurry :: (StrictPair a b -> c) -> a -> b -> c Source #
strictUncurry :: (a -> b -> c) -> StrictPair a b -> c Source #
type family IsBase t :: Bool where ... Source #
IsBase t is 'True whenever t is *not* a function space.
type family Domains t :: [Type] where ... Source #
Using IsBase we can define notions of Domains and CoDomains
which *reduce* under positive information IsBase t ~ 'True even
though the shape of t is not formally exposed
class Currying (as :: [Type]) b where Source #
Currying as b witnesses the isomorphism between Arrows as b
and Products as -> b. It is defined as a type class rather
than by recursion on a singleton for as so all of that these
conversions are inlined at compile time for concrete arguments.
Methods
uncurrys :: Proxy as -> Proxy b -> Arrows as b -> Products as -> b Source #
currys :: Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b Source #
class StrictCurrying (as :: [Type]) b where Source #
Methods
strictUncurrys :: Proxy as -> Proxy b -> Arrows as b -> StrictProducts as -> b Source #
strictCurrys :: Proxy as -> Proxy b -> (StrictProducts as -> b) -> Arrows as b Source #
Instances
| StrictCurrying ('[] :: [Type]) b Source # | |
Defined in Agda.Utils.TypeLevel Methods strictUncurrys :: Proxy ('[] :: [Type]) -> Proxy b -> Arrows ('[] :: [Type]) b -> StrictProducts ('[] :: [Type]) -> b Source # strictCurrys :: Proxy ('[] :: [Type]) -> Proxy b -> (StrictProducts ('[] :: [Type]) -> b) -> Arrows ('[] :: [Type]) b Source # | |
| StrictCurrying as b => StrictCurrying (a ': as) b Source # | |
Defined in Agda.Utils.TypeLevel Methods strictUncurrys :: Proxy (a ': as) -> Proxy b -> Arrows (a ': as) b -> StrictProducts (a ': as) -> b Source # strictCurrys :: Proxy (a ': as) -> Proxy b -> (StrictProducts (a ': as) -> b) -> Arrows (a ': as) b Source # | |
type family Apply (t :: Function k l -> Type) (u :: k) :: l Source #
Instances
| type Apply (Constant1 a :: Function k Type -> Type) (b :: k) Source # | |
| type Apply (Constant0 :: Function Type (Function b Type -> Type) -> Type) (a :: Type) Source # | |
| type Apply (ConsMap0 f :: Function k (Function [l] [l] -> Type) -> Type) (a :: k) Source # | |
| type Apply (ConsMap1 f a2 :: Function [a1] [a1] -> Type) (tl :: [a1]) Source # | |