Exercise 4.

This is a bonus exercise. You will receive 4 extra marks if you can explain how to modify the grammar and the type checker of Exercise 3 such that the revised language has

• functions returning not only primitive types but also functions,
• local definition-declarations in function bodies.

As a hint, we give the revised rule for generating functions types

T $\longmapsto$ A₁$\bf\rightarrow$$\bf ($T₂$\bf )$

Here's a program that must be accepted by the revised grammar and type checker.

f: integer -> (integer -> (integer));
f(n: integer): integer -> (integer) == {
    g: integer -> (integer);
    g(m: integer): integer == { n + m; };
}

Only a brief explanation is needed, not a translation scheme.

Answer 4