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:

Nat  Nat  Nat

and the type of the addition function for vectors is:

(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):

(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):

example₁ = \ (A : Set)(x : A)  x
example₂ = \ A x  x

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

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:

prop₁ : ((x : A) (y : B)  C) is-the-same-as   ((x : A)  (y : B)  C)
prop₂ : ((x y : A)  C)       is-the-same-as   ((x : A)(y : A)  C)
prop₃ : (forall (x : A)  C)  is-the-same-as   ((x : A)  C)
prop₄ : (forall x  C)        is-the-same-as   ((x : _)  C)
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:

(\x y  e)                    is-the-same-as   (\x  (\y  e))

Functional application:

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