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 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
in  e’
```

After type-checking, the meaning of this is simply the substitution `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.

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

```f : Nat → List Nat
f zero    = [ zero ]
f (suc n) = let sing = [ suc n ]
in  sing ++ f n
```

Same definition using where

```f' : Nat → List Nat
f' zero = [ zero ]
f' (suc n) = sing ++ f' 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:

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