Safe Haskell	None
Language	Haskell2010

Agda.Utils.TypeLevel

Synopsis

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 -> Type) -> Type) (n :: l) (as :: [k]) :: l where ...
type family Map (f :: Function k l -> Type) (as :: [k]) :: [l] where ...
data ConsMap0 :: (Function k l -> Type) -> Function k (Function [l] [l] -> Type) -> Type
data ConsMap1 :: (Function k l -> Type) -> k -> Function [l] [l] -> Type
type family Constant (b :: l) (as :: [k]) :: [l] where ...
type Arrows (as :: [Type]) (r :: Type) = Foldr (->) r as
type Products (as :: [Type]) = Foldr (,) () as
type family IsBase (t :: Type) :: Bool where ...
type family Domains (t :: Type) :: [Type] where ...
type family Domains' (t :: Type) :: [Type] where ...
type family CoDomain (t :: Type) :: Type where ...
type family CoDomain' (t :: Type) :: Type where ...
class Currying as b where
- uncurrys :: Proxy as -> Proxy b -> Arrows as b -> Products as -> b
- currys :: Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b
data Function :: Type -> Type -> Type
data Constant0 :: Function a (Function b a -> Type) -> Type
data Constant1 :: Type -> Function b a -> Type
type family Apply (t :: Function k l -> Type) (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)

Equations

All p '[] = ()
All p (a ': as) = (p a, All p as)

type family If (b :: Bool) (l :: k) (r :: k) :: k where ... Source #

On Booleans

Equations

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

type 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)

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.

Equations

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

type family Map (f :: Function k l -> Type) (as :: [k]) :: [l] where ... Source #

Equations

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

data ConsMap0 :: (Function k l -> Type) -> Function k (Function [l] [l] -> Type) -> Type Source #

Instances

Instances details

type Apply (ConsMap0 f :: Function k (Function [l] [l] -> Type) -> Type) (a :: k) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (ConsMap0 f :: Function k (Function [l] [l] -> Type) -> Type) (a :: k) = ConsMap1 f a

data ConsMap1 :: (Function k l -> Type) -> k -> Function [l] [l] -> Type Source #

Instances

Instances details

type Apply (ConsMap1 f a2 :: Function [a1] [a1] -> Type) (tl :: [a1]) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (ConsMap1 f a2 :: Function [a1] [a1] -> Type) (tl :: [a1]) = Apply f a2 ': tl

type family Constant (b :: l) (as :: [k]) :: [l] where ... Source #

Equations

Constant b as = Map (Constant1 b) as

type Arrows (as :: [Type]) (r :: Type) = Foldr (->) r as Source #

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

type Products (as :: [Type]) = Foldr (,) () as Source #

type family IsBase (t :: Type) :: Bool where ... Source #

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

Equations

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

type family Domains (t :: Type) :: [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)

type family Domains' (t :: Type) :: [Type] where ... Source #

Equations

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

type family CoDomain (t :: Type) :: Type where ... Source #

Equations

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

type family CoDomain' (t :: Type) :: Type where ... Source #

Equations

CoDomain' (a -> t) = CoDomain 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.

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 #

Instances

Instances details

Currying ('[] :: [Type]) b Source #
Instance details Defined in Agda.Utils.TypeLevel Methods uncurrys :: Proxy '[] -> Proxy b -> Arrows '[] b -> Products '[] -> b Source # currys :: Proxy '[] -> Proxy b -> (Products '[] -> b) -> Arrows '[] b Source #
Currying as b => Currying (a ': as) b Source #
Instance details Defined in Agda.Utils.TypeLevel Methods uncurrys :: Proxy (a ': as) -> Proxy b -> Arrows (a ': as) b -> Products (a ': as) -> b Source # currys :: Proxy (a ': as) -> Proxy b -> (Products (a ': as) -> b) -> Arrows (a ': as) b Source #

data Function :: Type -> Type -> Type Source #

Instances

Instances details

type Apply (Constant0 :: Function Type (Function b Type -> Type) -> Type) (a :: Type) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (Constant0 :: Function Type (Function b Type -> Type) -> Type) (a :: Type) = Constant1 a :: Function b Type -> Type
type Apply (ConsMap0 f :: Function k (Function [l] [l] -> Type) -> Type) (a :: k) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (ConsMap0 f :: Function k (Function [l] [l] -> Type) -> Type) (a :: k) = ConsMap1 f a

data Constant0 :: Function a (Function b a -> Type) -> Type Source #

Instances

Instances details

type Apply (Constant0 :: Function Type (Function b Type -> Type) -> Type) (a :: Type) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (Constant0 :: Function Type (Function b Type -> Type) -> Type) (a :: Type) = Constant1 a :: Function b Type -> Type

data Constant1 :: Type -> Function b a -> Type Source #

Instances

Instances details

type Apply (Constant1 a :: Function k Type -> Type) (b :: k) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (Constant1 a :: Function k Type -> Type) (b :: k) = a

type family Apply (t :: Function k l -> Type) (u :: k) :: l Source #

Instances

Instances details

type Apply (Constant1 a :: Function k Type -> Type) (b :: k) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (Constant1 a :: Function k Type -> Type) (b :: k) = a
type Apply (Constant0 :: Function Type (Function b Type -> Type) -> Type) (a :: Type) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (Constant0 :: Function Type (Function b Type -> Type) -> Type) (a :: Type) = Constant1 a :: Function b Type -> Type
type Apply (ConsMap0 f :: Function k (Function [l] [l] -> Type) -> Type) (a :: k) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (ConsMap0 f :: Function k (Function [l] [l] -> Type) -> Type) (a :: k) = ConsMap1 f a
type Apply (ConsMap1 f a2 :: Function [a1] [a1] -> Type) (tl :: [a1]) Source #
Instance details Defined in Agda.Utils.TypeLevel type Apply (ConsMap1 f a2 :: Function [a1] [a1] -> Type) (tl :: [a1]) = Apply f a2 ': tl