PLT11 course -- assignment 3

(C) Ralf Lämmel, Andrei Varanovich, University of Koblenz Landau



The following positions can be approached independently.

Presentations by student teams would also just show ONE position.

(You may want to solve several positions to increase chances of presenting.)

If some of the assignments are not sufficiently discussed in the next lab, they can also be carried over to the next week.

1. NB with signed and unsigned integers

We set up NB to provide types for natural numbers and Booleans. Now suppose we replace the type of natural numbers by the type of integers. This would be trivial. (One pleasant side effect though would be that we could redefine the pred operation to be usefully applicable to arbitrary integers, whereas it was previously not usefully applicable to the natural number 0.)

Let us though make this revision somewhat more interesting by distinguishing two types: int for possibly signed integers and uint for unsigned integers (i.e., natural numbers). Revise the type system so that you make an effort to derive the (more restricted and hence more interesting) type uint in cases where this is easily possible whereas you fall back to int in all the other cases.

Please, implement this variation in Prolog.

You would typically start from the following code:

2. Type-safe lambdas

Present the executive summary of the type safety theorem and proof for the simply typed lambda calculus.

(See [TAPL] for details.)

The challenge will be not to rely on too much machinery/details.

Make sure your fellow students understand the idea.

Prepare your presentation in a short text file (.doc, .tex, .pdf).

3. System F

Please, implement the typing rules of System F.

Please, show that you can type-check the definition of the double function.

Important tips in the interest of simplifying your effort:

  • You do not need to implement the evaluation rules; the typing rules are sufficient.
  • You should not build on top of our existing Prolog-based lambda calculi; they are rather complicated.
  • That is, try to implement the 5 typing rules of System F (as shown in the lecture) as is.

If you are an overachiever, please also show that you can type-check the definition of the selfapp function.

4. Tuple subtyping

Consider the extension of the simply-typed lambda calculus for pairs.

Consider also the extension of ditto calculus for extensible records.

Now, please, cook up an extension for tuples of arbitrary arity with subtyping.

What are tuples of arbitrary arity?

  • A tuple of arity 0 is ().
  • A tuple of arity 1 is (true).
  • A tuple of arity 2 is (true, "false").
  • A tuple of arity 3 is (false, "true", 42).
  • etc.

You don't need to implement the extension for tuple subtyping.

Instead focus on developing the few typing and evaluation rules and explain them.

Prepare your presentation in a short text file (.doc, .tex, .pdf).

If you are an overachiever, you would implement this extension such that you can demonstrate it as well.