Assignment 7: Type Checking & Subtyping

Overview

In this assignment, you’ll implement most of the typechecker for Moses, a functional programming language with subtypes.

The goal of this assignment is to understand type systems.¹ To do so, you will need to:

• Understand the rules for a type system and how they work together to provide a formal specification (in other words, “a description in math”) for a typechecker.
• Implement typechecking, by translating the rules of a type system into code.

As with many programming-languages assignments, this one asks you to read and understand much more than it asks you to write code. You might end up writing no more than 60 lines of code (plus, of course, lots of comments), but you should first be sure to understand the rules that you are implementing.

Getting Started

Start by reading the overview of the Moses language. Just skim this file for now, to reinforce your experience from the lab and to notice what is in the file, so you can come back to it later.

Materials

Use the assignment workflow and the link provided on Piazza to get access to this week’s files.

As always, your final submission cannot have syntax or type errors. Functions must have the exact names and types given in the assignment (though you are always encouraged to define other helper functions).

Subtyping [25%]

Pull up the description of Moses’s type system, and read the introductory section and the section on subtypes.

Now you have read the specification of the type system. The implementation of the type system is in Typecheck.hs, included with this assignment. It is incomplete, and it is up to us to finish it.

Our first task will be to finish the code for subtyping, which we will need before we can implement the rest of the type checker.

Your task: In Typecheck.hs, finish the implementations of commonSupertype and commonSubtype.

Implementation Tips

• Be sure to look in MosesAST.hs for the definition of the abstract syntax for types. You can also look at the autogenerated documentation. for this file.

• isSubtype returns true when $x \sqsubseteq y$.

• commonSupertype x y returns the most specific type $t$ that is a supertype of $x$ and $y$. Formally:

  $$x \sqsubseteq t \;\;\wedge\;\; y \sqsubseteq t \;\;\wedge\;\; (\nexists \;t' \neq t : t' \sqsubseteq t \;\wedge\;x \sqsubseteq t' \;\wedge\;y \sqsubseteq t')$$

  Another way of saying this is that it returns the “least upper bound” of $x$ and $y$ (denoted $x \sqcup y$). Such a $t$ always exists—in the worst case ANY is the least upper bound.

• commonSubtype x y returns the most general type $t$ that is a subtype of $x$ and $y$. Formally:

  $$t \sqsubseteq x \;\;\wedge\;\; t \sqsubseteq y \;\;\wedge\;\; (\nexists \;t' \neq t : t \sqsubseteq t' \;\wedge\;t' \sqsubseteq x \;\wedge\;t' \sqsubseteq y)$$

  Another way of saying this is that it returns the “greatest lower bound” of $x$ and $y$ (denoted $x \sqcap y$). Such a $t$ always exists—in the worst case, NONE is the greatest lower bound.

• When you read the code for isSubtype (which is strongly recommended even though this function is complete), notice the “backwardness” of the subtyping rule for function arguments. Similar “backwardness” applies when writing commonSupertype—there is a reason to define commonSubtype as well (they’ll end up mutually recursive!).

Testing

We’ve provided a few automated tests (review the how-to article for information on running tests). You can also add to those tests, and you can manually test your code.

• Automated tests: test/SubtypeSpec.hs contains a small number of automated tests for subtyping.
• Manual testing: You can also manually test your code by loading Typecheck.hs in ghci and calling commonSubtype and commonSupertype directly.

Type Checking [75%]

The main functionality of the type system is defined by the function typeofExpr in Typecheck.hs. This unfinished function checks that an expression is well-typed and returns its type. You should finish the definition of typeofExpr.

Your task: Finish the typechecker, using the type rules described in the type-checking document.

Implementation Tips

• You should always return the most useful and specific type reasonably possible— ANY might be a valid type for everything but it isn’t very useful. (Also, remember that the mythical NONE value is allowed wherever you need it.)

