Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

## Synopsis

- data List (f ∷ k → Type) (as ∷ [k]) where
- mapList ∷ (∀ a. f a → g a) → List f as → List g as
- mapListC ∷ ∀ c as f g. All c as ⇒ (∀ a. c a ⇒ f a → g a) → List f as → List g as
- mapMList ∷ Applicative m ⇒ (∀ a. f a → m (g a)) → List f as → m (List g as)
- mapMListC ∷ ∀ c as f g m. (Applicative m, All c as) ⇒ (∀ a. c a ⇒ f a → m (g a)) → List f as → m (List g as)
- foldMapList ∷ Monoid b ⇒ (∀ a. f a → b) → List f as → b
- foldMapListC ∷ ∀ c as b f. (All c as, Monoid b) ⇒ (∀ a. c a ⇒ f a → b) → List f as → b
- appendList ∷ List f as → List f bs → List f (Append as bs)
- lengthList ∷ List f as → Int
- type family Append as as' where ...
- type family MapList (f ∷ k → j) as where ...
- data ListCtx f (as ∷ [Type]) c where
- pattern NilCtx ∷ c a → ListCtx f '[a] c
- pattern ListCtx ∷ () ⇒ as'' ~ Append as (a ': as') ⇒ List f as → c a → List f as' → ListCtx f as'' c
- data ListCtxWhole f as c where
- ListCtxWhole ∷ List f as → c a → List f as' → ListCtxWhole f (Append as (a ': as')) c

- toWholeCtx ∷ ListCtx f as c → ListCtxWhole f as c
- fromWholeCtx ∷ ListCtxWhole f as c → ListCtx f as c
- fillListCtx ∷ ListCtx f as c → (∀ a. c a → f a) → List f as
- mapListCtx ∷ (∀ a. f a → g a) → ListCtx f as c → ListCtx g as c
- mapListCtxC ∷ ∀ c as f g h. All c as ⇒ (∀ a. c a ⇒ f a → g a) → ListCtx f as h → ListCtx g as h
- type family FunTy ts res where ...
- listShape ∷ ∀ as. TypeList as ⇒ List (Const ()) as
- class TypeList ts where
- uncurryList ∷ FunTy (MapList f ts) r → List f ts → r
- uncurryList_ ∷ (∀ a. f a → a) → FunTy ts r → List f ts → r
- curryList ∷ (List f ts → r) → FunTy (MapList f ts) r
- curryList_ ∷ (∀ a. a → f a) → (List f ts → r) → FunTy ts r
- unfoldList ∷ (∀ a as. List f as → f a) → List f ts

- type family All (c ∷ k → Constraint) (as ∷ [k]) ∷ Constraint where ...

# Documentation

data List (f ∷ k → Type) (as ∷ [k]) where Source #

A heterogeneous list / an inductive tuple.
We use this heavily to represent arguments to
functions in terms. A term application (c.f. `Base`

)
is represented as `App :: fn as b -> List (Term fn) as -> Term fn b`
for example.

mapMListC ∷ ∀ c as f g m. (Applicative m, All c as) ⇒ (∀ a. c a ⇒ f a → m (g a)) → List f as → m (List g as) Source #

foldMapList ∷ Monoid b ⇒ (∀ a. f a → b) → List f as → b Source #

lengthList ∷ List f as → Int Source #

pattern ListCtx ∷ () ⇒ as'' ~ Append as (a ': as') ⇒ List f as → c a → List f as' → ListCtx f as'' c Source #

A view of a `ListCtx`

where you see the whole context at the same time.

data ListCtxWhole f as c where Source #

Internals for the `ListCtx`

pattern

ListCtxWhole ∷ List f as → c a → List f as' → ListCtxWhole f (Append as (a ': as')) c |

toWholeCtx ∷ ListCtx f as c → ListCtxWhole f as c Source #

fromWholeCtx ∷ ListCtxWhole f as c → ListCtx f as c Source #

fillListCtx ∷ ListCtx f as c → (∀ a. c a → f a) → List f as Source #

mapListCtx ∷ (∀ a. f a → g a) → ListCtx f as c → ListCtx g as c Source #

mapListCtxC ∷ ∀ c as f g h. All c as ⇒ (∀ a. c a ⇒ f a → g a) → ListCtx f as h → ListCtx g as h Source #

type family FunTy ts res where ... Source #

A function type from `ts`

to `res`

:
FunTy '[Int, Bool] Double = Int -> Bool -> Double

listShape ∷ ∀ as. TypeList as ⇒ List (Const ()) as Source #

Materialize the shape of the type list `as`

, this is very useful
for avoiding having to write type classes that recurse over `as`

.

class TypeList ts where Source #

Higher-order functions for working on `List`

s

uncurryList ∷ FunTy (MapList f ts) r → List f ts → r Source #

uncurryList_ ∷ (∀ a. f a → a) → FunTy ts r → List f ts → r Source #

curryList ∷ (List f ts → r) → FunTy (MapList f ts) r Source #

curryList_ ∷ (∀ a. a → f a) → (List f ts → r) → FunTy ts r Source #

unfoldList ∷ (∀ a as. List f as → f a) → List f ts Source #

#### Instances

TypeList ('[] ∷ [Type]) Source # | NOTE: the two instances for |

Defined in Constrained.List uncurryList ∷ ∀ (f ∷ Type → Type) r. FunTy (MapList f '[]) r → List f '[] → r Source # uncurryList_ ∷ (∀ a. f a → a) → FunTy '[] r → List f '[] → r Source # curryList ∷ ∀ (f ∷ Type → Type) r. (List f '[] → r) → FunTy (MapList f '[]) r Source # curryList_ ∷ (∀ a. a → f a) → (List f '[] → r) → FunTy '[] r Source # unfoldList ∷ (∀ a (as ∷ [Type]). List f as → f a) → List f '[] Source # | |

TypeList as ⇒ TypeList (a ': as) Source # | |

Defined in Constrained.List uncurryList ∷ ∀ (f ∷ Type → Type) r. FunTy (MapList f (a ': as)) r → List f (a ': as) → r Source # uncurryList_ ∷ (∀ a0. f a0 → a0) → FunTy (a ': as) r → List f (a ': as) → r Source # curryList ∷ ∀ (f ∷ Type → Type) r. (List f (a ': as) → r) → FunTy (MapList f (a ': as)) r Source # curryList_ ∷ (∀ a0. a0 → f a0) → (List f (a ': as) → r) → FunTy (a ': as) r Source # unfoldList ∷ (∀ a0 (as0 ∷ [Type]). List f as0 → f a0) → List f (a ': as) Source # |

type family All (c ∷ k → Constraint) (as ∷ [k]) ∷ Constraint where ... Source #