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