COMP 105 Homework: Type Systems

Due Wednesday, November 9, at 11:59 PM

The purpose of this assignment is to help you learn about type systems.

Setup

Make a clone of the book code:

  git clone linux.cs.tufts.edu:/comp/105/build-prove-compare

You will need copies of build-prove-compare/bare/tuscheme/tuscheme.sml and build-prove-compare/bare/timpcore/timpcore.sml.

Use dell24 server to do your work

For testing and submitting your code, you should use the dell24 server (it contains the correct version of sml and mosml). To do so:

      ssh [cs_user]@dell24.cs.tufts.edu
    

Dire warnings

As in the ML homework, use function definition by pattern matching. In particular, do not use the functions null, hd, and tl.

Individual Problems

Working on your own, please solve the exercises Exercise 8 on page 458 and Exercise 14 on page 459 described below. These exercises are in Volume 2 of the book.

Problem Details

8. Adding lists to Typed Impcore. Do Exercise 8 on page 458 of Ramsey. The exercise requires you to design new syntax and to write type rules for lists. I expect your type rules to be deterministic.

Hint: This exercise 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. I recommend that you do Pair Exercise 2 first. It will give you more of a feel for monomorphic type systems.

Here are some things to watch out for:

14. Polymorphic functions in Typed uScheme. Do Exercise 14 on page 459 of Ramsey. Note that all? should return true when given an empty list (the predicate vacuously holds of all the elements of the list).

Pair Problems

Working with a partner, please solve the exercises Exercise 2 on page 455, Exercise 24 on page 464, Exercise 23 on page 464, and Exercise T described below.

Problem Details

2. Type checking arrays. Do Exercise 2 on page 455 of Ramsey. The course solution to this problem is 21 lines of ML.

24. Type checking polymorphic queues. Do Exercise 24 on page 464 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 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: because empty-queue is not a function, you will have to modify the definition of initialBasis on page 449. That page shows two places you will update: the <<primitive functions for Typed &mu;Scheme [[::] ]>>]] and the [[<primitives that aren't functions, for Typed μScheme ::>.

You may not be able to test your implementation before completing 23.

The course solution to this problem, including the implementation of put above, is under 20 lines of ML.

23. Type checking Typed uScheme. Do Exercise 23 on page 464 of Ramsey: 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 ([x : 'a]) x)))
    ; type is (forall ('a) ('a -> 'a))                      (NEW NOTATION)
    (val e4 (+ 1 #t)) ; extra example
    ; type error
    (val e5 (lambda ([x : int]) (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.

What to submit: Individual Problems

You should submit three files:

How to submit: Individual Problems

When you are ready, run submit105-typesys-solo to submit your work. Note you can run this script multiple times; we will grade the last submission.

What to submit: Pair Problems

For your joint work with your partner, you should submit four files:

How to submit: Pair Problems

When you are ready, run submit105-typesys-pair to submit your work. Note you can run this script multiple times; we will grade the last submission.

How your work will be evaluated

We will use auto-grading to evaluate the functional correctness of your code. We will use the test cases that you submit to evaluate everyone's type checker. You will get points for every bug that your test case triggers. As for structure and organization, we will use the same criteria as in previous homework assignments.

Hints

How to build a type checker

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:

  1. 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.

  2. You can begin by type-checking literal numbers and Booleans.

  3. Add IF-expressions as done in class.

  4. 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.

  5. Implement the rule for function application. You should be able to test all the arithmetic and comparisons from class.

  6. Implement LET binding. The Scheme version is slightly more general than we covered in class. Be careful with your contexts. Implement VAR.

  7. Once you've got LET working, LAMBDA should be quite similar.

  8. Knock off SET, WHILE, BEGIN.

  9. 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.

  10. Knock off the definition forms VALREC and DEFINE. (Remember that DEFINE is syntactic sugar for VALREC.)

  11. 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.)

Finally, take a look at sections 6.6.6-9 in the textbook. They are chock full of useful functions and representations that are already implemented for you.

Let me suggest that you replace the line in the source code

  val fundefs   =
  (* predefined {\tuscheme} functions, as strings (generated by a script) *)

with

      val basis_included = false
      val fundefs = if not basis_included then [] else

This should enable you to test things.

Before submitting, turn the basis back on.

Other advice

Here's some generic advice for writing any of the type-checking code, but especially the queues:

  1. Compile early (you could use the command mosmlc -o tuscheme tuscheme.sml).
  2. Compile insanely often.
  3. Use an editor that jumps straight to the location of the error.
  4. Come up with examples in Typed uScheme.
  5. Figure out how those examples are represented in ML.
  6. Keep in mind the distinction between the term language (values of queue type, values of function type, values of list type) and the type language (queue types, function types, list types).
  7. If you're talking about a thing in the term language, you should be able to give its type.
  8. If you're talking about a thing in the type language, you should be able to give its kind.

Avoid common mistakes

Here are some common mistakes:

A few words about difficulty and time

In Exercise 8 on page 458, I am asking you to create new type rules on your own. Many students find this exercise easy, but many find it very difficult. My 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.

Back to the class home page