| Copyright | (c) Sebastian Graf 2018 |
|---|---|
| License | ISC |
| Maintainer | sgraf1337@gmail.com |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Datafix.Utils.TypeLevel
Description
Some type-level helpers for 'curry'/'uncurry'ing arbitrary function types.
- type family All (p :: k -> Constraint) (as :: [k]) :: Constraint 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 -> *) -> *) (n :: l) (as :: [k]) :: l where ...
- type family Map (f :: Function k l -> *) (as :: [k]) :: [l] where ...
- data ConsMap0 :: (Function k l -> *) -> Function k (Function [l] [l] -> *) -> *
- data ConsMap1 :: (Function k l -> *) -> k -> Function [l] [l] -> *
- type family Constant (b :: l) (as :: [k]) :: [l] where ...
- type Arrows (as :: [*]) (r :: *) = Foldr (->) r as
- arrowsAxiom :: Arrows (ParamTypes func) (ReturnType func) :~: func
- type family Products (as :: [*]) where ...
- type family IsBase (t :: *) :: Bool where ...
- type family ParamTypes (t :: *) :: [*] where ...
- type family ParamTypes' (t :: *) :: [*] where ...
- type family ReturnType (t :: *) :: * where ...
- type family ReturnType' (t :: *) :: * where ...
- class Currying as b where
- data Function :: * -> * -> *
- data Constant0 :: Function a (Function b a -> *) -> *
- data Constant1 :: * -> Function b a -> *
- type family Apply (t :: Function k l -> *) (u :: k) :: l
Documentation
type family All (p :: k -> Constraint) (as :: [k]) :: Constraint 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)
type family Foldr' (c :: Function k (Function l l -> *) -> *) (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 :: [*]) (r :: *) = Foldr (->) r as Source #
Arrows [a1,..,an] r corresponds to a1 -> .. -> an -> r
arrowsAxiom :: Arrows (ParamTypes func) (ReturnType func) :~: func Source #
type family Products (as :: [*]) where ... Source #
Products [] corresponds to (),
Products [a] corresponds to a,
Products [a1,..,an] corresponds to (a1, (..,( an)..)).
So, not quite a right fold, because we want to optimize for the empty, singleton and pair case.
type family IsBase (t :: *) :: Bool where ... Source #
IsBase t is 'True whenever t is *not* a function space.
type family ParamTypes (t :: *) :: [*] where ... Source #
Using IsBase we can define notions of ParamTypes and ReturnTypes
which *reduce* under positive information IsBase t ~ 'True even
though the shape of t is not formally exposed
Equations
| ParamTypes t = If (IsBase t) '[] (ParamTypes' t) |
type family ParamTypes' (t :: *) :: [*] where ... Source #
Equations
| ParamTypes' (a -> t) = a ': ParamTypes t |
type family ReturnType (t :: *) :: * where ... Source #
Equations
| ReturnType t = If (IsBase t) t (ReturnType' t) |
type family ReturnType' (t :: *) :: * where ... Source #
Equations
| ReturnType' (a -> t) = ReturnType t |
class Currying as 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.