The purpose of this assignment is to help you learn about type systems.
git clone linux.cs.tufts.edu:/comp/105/book-codeYou will need copies of book-code/bare/tuscheme/tuscheme.sml and book-code/bare/timpcore/timpcore.sml.
As in the ML homework, use function definition by pattern matching.
In particular, do not use the functions null
, hd
, and tl
.
I recommend that you do Exercise 2 first (with your partner). It will give you more of a feel for monomorphic type systems.
Hint: Exercise 1 is more difficult than it first appears. I encourage you to scrutinize the lecture notes for similar cases, and to remember that you have to be able to type check every expression at compile time.
Here are some things to watch out for:
11. Do Exercise 11 on page 275 of Ramsey: write exists? and all? in Typed uScheme. Turn in this exercise in file 11.scm.
15. Do Exercise 15 on page 276
of Ramsey:
extend Typed uScheme with a type constructor for queues
and with primitives that operate on queues.
As it says in the exercise, do not change the
abstract syntax, the values, the eval
function, or the type
checker.
If you change any of these parts of the interpreter, your
solution will earn No Credit.
I've made one change to the exercise: instead of implementing
get
,
implement the two functions get-first
and get-rest
.
This change will save you from having to deal with pair types.
The change is reflected in
two updated pages from the book.
I recommend that you represent each queue as a list.
If you do this, you will be able to use the following primitive
implementation
of put
:
let fun put (x, NIL) = PAIR (x, NIL) | put (x, PAIR (y, ys)) = PAIR (y, put (x, ys)) | put (x, _) = raise BugInTypeChecking "non-queue passed to put" in put end
Turn in the code for this exercise in file tuscheme.sml, which should also include your solution to Exercise 13 below. Please include the answers to parts (a) and(b) in your README file.
Hint: because empty-queue is not a function,
you will have to modify the initialEnvs
function on page 270b.
The updated pages from the book
show two places you will update: the
<primitive functions for Typed μScheme
and the
::
><primitives that aren't functions, for Typed μScheme
.
::
>
My solution to this problem, including the implementation of put
above,
is under 20 lines of ML.
13.
Do Exercise 13 on page 275 of Ramsey:
write a type checker for Typed uScheme.
Turn in this exercise in file tuscheme.sml, which should also
include your solution to Exercise 15 above.
Don't worry about the quality of your error messages, but do
remember that your code must compile without errors or warnings.
My solution to this problem is about 120 lines of ML.
It is very similar to the type checker for Typed
Impcore that appears in the book.
If I had given worse error messages,
it could have been a little shorter.
T. Create three test cases for Typed uScheme type checkers. In file type-tests.scm, please put three val bindings to names e1, e2, and e3. (A val-rec binding is also acceptable.) After each binding, put in a comment the words "type is" followed by the type you expect the name to have. If you expect a type error, instead put a comment saying "type error". Here is an example (with more than three bindings):
(val e1 cons) ; type is (forall ('a) (function ('a (list 'a)) (list 'a))) (val e2 (@ car int)) ; type is (function ((list int)) int) (val e3 (type-lambda ('a) (lambda (('a x)) x))) ; type is (forall ('a) (function ('a) 'a)) (val e4 (+ 1 #t)) ; extra example ; type error (val e5 (lambda ((int x)) (cons x x))) ; another extra example ; type errorIf you submit more than three bindings, we will use the first three.
The only really viable strategy for building the type checker is one piece at a time. Writing the whole type checker before running any of it will make you miserable. Instead, start with small pieces similar to what we'll do in class:
It's OK to write out a complete case analysis of the syntax, but have every case raise the LeftAsExercise exception. This trick will start to get you a useful scaffolding, in which you can gradually replace each exception with real code. And of course you'll test each time.
You can begin by type-checking literal numbers and Booleans.
Add IF-expressions as done in class.
Implement the VAL rule for definitions, and maybe also the EXP rule. Now you can test a few IF-expressions with different types, but you'll need to disable the initial basis as shown below.
Implement the rule for function application. You should be able to test all the arithmetic and comparisons from class.
Implement LET binding. The Scheme version is slightly more general than we covered in class. Be careful with your contexts. Implement VAR.
Once you've got LET working, LAMBDA should be quite similar.
To create a function type, use the funtype
function in
the book.
Knock off SET, WHILE, BEGIN.
Because of the representation of types, function application is a bit tricky.
Study the funtype
function and make sure you
understand how to pattern match against its representation.
There are a couple of different ways to handle LET-STAR. As usual, the simplest way is to treat it as syntactic sugar for nested LETs.
Knock off the definition forms VALREC and DEFINE. (Remember that DEFINE is syntactic sugar for VALREC.)
Save TYAPPLY and TYLAMBDA for after the last class lecture on the topic. (Those are the only parts that have to wait until the last lecture; you can have your entire type checker, except for those two constructs, finished before the last class.)
Let me suggest that you replace the line in the source code
val basis = (* ML representation of initial basis *)with
val basis_included = false val basis = if not basis_included then [] elseWith luck this will enable you to test things.
Before submitting, turn the basis back on.
car
or cdr
to the empty list.
Don't do this!
It can be done, but by the standards of COMP 105, such type systems
are insanely complicated.
As in ML, taking car
or cdr
of the empty list should be a
well-typed term that causes an error at run time.
ledit ./timpcoreJust plain timpcore will get the system version.
eqType
function to see if two types are equal.
If you use built-in equality, you will get wrong
answers.
val-rec
form requires an extra side condition; in
(val-rec x e)it is necessary to be sure that
e
can be evaluated without
evaluating x
.
Many students forget this side condition, which can be implemented
very easily with the help of the function appearsUnprotectedIn
,
which should be listed in the ``code index'' of your book.
ListPair.foldr
and
ListPair.foldl
when what was really meant was ListPair.foldrEq
or
ListPair.foldlEq
.
Exercise 11, writing exists? and all? in Typed μScheme, requires that you really understand instantiation of polymorphic values. Once you get that, the problem is not at all difficult, but the type checker is very, very persnickety. A little of this kind of programming goes a long way.
Exercise 2, type-checking arrays in Typed Impcore, is probably the easiest exercise on this homework. You need to be able to duplicate the kind of reasoning and programming that we did in class for the language of expressions with LET and VAR.
Exercise 15, adding queues to Typed μScheme, requires you to understand how primitive type constructors and values are added to the initial basis. And it requires you to write ML code that manipulates μScheme representations. Study the way the existing primitives are implemented!
Exercise 13, the full type checker for Typed µScheme, presents two kinds of difficulty:
timpcore.sml
,
tuscheme.sml
, and type-tests.scm
. In addition to your code, please
provide a short README
file which describes, at a high level, the design
and implementation of your solutions.
README
file containing the following information:
README
, lists.pdf
and 11.scm
.
All files are mandatory.