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. This means that let-bound functions have to make sense as pure lambda expressions: they can not be recursive, and can not be defined by pattern matching on inductive types.
Example:
f : Nat
f = let h : Nat → Nat
h m = suc (suc m)
in h zero + h (suc zero)
However, it is possible to match on record types in the left-hand side of a let-bound function, as described below:
g : Nat
g = let h : Nat × Nat → Nat
h (x , y) = x + y
in h (1 , 2)
A let-expression has 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.
Warning
The internal syntax used by Agda does not have let-expressions as a construct. As a result, Agda inlines all let-bound variables during type checking. In particular, let-binding cannot be used to introduce sharing.
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.
If R lacks eta-equality, e.g. by being declared with no-eta-equality,
then warning ShouldBeEtaRecordPattern is triggered (since Agda 2.9.0).
Let binding record patterns
Let-expressions can be used to locally open a module. For example:
let z = x + y
open M z
in u -- using definitions from M
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.
No named where-modules under with or rewrite
Since Agda 2.9.0, a clause that uses
with-abstraction — be it via with,
rewrite, or with p ← e —
must not carry a named where-module. The following is rejected with
error NamedWhereModuleUnderWith:
f : Bool → Bool
f x with x
... | true = local
module M where -- rejected since Agda 2.9.0
local = false
... | false = true
The reason is that with-abstraction can change the types of the module
parameters that M inherits from its parent module.
However, these changed parameters are not visible in the source code which might be confusing.
Ignoring the changes, i.e., making M available outside of the clause with the original module parameters inherited from the parent module, even leads to
inconsistencies.
Ordinary anonymous where-blocks are unaffected by this restriction,
and so is using p ← e, which does not with-abstract
but introduces a let-binding:
ok : Bool → Bool
ok x with x
... | true = local
where
local = false
... | false = true
ok' : Bool → Bool
ok' x using y ← x = local
module M' where
local = y
If you need to refer to the local definitions from outside the clause, define them in a proper module instead, or move the with-abstraction into a helper function.
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)
This gives us access to the local function as
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:
h : Nat → List Nat
h zero = [ zero ]
h (suc n) = let sing = [ suc n ]
in sing ++ h n
Same definition using where:
h' : Nat → List Nat
h' zero = [ zero ]
h' (suc n) = sing ++ h' n
where sing = [ suc n ]
More than one definition in a let:
i : Nat → Nat
i n = let add2 : Nat
add2 = suc (suc n)
twice : Nat → Nat
twice m = m * m
in twice add2
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 (i m) + fibfact m
in aux (pred n)
where pred : Nat → Nat
pred zero = zero
pred (suc m) = m