File: FunCompose.dhall

package info (click to toggle)
haskell-dhall 1.42.3-1
  • links: PTS, VCS
  • area: main
  • in suites: sid
  • size: 23,784 kB
  • sloc: haskell: 24,804; makefile: 3
file content (18 lines) | stat: -rw-r--r-- 525 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
 

let compose
    : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c
    =   λ(A : Type)
      → λ(B : Type)
      → λ(C : Type)
      → λ(f : A → B)
      → λ(g : B → C)
      → λ(x : A)
      → g (f x)

let composeN : ∀ (a : Type) → Natural → (a → a) → a → a
    = λ (a : Type)
	→ λ (n : Natural)
	→ λ (f : a → a)
	→ Natural/fold n (a → a) (compose a a a f) (λ (x : a) → x)

in composeN Natural 100000 (λ (x : Natural) → x + 1) 0