For most languages, types are not needed at run-time. Consider this type erasure function.
erase(x) erase(λx : T1.t2) erase(t1 t2)
= λx.erase(t2)
= erase(t1) erase(t2)
By careful design, we have:
t → t′ =⇒ erase(t) → erase(t′).
Proved by induction on evaluation derivations.
erase(t)→m′ =⇒ ∃t′ |t →t′ ∧erase(t′)=m′
J. Carette (McMaster University) Types Fall 2023 1 / 15
Curry Style language definition
The approach we have followed:
Start with terms representing desired behaviours (syntax). Formalize those behaviours using evaluation rules (semantics). Use a typing system to reject undesired behaviours (typing).
This is often called a Curry-Style language definition, because semantics are given priority over typing.
i.e., we can remove the typing and still have a functional system.
J. Carette (McMaster University) Types Fall 2023 2 / 15
Church Style language definition
A different approach is as follows:
Start with terms representing desired behaviours (syntax). Identify the well-typed terms using typing rules (typing). Give semantics only to well-typed terms (semantics).
Under Church-Style language design, typing is given priority.
Questions like “How does an ill-typed term behave?” don’t occur, because ill-typed term cannot even be evaluated!
Historically:
▶ Explicitly typed languages have normally been presented Church-Style.
▶ Implicitly typed languages have normally been presented Curry-Style.
Thus Church-style is sometimes confused with explicit typing (and vice-versa for Curry).
J. Carette (McMaster University) Types Fall 2023 3 / 15
Atomic Types
PLs provides a set of atomic types, often including:
Booleans (B), Natural Numbers (N), Integers (Z), Characters, Strings, etc.
Do not confuse floats for Real Numbers (R)! We will avoid all talk of both floats and reals in this course.
These are sometimes known as primitives. These are normally accompanied by a set of primitive operations, such as:
+, −, ×, ==, &&, ||, etc.
Adding these is very easy, with the only difficulty appearing when we try to
add partial functions.
J. Carette (McMaster University) Types Fall 2023 4 / 15
Atomic Type Semantics
Augment language with a set A of uninterpreted base types.
Helpful in the following examples:
(λx :A.x):A⇒A
(λf :A⇒A.λx :A.f (f x)):(A⇒A)⇒A⇒A
J. Carette (McMaster University) Types Fall 2023 5 / 15
程序代写 CS代考 加QQ: 749389476
Statements
What does := return ?
J. Carette (McMaster University) Types Fall 2023 6 / 15
Statements
What does := return ? It doesn’t, but it has a side-effect on memory. So: how do we type side-effects?
Let us first do “sequencing”. Easiest done by first introducing a Unit type.
J. Carette (McMaster University) Types Fall 2023 6 / 15
Unit Type Semantics
J. Carette (McMaster University) Types Fall 2023 7 / 15
Sequencing
In languages with side effects, want to “execute” some commands.
Solution? Make commands return value unit.
Sequencing of commands is then denoted ;
As usual, can add it to language as a new term, or make it derived.
J. Carette (McMaster University) Types Fall 2023 8 / 15
As a New Term
Grammar: ⟨t⟩ ::= …
| ⟨t⟩ ; ⟨t⟩ Evaluation rules:
t 1 → t 1′
t 1 ; t 2 → t 1′ ; t 2
unit; t2 → t2
Γ⊢t1 :Unit Γ⊢t2 :T2
Γ ⊢ (t1;t2) : T2
(E-Seq) (E-SeqNext)
Typing rule
J. Carette (McMaster University) Types
Fall 2023 9 / 15
Derived Form Approach
As smaller languages mean smaller proofs…
t1;t2 =(λx:Unit.t2)t1 (1) Which throws away the value associated to t1 (in call-by-value semantics),
and yields t2
J. Carette (McMaster University) Types Fall 2023 10 / 15
Surface vs Core Language
Derived forms are everywhere in modern programming languages, where they are often called syntactic sugar.
They allow the programmer to use the language more easily by providing abstractions of the language used by the compiler.
Ultimately, however, programs must be desugared before object code generation.
▶ Higher-level constructs are replaced with equivalent terms in the core language.
This forms the distinction between:
The external language, or that of the programmer.
The internal language, or what the compiler (eventually) works with.
J. Carette
(McMaster University) Types Fall 2023 11 / 15
Sequencing is a Derived Form
Definition
λE as the simply typed λ-Calculus, enriched with Unit, unit, t1;t2, E-Seq, E-SeqNext, and T-Seq.
Definition
λI as the simply typed λ-Calculus, Unit type and unit term only.
Define e ∈ λE → λI as a meta-level elaboration function. It replaces all
instances of t1; t2 with (λx : Unit.t2) t1.
THEOREM [Sequencing is a Derived Form] For each term t of λE , we
t −→ t ⇐ ⇒ e ( t ) −→ e ( t ) Γ ⊢E t : T ⇐⇒ Γ ⊢I e(t) : T
J. Carette (McMaster University) Types Fall 2023 12 / 15
浙大学霸代写 加微信 cstutorcs
Ascription Semantics
“We say that t has type T” – this is not casting!
This is most useful once we introduce polymorphism, but is already useful as documentation.
J. Carette (McMaster University) Types Fall 2023 13 / 15
Let Bindings: naming sub-expressions
Semantically, we want (let x = t1 in t2) to evaluate to a substitution of x for t1 in t2.
J. Carette (McMaster University) Types Fall 2023 14 / 15
Programming Help
Let semantics
Intuitively, we want:
letx =t1 int2 = (λx :T1.t2)t1
But where does T1 come from?
Best to think of let-in as a fusion of λ and application. We have t1 in our hands, use it!
Have two options:
▶ Regard elaboration as a transformation on typing derivations.
▶ Decorate terms with the results of typechecking.
So: evaluation semantics of let bindings can be desugared, but the typing behaviour must be built into the inner language.
J. Carette (McMaster University) Types Fall 2023 15 / 15