Due date: 10/26 @ at the beginning of class

Purpose: The goal of this problem set is to understand the role of types and type checking. In addition, you will demonstrate that you can expand your knowledge of a computing system (Redex) on your own (define-judgment-form).

---

Background:

The following revision of simple-lang equips the language with types:

  ;; specifying syntax 
  (define-language simple-lang 
    (st (x = et) (block (dt ...) st ...))
    (et x n (+ et et) (coerce t et))
    (dt (t x n))
    (t  int float)
    (n  number)
    (x  variable-not-otherwise-mentioned))

Here are the examples from the last problem set, adjusted to this new syntax:

  (define s1 
    (term (block ((int x 0) (int y 1)) (x = (+ x 1)) (y = x))))

  (define s2 
    (term
     (block ((int x 8) (int y 9))
	    (x = 0)
	    (block ((int z 9))
		   (x = 0) 
		   (z = 2))
	    (y = 1))))

  (define s3
    (term (block ((int x 0)) (block ((int x 9)) (x = (+ x 1))))))

  (define s4
    (term (block ((int x 0)) (block ((int y 9)) (block ((int z 3)) (y = x))))))

  (define s5
    (term (block ((int x 0)) (x = 1) (x = (+ x 1)))))

  (test-equal
   (for/and ((an-s (list s3 s1 s4 s2)))
     (redex-match? simple-lang st an-s))
   #t)

Use this code to create your solution file.

Problem 1:

Design the type judgment check, which consumes a statement st and checks whether st satisfies the type constraints. In particular, check enforces the following constraints:

1. in the ith declaration of a block, the declared type is equal to the type of the initial value;
2. each statement inside of a block satisfies the type constraints;
3. the declared type of the left-hand side of an assignment is equal to the type of the right-hand side;
4. similarly, the type of a variable is the specified type of the closest matching variable declaration;
5. the type of a number is int if it is a exact-integer? and float if it is an flonum?
6. the types of the two subexpression of an addition expression are equal and the type of the addition expression is the same as the type of its two sub-expressions.

These rules correspond to those of Algol, C, and Java except that these languages automatically convert int-typed expressions to float-typed expressions. In simple-lang, you need an explicit coerce expression to convert a value from one type to another.

Warning The side-condition of judgments differs from those of reduction rules and meta functions.

Problem 2:

Once the type checker has checked the constraints for a statement st, it is possible to strip all type-related information from st to determine its behavior via the standard reduction relation.

Copy and paste the relevant pieces of your standard reduction relation from problem set 6 into your solution file. Correct any mistakes that were pointed out.

Design the function strip, which consumes a statement st and strips all type-related elements.

Design the function eval-st, which consumes a statement and determines its behavior according to the untyped reduction semantics. For the latter step, it strips all type-related elements. If a statement does not type check, the function produces error.

Hint I have carefully engineered the above language definition so that copy-and-paste should work without problem. -- In principle, a semantics engineer would organize such a model in several files and import the untyped reduction relation.

Implementations for languages such as Algol have used type information to compile and run code. Stripping type information was common for languages such as SML; for example, the SML/NJ implementation used to translate its input to Scheme.

Problem 3:

Claim: All programs (typed or untyped) in simple-lang terminate. Articulate the central proof idea in 20 words or less.

Design the function size, which displaylns the size of statements s in the untyped simple-lang language.

Hint You may wish to turn your proof into an executable metafunction that traces the standard reductions of simple-lang programs and confirms your conjecture. Doing so requires some learning about traces and a modicum of Racket knowledge. Follow this hint only if you have time.

Deliverable:

Send in a single Racket file. Its name should consist of the two last names in alphabetical order separated with a hyphen; its suffix must be .rkt.

Your file must start with the following two lines:

  ;; NameOfPartner1, NameOfPartner2 
  ;; email@of.partner1.com, email@of.partner2.com

appropriately instantiated of course. Also separate problems with lines of the shape ";; " followed by 77 "-". That gives you a width of 80 chars. Try to stick to this width for all of your code; it ensures basic readability.