Local Definitions: let and where¶

There are two ways of declaring local definitions in Agda:

• let-expressions
• where-blocks

let-expressions¶

A let-expression defines an abbreviation. In other words, the expression that we define in a let-expression can neither be recursive, nor can let bound functions be defined by pattern matching.

Example:

f : Nat
f = let h : Nat  Nat
h m = suc (suc m)
in  h zero + h (suc zero)

let-expressions have the general form

let f₁ : A₁₁  A₁ₙ  A₁
f₁ x₁ … xₙ = e₁
…
fₘ : Aₘ₁  Aₘₖ  Aₘ
fₘ x₁ … xₖ = eₘ
in  e’

where previous definitions are in scope in later definitions. The type signatures can be left out if Agda can infer them. After type-checking, the meaning of this is simply the substitution e’[f₁ := λ x₁ xₙ e; …; fₘ := λ x₁ xₖ eₘ]. Since Agda substitutes away let-bindings, they do not show up in terms Agda prints, nor in the goal display in interactive mode.

Let binding record patterns¶

For a record

record R : Set where
constructor c
field
f : X
g : Y
h : Z

a let expression of the form

let (c x  y z) = t
in  u

will be translated internally to as

let x = f t
y = g t
z = h t
in  u

This is not allowed if R is declared coinductive.

where-blocks¶

where-blocks are much more powerful than let-expressions, as they support arbitrary local definitions. A where can be attached to any function clause.

where-blocks have the general form

clause
where
decls

or

clause
module M where
decls

A simple instance is

g ps = e
where
f : A₁  Aₙ  A
f p₁₁ … p₁ₙ= e₁
…
…
f pₘ₁ … pₘₙ= eₘ

Here, the pᵢⱼ are patterns of the corresponding types and eᵢ is an expression that can contain occurrences of f. Functions defined with a where-expression must follow the rules for general definitions by pattern matching.

Example:

reverse : {A : Set}  List A  List A
reverse {A} xs = rev-append xs []
where
rev-append : List A  List A  List A
rev-append [] ys = ys
rev-append (x ∷ xs) ys = rev-append xs (x ∷ ys)

Variable scope¶

The pattern variables of the parent clause of the where-block are in scope; in the previous example, these are A and xs. The variables bound by the type signature of the parent clause are not in scope. This is why we added the hidden binder {A}.

Scope of the local declarations¶

The where-definitions are not visible outside of the clause that owns these definitions (the parent clause). If the where-block is given a name (form module M where), then the definitions are available as qualified by M, since module M is visible even outside of the parent clause. The special form of an anonymous module (module _ where) makes the definitions visible outside of the parent clause without qualification.

If the parent function of a named where-block (form module M where) is private, then module M is also private. However, the declarations inside M are not private unless declared so explicitly. Thus, the following example scope checks fine:

module Parent₁ where
private
parent = local
module Private where
local = Set
module Public = Private

test₁ = Parent₁.Public.local

Likewise, a private declaration for a parent function does not affect the privacy of local functions defined under a module _ where-block:

module Parent₂ where
private
parent = local
module _ where
local = Set

test₂ = Parent₂.local

They can be declared private explicitly, though:

module Parent₃ where
parent = local
module _ where
private
local = Set

Now, Parent₃.local is not in scope.

A private declaration for the parent of an ordinary where-block has no effect on the local definitions, of course. They are not even in scope.

Proving properties¶

Sometimes one needs to refer to local definitions in proofs about the parent function. In this case, the module where variant is preferable.

reverse : {A : Set}  List A  List A
reverse {A} xs = rev-append xs []
module Rev where
rev-append : List A  List A  List A
rev-append [] ys = ys
rev-append (x :: xs) ys = rev-append xs (x :: ys)

Rev.rev-append : {A : Set} (xs : List A)  List A  List A  List A

Alternatively, we can define local functions as private to the module we are working in; hence, they will not be visible in any module that imports this module but it will allow us to prove some properties about them.

private
rev-append : {A : Set}  List A  List A  List A
rev-append []        ys = ys
rev-append (x ∷ xs) ys = rev-append xs (x ∷ ys)

reverse' : {A : Set}  List A  List A
reverse' xs = rev-append xs []

More Examples (for Beginners)¶

Using a let-expression:

tw-map : {A : Set}  List A  List (List A)
tw-map {A} xs = let twice : List A  List A
twice xs = xs ++ xs
in  map (\ x  twice [ x ]) xs

Same definition but with less type information:

tw-map' : {A : Set}  List A  List (List A)
tw-map' {A} xs = let twice : _
twice xs = xs ++ xs
in  map (\ x  twice [ x ]) xs

Same definition but with a where-expression

tw-map'' : {A : Set}  List A  List (List A)
tw-map'' {A} xs =  map (\ x  twice [ x ]) xs
where twice : List A  List A
twice xs = xs ++ xs

Even less type information using let:

g : Nat  List Nat
g zero    = [ zero ]
g (suc n) = let sing = [ suc n ]
in  sing ++ g n

Same definition using where:

g' : Nat  List Nat
g' zero = [ zero ]
g' (suc n) = sing ++ g' n
where  sing = [ suc n ]

More than one definition in a let:

h : Nat  Nat
h n = let add2 : Nat

twice : Nat  Nat
twice m = m * m

More than one definition in a where:

fibfact : Nat  Nat
fibfact n = fib n + fact n
where fib : Nat  Nat
fib zero = suc zero
fib (suc zero) = suc zero
fib (suc (suc n)) = fib (suc n) + fib n

fact : Nat  Nat
fact zero = suc zero
fact (suc n) = suc n * fact n

Combining let and where:

k : Nat  Nat
k n = let aux : Nat  Nat
aux m = pred (h m) + fibfact m
in aux (pred n)
where pred : Nat  Nat
pred zero = zero
pred (suc m) = m