/Prelude-v23.1.0/Function/composeList.dhall

Copy path to clipboard

Composes a list of functions starting from the left.

Examples

composeList Natural [ λ(x : Natural) → x * 2, λ(x : Natural) → x + 1 ] 1 ≡ 3

Source

{-|
Composes a list of functions starting from the left.
-}
let compose =
missing sha256:65ad8bbea530b3d8968785a7cf4a9a7976b67059aa15e3b61fcba600a40ae013
? ./compose.dhall

let identity =
missing sha256:f78b96792b459cb664f41c6119bd8897dd04353a3343521d436cd82ad71cb4d4
? ./identity.dhall

let composeList
: ∀(a : Type) → List (a → a) → a → a
= λ(a : Type) →
λ(functions : List (aa)) →
List/fold (aa) functions (aa) (compose a a a) (identity a)

let example0 =
assert
: composeList
Natural
[ λ(x : Natural) → x * 2, λ(x : Natural) → x + 1 ]
1
≡ 3

let property0 =
λ(a : Type) →
λ(f : aa) →
λ(g : aa) →
λ(h : aa) →
assert : composeList a [ f, g, h ] ≡ (λ(x : a) → h (g (f x)))

in composeList