10 Written: Types

These are due by midnight on Thursday, April 2.

Constraint Solving

Note: This problem is useful to do as practice while thinking through type inference.

Consider the following typed expression:

(lam (f : T1) -> T2
  (lam (x : T3 ) -> T4
    (lam (y : T5 ) -> T6
      (link x (f (f y))))))

The notation (-> T) refers to the annotated return type of the function. The types have been left unspecified (Tn) to be filled in by the type inference process. Derive type constraints from the above program. Then solve these constraints. From these solutions, fill in the values of Tn. Be sure to show all the steps specified by the algorithms (i.e., writing the answer based on intuition or knowledge is insufficient). You should use type variables where necessary. To save writing, you can annotate each expression with an appropriate type variable, and present the rest of the algorithm in terms of these type variables alone (to avoid having to copy the corresponding expressions). If you do this, be sure to annotate every sub-expression with a type variable.

Ocaml Type Errors

We talked in class, lab, and the notes about how type inference errors can be different from type checking errors for the same program. Write an Ocaml program with a type mismatch for which Ocaml reports a different error when you remove an annotation than when you put the correct annotation in. Present the essence of the example (don’t present an entire 100 line program), and give a plausible explanation for what is happening behind the scenes, contrasting type checking and inference, that results in the differing errors. Feel free to modify your Ocaml interpreter from lab in order to show the difference.

Datatype Design

Note: This question is more open-ended than the others. It reflects the kinds of decisions you would confront when designing a new language. There are lots of ways to go about answering. To avoid writing too much keep your answer to less than 500 words (this entire assignment writeup is around 650 words, for a feel of how much that is).

We have handled lists in our type checker by making both link and empty expressions type to (List T) types. That means that the type system doesn’t catch not-a-link errors on first and rest: they are in the allowed error set.

On the Web, you read a proposal for a better design: Suppose, instead, each variant creates a new type, call them (Link T) and (Empty T). Then you can give a precise type for the selector (e.g. first and rest would give a type error on (Empty T) typed arguments, only succeeding if the argument has type (Link T)). This would turn the dynamic check into a static one, thereby increasing the effectiveness of the type system. Because this was proposed on Twitter, it’s frustratingly short on details.

Can we build an effective type system out of this idea? If so, how, and if not, why not? If we can’t as stated, can we turn this into something that actually works? Have you seen any languages that do something like this? Hint: Coming up with a decent definition of what you argue makes a type system "effective" will go a long way towards constructing a good argument.

Inferring (a -> b)

It’s straightforward to write a program whose inferred type is (a -> a).

It’s harder to write a program whose inferred type is (a -> b).

One way to do it is to write a function that results in an error when applied, but has the desired type:

(lam (x) (first empty))

Can you write a program whose inferred type is (a -> b), but doesn’t evaluate to an error when applied to some value?

If so, give the program and describe its runtime behavior. If not, describe what you tried and argue why no such program exists.