Due by the start of class on Friday, April 17th

A Type System for Impcore

  1. (Ramsey, Problem 6.2) Prove that type checking for Typed Impcore always terminates. In other words, show that, for any expression e and environment Γ, there is a positive integer n such that if Γ |- e:τ, then the derivation of Γ |- e:τ requires no more than n rule applications, and if there is no type for e, then the proof of this also requires no more than n rule applications.

  2. (Ramsey, Problem 6.4) Prove that every expression in Typed Impcore has at most one type. In other words show that for all environments ξφΓρ> and expression e, there is at most one type τ such that ΓξφΓρ |- e:τ.

  3. (Ramsey, Problems 6.6 and 6.7) Many languages are designed with records and/or union types, also known as product and sum types (Ramsey 6.4). A record is a collection of elements, known as its elements (or "members"). In a statically typed language, these elements are fixed in number and order for each defined record type. Examples include the struct in C and classes without method definitions in C++ and Java. A union is similar to a record in the collection of elements of varios types, but where a record value consists of one of each of its element values, a union value holds only one of its element values at a time. The best known example is the union type in C/C++.

    Ramsey describes type rules for products and sums using numeric indices for the formation of values and extraction of members. In real languages, however, it is more common for the variants to be identified by names, with the number and names themselves definable for new types.

    Give type rules to support the addition of product and sum types to Typed Impcore. Be sure you include rules for formation, introduction, and elimination of both types.

    (To complete this problem, you'll need to study the rules for arrays in Section 6.3, as well as the "interlude" in 6.4. The fact that we have only barely mentioned this material means that you're going be pushed a bit more to figure some of the background out on your own. Pushing you in this way is part of the point of the problem. That being said, don't be shy about asking me for advice, early feedback, etc.)

John H. E. Lasseter