ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.TypeLevel

9 types
2 classes
2 values

PackageAgda-2.7.0.1
Exports25
LanguageHaskell2010
LicenceMIT
SourceTypeLevel.hs

familytype family All (p :: k -> Constraint) (as :: [k]) :: Constraint where

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 '[] = ()
All p (a ': as) = (p a, All p as)

familytype family If (b :: Bool) (l :: k) (r :: k) :: k where

On Booleans

Equations

If 'True l r = l
If 'False l r = r

familytype family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l where

On Lists

Equations

Foldr c n '[] = n
Foldr c n (a ': as) = c a (Foldr c n as)

familytype family Foldr' (c :: Function k (Function l l -> Type) -> Type) (n :: l) (as :: [k]) :: l where

Version of Foldr taking a defunctionalised argument so that we can use partially applied functions.

Equations

Foldr' c n '[] = n
Foldr' c n (a ': as) = Apply (Apply c a) (Foldr' c n as)

familytype family Map (f :: Function k l -> Type) (as :: [k]) :: [l] where

Equations

Map f as = Foldr' (ConsMap0 f) '[] as

datadata ConsMap0 (a :: Function k l -> Type) (b :: Function k (Function [l] [l] -> Type))

Instances1Apply

type Apply (ConsMap0 f) a = ConsMap1 f aDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel

datadata ConsMap1 (a :: Function k l -> Type) (b :: k) (c :: Function [l] [l])

Instances1Apply

type Apply (ConsMap1 f a2) tl = Apply f a2 ': tlDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel

familytype family Constant (b :: l) (as :: [k]) :: [l] where

Equations

Constant b as = Map (Constant1 b) as

typetype Arrows (as :: [Type]) r = Foldr (->) r as

Arrows [a1,..,an] r corresponds to a1 -> .. -> an -> r | Products [a1,..,an] corresponds to (a1, (..,( an, ())..))

typetype Products (as :: [Type]) = Foldr Tuple2 () as

datadata StrictPair a b

Constructors

Pair a b

typetype StrictProducts (as :: [Type]) = Foldr StrictPair () as

valuestrictCurry :: (StrictPair a b -> c) -> a -> b -> c

valuestrictUncurry :: (a -> b -> c) -> StrictPair a b -> c

familytype family IsBase t :: Bool where

IsBase t is 'True whenever t is *not* a function space.

Equations

IsBase (a -> t3) = 'False
IsBase a = 'True

familytype family Domains t :: [Type] where

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

Equations

Domains t = If (IsBase t) '[] (Domains' t)

familytype family Domains' t :: [Type] where

Equations

Domains' (a -> t) = a ': Domains t

familytype family CoDomain t where

Equations

CoDomain t = If (IsBase t) t (CoDomain' t)

familytype family CoDomain' t where

Equations

CoDomain' (a -> t2) = CoDomain t2

classclass Currying (as :: [Type]) b where

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
currys :: Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b

Instances2Currying

Currying '[] bDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel
Currying as b => Currying (a ': as) bDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel

classclass StrictCurrying (as :: [Type]) b where

Methods

strictUncurrys :: Proxy as -> Proxy b -> Arrows as b -> StrictProducts as -> b
strictCurrys :: Proxy as -> Proxy b -> (StrictProducts as -> b) -> Arrows as b

Instances2StrictCurrying

StrictCurrying '[] bDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel
StrictCurrying as b => StrictCurrying (a ': as) bDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel

datadata Function a b

Instances2Apply

type Apply Constant0 a = Constant1 aDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel
type Apply (ConsMap0 f) a = ConsMap1 f aDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel

datadata Constant0 (c :: Function a (Function b a -> Type))

Instances1Apply

type Apply Constant0 a = Constant1 aDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel

datadata Constant1 c (d :: Function b a)

Instances1Apply

type Apply (Constant1 a) b = aDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel

familytype family Apply (t :: Function k l -> Type) (u :: k) :: l

Instances4Apply

type Apply Constant0 a = Constant1 aDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel
type Apply (ConsMap0 f) a = ConsMap1 f aDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel
type Apply (ConsMap1 f a2) tl = Apply f a2 ': tlDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel
type Apply (Constant1 a) b = aDefined in Agda-2.7.0.1 · Agda.Utils.TypeLevel