ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.TypeLevel

Synopsis

family All
family If
family Foldr
family Foldr'
family Map
data ConsMap0
data ConsMap1
family Constant
type Arrows
type Products
data StrictPair
type StrictProducts
value strictCurry
value strictUncurry
family IsBase
family Domains
family Domains'
family CoDomain
family CoDomain'
class Currying
class StrictCurrying
data Function
data Constant0
data Constant1
family Apply

PackageAgda-2.8.0.2
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

Source#

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

Source#

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

Source#

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.8.0.2 · 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.8.0.2 · Agda.Utils.TypeLevel

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

Equations

Constant b as = Map (Constant1 b) as

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

Source#

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

Source#

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

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

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

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

Instances2Currying

Currying '[] bDefined in Agda-2.8.0.2 · Agda.Utils.TypeLevel
Currying as b => Currying (a ': as) bDefined in Agda-2.8.0.2 · 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.8.0.2 · Agda.Utils.TypeLevel
StrictCurrying as b => StrictCurrying (a ': as) bDefined in Agda-2.8.0.2 · Agda.Utils.TypeLevel

datadata Function a b

Instances2Apply

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

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

Instances1Apply

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

datadata Constant1 c (d :: Function b a)

Instances1Apply

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

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

Instances4Apply

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