module LambdaNotation where

open import Nat

-- Three ways of writing the identity function on Nat, index x₀ is produced by typing x \_ 0

-- without lambda

idNat₀ : Nat → Nat
idNat₀ x = x

-- lambda notation a la Curry

idNat₁ : Nat → Nat
idNat₁ = λ x → x

-- lambda notation a la Church (with type label Nat for x)

idNat₂ : Nat → Nat
idNat₂ = λ (x : Nat) → x

-- the polymorphic identity function, with lambda and a la Curry
-- explicit polymorphism (note dependent function space!), cf Haskell id :: a -> a

id : (A : Set) → A → A
id = λ A x → x

-- with implicit type argument, note curly braces: {A : Set}

id' : {A : Set} → A → A
id' = λ x → x

-- the K combinator with wildcards and telescopes

K : (A B : Set) → A → B → A
K _ _ x _ = x