• Sometimes, a type rule requires that a subexpression has a particular type (for example, the subexpression must be a number or a list). There are several useful helper functions that you can use when you recurse in typeofExpr to check subexpressions, including typeofExprWantNumber, typeofExprWantList, etc. which each call typeofExpr but then make sure that the resulting type is of a particular form.

• The code also uses a custom Monad called Fallible which is like the Maybe type, but instead of Nothing can provide a reason why typechecking failed. As a result, your code will probably want to use do notation.

• As you write rules for the different expression cases, you’ll find yourself wanting to do many of the same things each time. Rather than copy and paste code, try to make your life easier by abstracting out common functionality into helper functions.

Testing

There are several kinds of tests you can use to check your code.

• Automated tests: test/TypecheckSpec.hs contains a few tests.

• Manual testing: You can also manually test your code by loading Typecheck.hs in ghci and calling checkTypeof, like so:

        checkTypeof "lambda x => x"            

• Integration tests: test/ProgramSpec.hs contains tests for several Moses programs, located in the test directory. Because these tests use the Moses executable, you need to recompile the executable each time you change your code before rerunning these tests. You can also manually run Moses on a file by (re)loading Moses.hs in ghci and calling runfile:

       runfile "test/okay-var1.mose"
  

Suggested implementation order

Proceed as follows:

1. Typecheck primitive values (Exactly…). This part is done already. Read the code and make sure you understand what it does.

2. Typecheck variables (Var…) by looking them up in the type environment. This part is done already; but read and understand the code.

3. Typecheck tuples (Tuple…). This one is already mostly written. The provided code uses Haskell’s mapM function, which you may want to look up. You just need to finish the code by making it return the right type.

4. Typecheck $\lambda$-expressions. Your code will need a Map.insert call and a recursive call back to typeofExpr on the function body.

5. Typecheck simple (non-tuple) let-expressions. This code isn’t much different from checking $\lambda$-expressions.

6. Typecheck conditionals. We want a BOOL for the condition—one of the helper functions is likely to be handy here. For the result type, commonSupertype will also be useful.

7. Typecheck the list cons operator (:). We single this one out for special treatment because, unlike all the other operators, its arguments have different types. Once again, commonSupertype is your friend (e.g., 1 : ["Foo"] is legal, and has type [ANY]). Also useful is one of the helper functions to make sure the right-hand side typechecks as a list of some kind.

8. Typecheck case expressions. This code is similar to the code for simple lets and the code for if statements. Again, the provided helper functions and commonSupertype are your friends.

9. Typecheck tuple-match let-expressions. The right-hand side needs to be a tuple of the same size as the number of variables. You might find the Haskell functions zip and foldl handy when extending the type environment.

10. Typecheck all the remaining the binary operators. There are a lot, and some are similar, some different. The partial code gives a suggestion for how to handle the constraints and checking. Note that the relational operators are overloaded, they either take two REALs, or they take two STRINGs. The type Fallible is a member of the Alternative typeclass, so the <|> operator may be useful when handling this either/or situation.

11. Typecheck function application. The first expression needs to be “some kind of function”, and the second expression needs to be compatible with the function argument.

You can stop now. All of the graded components are implemented.

However, there is one feature that the typechecker does not currently support: letrec. If you are interested in adding letrec to the typechecker, keep going.

letrec [ungraded & optional]

It’s best to try a couple of different ways to typecheck letrec.

1. First try this: When typechecking the value of the variable, use NONE as the type of the variable. The type of the value will give you a new (hopefully better) type for the variable, which you should use when you typecheck the body of the letrec.

2. The suggested approach above for recursive declarations almost works, but has a subtle bug. It types the following declaration as INT -> INT:

       letrec silly = \n :: INT => if n == 42 then 54 else silly
       in silly
   

   This type isn’t really correct, because if silly has type INT -> INT, then the type of the if statement is the common supertype of INT and INT -> INT, which is ANY, thus the real type of the expression ought to have been INT -> ANY. To address this bug, the easiest approach is relatively simple: do what you did in your original version multiple times.