Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 (as :: [k]) :: [Type] 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
  - uncurrys :: Proxy as -> Proxy b -> Arrows as b -> Products as -> b
  - currys :: Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b
- 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 If (b :: Bool) (l :: k) (r :: k) :: k where ... Source #

On Booleans

Equations

If 'True (l :: k) (r :: k) = l |
If 'False (l :: k) (r :: k) = r |

type family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l where ... Source #

On Lists

Equations

Foldr (c :: k -> l -> l) (n :: l) ('[] :: [k]) = n |
Foldr (c :: k -> l -> l) (n :: l) (a ': as :: [k]) = 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 :: Function k (Function l l -> Type) -> Type) (n :: l) ('[] :: [k]) = n |
Foldr' (c :: Function k (Function l l -> Type) -> Type) (n :: l) (a ': as :: [k]) = Apply (Apply c a) (Foldr' c n as) |

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

Equations

Map (f :: Function k l -> Type) (as :: [k]) = Foldr' (ConsMap0 f) ('[] :: [l]) as |

data ConsMap0 (a :: Function k l -> Type) (b :: Function k (Function [l] [l] -> 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 (a :: Function k l -> Type) (b :: k) (c :: Function [l] [l]) 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 (as :: [k]) :: [Type] where ... Source #

Equations

Constant b (as :: [k]) = Map (Constant1 b :: Function k Type -> Type) as |

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, ())..))`

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

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.

Equations

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

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

Equations

Domains t = If (IsBase t) ('[] :: [Type]) (Domains' t) |

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

Equations

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

type family CoDomain t where ... Source #

Equations

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

type family CoDomain' t where ... Source #

Equations

CoDomain' (a -> t2) = CoDomain t2 |

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 #

#### Instances

Instances details

Currying ('[] :: [Type]) b Source # |
Instance details Defined in Agda.Utils.TypeLevel Methods uncurrys :: Proxy ('[] :: [Type]) -> Proxy b -> Arrows ('[] :: [Type]) b -> Products ('[] :: [Type]) -> b Source # currys :: Proxy ('[] :: [Type]) -> Proxy b -> (Products ('[] :: [Type]) -> b) -> Arrows ('[] :: [Type]) 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 #

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

Instances details

StrictCurrying ('[] :: [Type]) b Source # |
Instance details 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 # |
Instance details 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 #

data Function a b 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 (c :: Function a (Function b a -> 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 c (d :: Function b a) 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