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)
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:
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
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 (h m) + fibfact m
in aux (pred n)
where pred : Nat → Nat
pred zero = zero
pred (suc m) = m