module LambdaNotation where

-- We shall use the type of Booleans here, and thus need to "import" and "open" that file:

open import Bool

-- Let's define the identity function on Booleans.
-- We write \_0 for an index ₀

idbool₀ : Bool → Bool
idbool₀ x = x

-- We can write the same definition with lambda notation:

idbool₁ : Bool → Bool
idbool₁ = λ x → x

-- Note that this is "a la Curry": there is no type label on the variable x.

-- Alternatively, we can use typed lambda calculus "a la Church" where there is a type label Bool on x:

idbool₂ : Bool → Bool
idbool₂ = λ (x : Bool) → x

-- Identity is a polymorphic function, and the type inference algorithm in Haskell would infer 
-- the polymorphic type a -> a. If one wants to be explicit about the fact that a is arbitrary, one might
-- write this type as ∀a. a → a

-- In Agda you must explicitly write this "quantification" (and we usually use big letters for type variables):

id : (X : Set) → X → X
id X x = x

-- This is our first example of a dependent type: the type X → X depends on the variable X : Set, and that 
-- (X : Set) → X → X is the type of functions which take a set X and an element x : X to an element of X.
-- In general we write (x : A) → B for the dependent function space: 
-- the type of functions which maps an x : A to an element of B, where B may depend on x. 

-- Note that this polymorphic identity function in Agda has two arguments (X and x) in contrast to
-- the Haskell polymorphic identity function. However, it is possible to omit the first argument, 
-- if we instead use curly braces in the dependent function space:

id' : {X : Set} → X → X
id' x = x

-- We say that the argument X is "implicit", and we thus get a similar notation as in Haskell.

-- Exercise: Define the polymorphic version of if_then_else_ in Agda!

-- Yet, another feature of Agda is the use of "wildcards" _. 
-- For example K combinator (the constant function) can be defined with wildcards as follows:

K : (X Y : Set) → X → Y → X
K _ _ x _ = x

-- Note that we here have used the "telescope" notation (X Y : Set) → ... as an abbreviation for 
-- (X : Set) → (Y : Set) → ...