Unification Monad

AFP Exercise 2: Monad Transformers

Start file: Infer.zip. This file should contain:

• Infer.hs
• UU_BinaryTrees.hs
• UU_Parsing_Core.hs
• UU_Parsing_Derived.hs
• UU_Scanner.hs

In the second exercise, we will use a number of standard, pre-defined monads. More precisely, you will have to combine monads by using monad transformers. Documentation of available functions can be found in the hierarchical libraries (see Control.Monad and Control.Monad.*).

You are given a working type inferencer for a small expression language, including a scanner and a parser. The parser is included only to help you test your type inferencer. You will have to adjust the Haskell module Infer.hs: the others are library files.

The first step is to compile the program as you received it: this can be done by calling

ghc --make -fglasgow-exts -o Infer.exe Infer

This should produce an executable Infer.exe. Experiment with the type inferencer. You are given a prompt, and after you entered a valid expression, the type inferred for this expression is displayed. Here is a possible session:

   _   ___ ___
  /_\ | __| _ \        A Monadic Type Inferencer
 / _ \| _||  _/                (May 2005)
/_/ \_\_| |_|

> \f x -> f (f x)
\f -> \x -> f (f x) :: (a -> a) -> a -> a
> \x y -> if True then x else y fi
\x -> \y -> if True then x else y fi :: a -> a -> a
> let id = \x -> x in id id 3 ni
let id = \x -> x in id id 3 ni :: Int
> \f -> f x

Fail: #4: Unbound variable "x"

The last expression is not valid since it is not closed (it contains an unbound variable). The type inferencer aborts as soon as something unexpected (e.g., it encounters an unbound variable) happens. Make sure that you have a good understanding of the given code before you continue with this exercise.

The goal is to improve the readability of the code by using monads (and monad transformers). The only monad that is currently used is the IO monad (for the main functions only). Furthermore, you are asked to implement a number of additional features. The modifications that you have to make are limited to the following program parts:

• 5. Type inference utility functions
• 6. Type inference
• 7. Main functions

Step 1: Introducing the monad

The first candidate monad is, obviously, the state monad. As you may have noticed, the functions inferScheme and inferType thread some values in a regular way. These aspects of type inference may (or may not) be modeled by making them part of a state that is kept in the monad. The type inference utility functions too (code part 5) are candidates to be rewritten as a monadic computation.

See Question 1: this might give you some inspiration.

Step 2: Failure is an option!

The program contains four locations where it may crash (the 4 calls to the function error). Adjust the code such that a nice error message is presented (for all 4 cases), and such that the program is not aborted. That is, after entering an invalid expression, the user is confronted with some error message, after which he can type in another one.

Optional: In case of a type error, generate error messages that resemble to some level the error message generated by the Hugs interpreter.

Prelude> :t (True False)
ERROR - Type error in application
*** Expression     : True False
*** Term           : True
*** Type           : Bool
*** Does not match : a -> b

ERROR - Type error in application
*** Expression     : x x
*** Term           : x
*** Type           : a -> b
*** Does not match : a
*** Because        : unification would give infinite type

Step 3: Debugging type inference

To gain more insight in the progress of the type inference algorithm, debugging messages should be reported to the user before the inferred type is presented. Again, you have to use a monad to facilitate debugging. Information you may want to display:

• Two types are being unified by the type inference algorithm
• A type variable is mapped to some type in the (current) substitution
• An identifier is added to the type environment (Gamma) with some type scheme
• A subexpression is assigned some type

Ofcourse, more relevant debugging information is welcome! Just to give you some idea, the following output might be the result of entering \f x -> f x.

> \f x -> f x
("f",v0) in Gamma
("x",v1) in Gamma
f :: v0
x :: v1
Unifying v0 and v1 -> v2
v0 := v1 -> v2
f x :: v2
\x -> f x :: v1 -> v2
\f -> \x -> f x :: (v1 -> v2) -> v1 -> v2

\f -> \x -> f x :: (a -> b) -> a -> b

Hint: try to localize your code for debugging. Typically, one location should be enough.

Step 4: Extending the prompt

The last part of this exercise requires some IO programming. In addition to typing in some expression, the user can also type in one of the following three commands:

• :q - leave the program
• :debug on - enable showing debugging information
• :debug off - disable showing debugging information

Like Hugs and ghci, commands always start with a colon (:). Give a warning if an unknown command is entered. By default, you may assume debugging to be turned off.

Questions to be answered

Question 1: The code of inferType could have been generated by the Attribute Grammar System. In fact, some values correspond closely to inherited, chained, and synthesized attributes. What is the relation between these three categories of attributes on the one hand, and the role they play when using a state monad on the other hand?

Question 2: Comment on the monad you have chosen to use. Are there alternative ways to assemble your monad? Also explain why certain aspects are included in the state monad (and also, why certain information is kept outside the monad).