Functions

See the official user manual for the most up-to-date version of the information on this page.

TOC

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

 \ (A : Set)(x : A) -> x
 \ A x -> x

Applications are written as f a b c where f is a function and a, b and c are arguments.

Function declarations

The general form for defining a function is

 f : (x1 : A1) -> ... -> (xn : An) -> B
 f p1 ... pn = d
 ...
 f q1 ... qn = e

where f is a new identifier, A is a type, B is a type under the assumption that the variable x has the type A, p_i and q_i are patterns and d and e are expressions.

The declaration above gives the identifier f type (x1 : A1) -> ... -> (xn : An) -> B and f is defined by the defining equations. Patterns are matched from top to bottom, i.e., the first pattern that matches the actual parameters is the one that is used.

Abstraction

An object in the type (x : A) -> B is always equal to

 \x -> b

where b : B under the assumption that x : A.

Typed abstraction can also be used:

 \(x : A) -> b

is another notation for the abstraction above if the type of the variable x is A.

Application

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

The following notational conventions can be used

• function types

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

Pattern matching lambdas.

Anonymous pattern matching functions can be defined using the syntax

  \ { p11 .. p1n -> e1 ; ... ; pm1 .. pmn -> em }

(where, as usual, \ and -> can be replaced by λ and →). Internally this is translated into a function definition of the following form:

  .extlam p11 .. p1n = e1
  ...
  .extlam pm1 .. pmn = em

This means that anonymous pattern matching functions are generative. For instance, refl will not be accepted as an inhabitant of the type

  (λ { true → true ; false → false }) ≡
  (λ { true → true ; false → false }),

because this is equivalent to extlam1 ≡ extlam2 for some distinct fresh names extlam1 and extlam2.

Currently the 'where' and 'with' constructions are not allowed in (the top-level clauses of) anonymous pattern matching functions.

Examples:

  and : Bool → Bool → Bool
  and = λ { true x → x ; false _ → false }

  xor : Bool → Bool → Bool
  xor = λ { true  true  → false
          ; false false → false
          ; _     _     → true
          }

  fst : {A : Set} {B : A → Set} → Σ A B → A
  fst = λ { (a , b) → a }

  snd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p)
  snd = λ { (a , b) → b }

Unlike the usual layout rules, the { ... } block of a pattern matching lambda cannot be replaced by indentation.