Function Types

Function types are written (x : A) → B, or in the case of non-dependent functions simply A → B. For instance, the type of the addition function for natural numbers is:

  1. Nat → Nat → Nat

and the type of the addition function for vectors is:

  1. (A : Set) → (n : Nat) → (u : Vec A n) → (v : Vec A n) → Vec A n

where Set is the type of sets and Vec A n is the type of vectors with n elements of type A. Arrows between consecutive hypotheses of the form (x : A) may also be omitted, and (x : A) (y : A) may be shortened to (x y : A):

  1. (A : Set) (n : Nat)(u v : Vec A n) → Vec A n

Functions are constructed by lambda abstractions, which can be either typed or untyped. For instance, both expressions below have type (A : Set) → A → A (the second expression checks against other types as well):

  1. example₁ = \ (A : Set)(x : A) → x
  2. example₂ = \ A x → x

You can also use the Unicode symbol λ (type “\lambda” or “\Gl” in the Emacs Agda mode) instead of \ (type “\\” in the Emacs Agda mode).

The application of a function f : (x : A) → B to an argument a : A is written f a and the type of this is B[x := a].

Notational conventions

Function types:

  1. prop₁ : ((x : A) (y : B) → C) is-the-same-as   ((x : A) → (y : B) → C)
  2. prop₂ : ((x y : A) → C)       is-the-same-as   ((x : A)(y : A) → C)
  3. prop₃ : (forall (x : A) → C)  is-the-same-as   ((x : A) → C)
  4. prop₄ : (forall x → C)        is-the-same-as   ((x : _) → C)
  5. prop₅ : (forall x y → C)      is-the-same-as   (forall x → forall y → C)

You can also use the Unicode symbol ∀ (type “\all” in the Emacs Agda mode) instead of forall.

Functional abstraction:

  1. (\x y → e)                    is-the-same-as   (\x → (\y → e))

Functional application:

  1. (f a b)                       is-the-same-as    ((f a) b)