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
(definejudgmentform).
Background:
The following revision of simplelang equips the language with
types:
;; specifying syntax
(definelanguage simplelang
(st (x = et) (block (dt ...) st ...))
(et x n (+ et et) (coerce t et))
(dt (t x n))
(t int float)
(n number)
(x variablenototherwisementioned))
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)))))
(testequal
(for/and ((ans (list s3 s1 s4 s2)))
(redexmatch? simplelang st ans))
#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:

in the ith declaration of a block, the declared type is equal to
the type of the initial value;

each statement inside of a block satisfies the type constraints;

the declared type of the lefthand side of an assignment is
equal to the type of the righthand side;

similarly, the type of a variable is the specified type of the closest
matching variable declaration;

the type of a number is int if it is a
exactinteger?
and float if it is an flonum?

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
subexpressions.
These rules correspond to those of Algol, C, and Java except that these
languages automatically convert inttyped expressions to
floattyped expressions. In simplelang, you need an
explicit coerce expression to convert a value from one type to
another.
Warning The sidecondition 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 typerelated 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 typerelated elements.
Design the function evalst, which consumes a statement and
determines its behavior according to the untyped reduction semantics. For
the latter step, it strips all typerelated elements. If a statement does
not type check, the function produces error.
Hint I have carefully engineered the above language
definition so that copyandpaste 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 simplelang 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 simplelang language.
Hint You may wish to turn your proof into an executable
metafunction that traces the standard reductions of
simplelang 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.