The purpose of this assignment is to help you learn about type systems.
If you have not done so already, get a copy of the book code:
git clone data.cs.purdue.edu:/homes/cs456/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
.
Working on your own, please solve the exercises Exercise 8 on page 452 and Exercise 14 on page 453 (of Volume 1 of the book) described below.
Working with a partner, please solve the exercises Exercise 2 on page 449, Exercise 24 on page 458, Exercise 23 on page 458, and Exercise T described below.
2. Type checking arrays. The course solution to this problem is 21 lines of ML.
24.
Type checking polymorphic queues.
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 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
Hint: you will modify two parts of the code that build the initial basis. Both parts are shown under “Building the initial basis” on page 443. Your definitions of empty?
, put
, get-first
, and get-rest
can go next to primitives null?
, cons
, car
, and cdr
. But because empty-queue
is not a function, you will add its definition in a different place, as ⟨primitives that aren’t functions, for Typed μScheme ::
1295e⟩. In the (book) code, look for the comment
(* primitives that aren't functions, for \tuscheme\ [[::]] 1295e *)
A couple of lines below, you will see an empty list. Edit the list to add a triple containing the name, value, and type of empty-queue
.
The course solution to this problem, including the implementation of put
above, is under 20 lines of ML.
23. Type checking Typed uScheme. Write a type checker for Typed uScheme. Don't worry about the quality of your error messages, but do remember that your code must compile without errors or warnings. The course 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 the code gave worse error messages, it could have been a little shorter.
T. Test cases for type checkers. Create three test cases for Typed uScheme type checkers. In your test file, 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) ('a (list 'a) -> (list 'a))) (NEW NOTATION) (val e2 (@ car int)) ; type is ((list int) -> int) (NEW NOTATION) (val e3 (type-lambda ('a) (lambda (('a x)) x))) ; type is (forall ('a) ('a -> 'a)) (NEW NOTATION) (val e4 (+ 1 #t)) ; extra example ; type error (val e5 (lambda ((int x)) (cons x x))) ; another extra example ; type error
If you submit more than three bindings, we will use the first three.
Each binding must be completely independent of all the others. In particular, you cannot use values declared in earlier bindings as part of your later bindings. PLEASE MAKE SURE YOU FOLLOW THE ABOVE DIRECTIONS EXACTLY.
You should submit three files:
When you are ready, run turnin -c cs456 -p typesys-solo README lists.pdf typesys-forall.scm from your working directory to submit your work. All files are mandatory.
For your joint work with your partner, you should submit four files:
For your joint work with your partner, use
turnin -c cs456 -p typesys-pair README timpcore.sml tuscheme.sml type-tests.scmfrom a directory that contains the following files:
timpcore.sml
,
tuscheme.sml
, and type-tests.scm
.
For your type checker, it would be a grave error to copy and paste the Typed Impcore code into Typed uScheme. You are much better off simply adding a brand new type checker to the tuscheme.sml interpreter. Use the techniques presented in class, and start small.
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:
funtype
function in
the book.
funtype
function and make sure you
understand how to pattern match against its representation.
We 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 [] else
This should enable you to test things.
Before submitting, turn the basis back on.
Here's some generic advice for writing any of the type-checking code, but especially the queues:
Here are some common mistakes:
car
or cdr
to the empty list.
Don't do this!
It can be done, but by the standards of CS 456, 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.
rlwrap ./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
.
In Exercise 8, we ask you to create new type rules on your own. Many students find this exercise easy, but many find it very difficult. Our sympathy is with the difficult camp; you haven't had much practice creating new rules on your own.
Exercise 14, 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 24, 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 23, the full type checker for Typed µScheme, presents two kinds of difficulty:
For the first item, we'll talk a lot in class about the concepts and the connection between type theory and type checking. For the second item, it's not so difficult provided you remember what you've learned about building big software: don't write it all in one go. Instead, start with a tiny language and grow it very slowly, testing at each step.