Data.DList

A module defining the dependent list and its interface

Definitions

data DList : (a -> Type) -> List a -> Type

  A dependent list
  @ f  the constructor of the types of elements
  @ ts the partameters from which the types of the lists elements are
       constructed

Totality: total
Visibility: public export
Constructors:

Nil : DList f []

  The empty dependent list

(::) : f x -> DList f xs -> DList f (x :: xs)

  Prepends a dependently typed element to a dependent list

Hints:

DFoldable (flip DList xs)

DFunctor (flip DList xs)

(++) : DList f xs -> DList f ys -> DList f (xs ++ ys)

  Concatenate two dependent lists

Visibility: public export
Fixity Declaration: infixr operator, level 7

length : DList f xs -> Nat

  Return the length of a dependent list

Visibility: export

head : DList f (x :: xs) -> f x

  The head of a dependent list

Visibility: export

tail : DList f (x :: xs) -> DList f xs

  The tail of a dependent list

Visibility: export

split : DList f (xs ++ xs') -> (DList f xs, DList f xs')

  split a dependent list in two

Visibility: export

pushToParams : DList (f . g) ts -> DList f (map g ts)

  Push a component of the element type constructor to the parameter list

Visibility: export

pullFromParams : DList f (map g ts) -> DList (f . g) ts

  Pull a component of the element type constructor from the parameter list

Visibility: export

dmap : (a x -> b x) -> DList a xs -> DList b xs

  Apply a function to every element of a dependent list

Visibility: export

undmap : (a x -> b) -> DList a xs -> List b

  Turn a dependent list into a non-dependent one by applying a
  dependency-removing function to its elements.

Visibility: export

dmapList : ((x : t) -> f x) -> (xs : List t) -> DList f xs

  Apply a dependent function to every element of a list,
  thus, generate a dependent list

Visibility: export

dmapList' : (0 f : (a -> b)) -> ((x : a) -> g (f x)) -> (xs : List a) -> DList g (map f xs)

  A more general version of `dmapList`, where the resulting list is dependent
  on a list of parameters which is itself a mapping on the original list

Visibility: export

dtraverse : Monad f => (a x -> f (b x)) -> DList a xs -> f (DList b xs)

  Dependent version of `traverse`.
  
  Map each element of a dependent list to a computation, evaluate those
  computations and combine the results.

Visibility: export

dtraverseList : Monad m => ((x : a) -> m (g x)) -> (xs : List a) -> m (DList g xs)

  Map each element of a list to a computation whose result type is dependent
  on the element, evaluate those computations and combine the results.

Visibility: export

dfoldr : (el x -> acc -> acc) -> acc -> DList el ts -> acc

  `foldr` version for dependent lists

Visibility: export

dfoldl : (acc -> el x -> acc) -> acc -> DList el ts -> acc

  `foldl` version for dependent lists

Visibility: export

dunzipWith : (f x -> (g x, h x)) -> DList f xs -> (DList g xs, DList h xs)

  `unzipWith` for dependent lists

Visibility: export

dunzip : DList (\x => (f x, g x)) xs -> (DList f xs, DList g xs)

  `unzip` for dependent lists

Visibility: export

dzipWith : (f x -> g x -> h x) -> DList f xs -> DList g xs -> DList h xs

  `zipWith` for dependent lists

Visibility: export

dzip : DList f xs -> DList g xs -> DList (\x => (f x, g x)) xs

  `zip` for dependent lists

Visibility: export

unzipParamsWith : (a -> (y : b ** f y)) -> List a -> (ys : List b ** DList f ys)

  Unzip a list to a dependent list and its parameter list, using a function
  that returns a dependent pair

Visibility: export

unzipParams : List (x : a ** f x) -> (xs : List a ** DList f xs)

  Unzip a list of dependent pairs
  Returns a list of parameters and a list of the dependent elements

Visibility: export

zipParamsWith : ((y : b) -> f y -> a) -> (ys : List b ** DList f ys) -> List a

  Zip a dependent list with its params, according to a zipping function

Visibility: export

zipParams : (ys : List b ** DList f ys) -> List (y : b ** f y)

  Zip a dependent list with its params

Visibility: export

unzipDSums : List (DSum f g) -> (Some (DList f), Some (DList g))

  Unzip a list of dependent sums

Visibility: export

zipToDSums : DList f xs -> DList g xs -> List (DSum f g)

  Zip two dependent lists into a list of dependent sums

Visibility: export

unzipDPairsWith : {0 f : t -> Type} -> (f x -> (g x, h x)) -> (dpairs : List (x : t ** f x)) -> (DList g (map fst dpairs), DList h (map fst dpairs))

  Zip a list of dependent pairs with an un-zipping function

Visibility: export

unzipDPairs : (dpairs : List (x : t ** (f x, g x))) -> (DList f (map fst dpairs), DList g (map fst dpairs))

  Zip a list of dependent pairs
  (of pairs of elements dependent on a common parameter)

Visibility: export

zipToDPairsWith : {0 h : t -> Type} -> (f x -> g x -> h x) -> DList f xs -> DList g xs -> List (x : t ** h x)

  Zip two dependent lists into a list of dependent pairs, according to a
  zipping function

Visibility: export

zipToDPairs : DList f xs -> DList g xs -> List (x : t ** (f x, g x))

  Zip two dependent lists into a list of dependent pairs
  (of pairs of elements dependent on a common parameter)

Visibility: export