Chapter 1Foundationsslides.en.pdf:99-101

Declarations and Scope

How identifiers are introduced and where they live

Def 2.6 — DeclarationDef 2.7 — ScopeDef 2.8 — Naming complex objects

Concept

A declaration introduces an identifier into scope. In mathematics (and SML):

Simple definition: $\text{gcd}(a, b) :=$ (some expression).
Pattern definition: $\text{succ}(0) := 1, \text{succ}(s(n)) := s(\text{succ}(n))$ .
Implicit definition / description: "the smallest $x$ such that $P(x)$ ".

The scope of an identifier is the part of an expression where it refers to
its declaration. Outside the scope, the name is either unbound or shadows
another declaration.

Examples/counterexamples: To prove a $\forall x. P(x)$ statement, a single
$x$ where $P(x)$ fails is enough — a counterexample.

Animation — declarations scope

Transcript — click a line to jump8 cues

0.0sDeclarations and Scope
1.1sAn outer cyan rectangle: let outer in ... end
2.2sAn inner amber rectangle: let inner in ... end
3.6sOuter binding: x = 5
4.7sInner binding: x = 99 (shadows the outer)
6.3sArrow from outer binding to its use x = 5
7.5sArrow from inner binding to its use x = 99
9.0sInner binding shadows the outer one

Practice — score 100% to advance

Multiple choice

What is a declaration?

What is the scope of an identifier?

Which is a counterexample to 'every prime is odd'?

Pattern definitions are useful when…

Loading…