Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.List

Synopsis

data List (f ∷ k → Type) (as ∷ [k]) where
- Nil ∷ List f '[]
- (:>) ∷ f a → List f as → List f (a ': as)
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
- (:?) ∷ c a → List f as → ListCtx f (a ': as) c
- (:!) ∷ f a → ListCtx f as c → ListCtx f (a ': as) c
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.

Constructors

Nil ∷ List f '[]
(:>) ∷ f a → List f as → List f (a ': as) infixr 5

Instances

Instances details

HasVariables fn (List (Term fn) as) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ List (Term fn) as → FreeVars fn Source # freeVarSet ∷ List (Term fn) as → Set (Name fn) Source # countOf ∷ Name fn → List (Term fn) as → Int Source # appearsIn ∷ Name fn → List (Term fn) as → Bool Source #
HasVariables fn (List (Binder fn) as) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ List (Binder fn) as → FreeVars fn Source # freeVarSet ∷ List (Binder fn) as → Set (Name fn) Source # countOf ∷ Name fn → List (Binder fn) as → Int Source # appearsIn ∷ Name fn → List (Binder fn) as → Bool Source #
(∀ (a ∷ k). Show (f a)) ⇒ Show (List f as) Source #
Instance details Defined in Constrained.List Methods showsPrec ∷ Int → List f as → ShowS Source # show ∷ List f as → String Source # showList ∷ [List f as] → ShowS Source #
(∀ a. Rename (f a)) ⇒ Rename (List f as) Source #
Instance details Defined in Constrained.Core Methods rename ∷ Typeable x ⇒ Var x → Var x → List f as → List f as Source #
(∀ (a ∷ k). Eq (f a)) ⇒ Eq (List f as) Source #
Instance details Defined in Constrained.List Methods (==) ∷ List f as → List f as → Bool Source # (/=) ∷ List f as → List f as → Bool Source #

mapList ∷ (∀ a. f a → g a) → List f as → List g as Source #

mapListC ∷ ∀ c as f g. All c as ⇒ (∀ a. c a ⇒ f a → g a) → List f as → List g as Source #

mapMList ∷ Applicative m ⇒ (∀ a. f a → m (g a)) → List f as → m (List g as) Source #

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 #

foldMapListC ∷ ∀ c as b f. (All c as, Monoid b) ⇒ (∀ a. c a ⇒ f a → b) → List f as → b Source #

appendList ∷ List f as → List f bs → List f (Append as bs) Source #

lengthList ∷ List f as → Int Source #

type family Append as as' where ... Source #

Append two type-level lists

Equations

Append '[] as' = as'
Append (a ': as) as' = a ': Append as as'

type family MapList (f ∷ k → j) as where ... Source #

Map a type functor over a list

Equations

MapList f '[] = '[]
MapList f (a ': as) = f a ': MapList f as

data ListCtx f (as ∷ [Type]) c where Source #

A List with a hole in it, can be seen as a zipper over type-level lists.

We use this to represent contexts over terms in Base. For example, an application of f to a single variable of type a would be the pair `(fn as b, ListCtx Value as (HOLE a))` where HOLE (c.f. Base) is isomorphic to :~:.

Constructors

(:?) ∷ c a → List f as → ListCtx f (a ': as) c infixr 5
(:!) ∷ f a → ListCtx f as c → ListCtx f (a ': as) c infixr 5

pattern NilCtx ∷ c a → ListCtx f '[a] c Source #

A Convenient pattern for singleton contexts

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

Constructors

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

Equations

FunTy '[] a = a
FunTy (a ': as) r = a → FunTy as r

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 Lists

Methods

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

Instances details

TypeList ('[] ∷ [Type]) Source #	NOTE: the two instances for `TypeList` are `TypeList '[]` and `TypeList '(a : as)`. That way its basically just a structurally recursive function on type-level lists that computes the `TypeList` dictionary.
Instance details Defined in Constrained.List Methods 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 #
Instance details Defined in Constrained.List Methods 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 #

Equations

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