Assignment #3: COS 441
Due by midnight on Wednesday Oct. 8. Email all completed assignments
to Rob at rdockins@princeton.edu. Please put "COS 441 A3" in the
subject line of any such email.
There are 15 points to gain on this assignment.
Question 1. [4 points] In order to program effectively in SML, you need to be
able to understand the type inference error messages that the compiler will
tell you when you make a mistake in a program. The goal of this
problem is make as few changes as possible to the files a.sml, b.sml
and c.sml so that they type check. In other words, don't change 2 lines
when you could change 1 line in the file. Don't change 2 operators when
you could change 1 operator. (I'm not going to be super-strict about this
but basically I want to see if you can exactly pinpoint where the type
error is in the file and change it.) Hand in your changed versions of
a.sml and b.sml.
To solve this problem, start sml interpreter. At the prompt, type
use "a.sml";
then look at the error message you get. Then use the information in
that error message to make a change to the file so that it type
checks. Try doing "use a.sml" again to see if there are any more
errors. Repeat until there are no errors. Do this for both a.sml and
b.sml. The files are here:
http://www.cs.princeton.edu/courses/archive/fall08/cos441/notes/a3code/
For your reference, here's a list of error messages:
http://www.smlnj.org/doc/errors.html
Error [54] is *particularly* common and [55] happens somewhat frequently too.
At the very bottom of the page, there are some warnings that happen often
too, particularly [1] and [2]. You should remove any such warnings as well.
Question 2 [1 point]: Give an example of an expression that could
generate this kind of error message:
[opening myprog.sml]
myprog.sml:1.1-1.8 Error: operator and operand don't agree [literal]
operator domain: int * int
operand: int * bool
in expression:
... <<<======= you supply the expression
Question 3 [10 points]
Here is the definition of a simple logic with true, false,
inequalities, conjunction and disjunction. (We used this logic
in the last assignment too.) The formulas F are the following:
F ::= true | false | n1 <= n2 | F1 /\ F2 | F1 \/ F2
The truth of a logical formula is determined by judgements with the form
|- leq n1 n2 and |- F
Here are the rules for |- leq n1 n2:
------------ (Z-LEQ)
|- leq Z n2
|- leq n1 n2
--------------------- (S-LEQ)
|- leq (S n1) (S n2)
Here are the rules for proving |- F:
-------- (T)
|- true
|- leq n1 n2
-------------- (LEQ)
|- n1 <= n2
|- F1 |- F2
----------------------- (/\)
|- F1 /\ F2
|- F1 |- F2
------------------ (\/1) ----------- (\/2)
|- F1 \/ F2 |- F1 \/ F2
Now, download the file logic.sml from here:
http://www.cs.princeton.edu/courses/archive/fall08/cos441/notes/a3code/logic.sml
and fill in the missing definitions.