Unification Monad

Afp0405
---+ AFP Exercise 2: Monad Transformers

*Start file*: [[%ATTACHURL%/Infer.zip][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 
[[http://www.nomaware.com/monads/html/transformers.html][monad transformers]].
Documentation of available functions can be found in the 
[[http://www.haskell.org/ghc/docs/latest/html/libraries/][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
<verbatim>
ghc --make -fglasgow-exts -o Infer.exe Infer
</verbatim>
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:
<verbatim>
   _   ___ ___
  /_\ | __| _ \        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"
</verbatim>
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.

<verbatim>
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
</verbatim>

---+++ 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=. 

<verbatim>
> \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
</verbatim>

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).
Topic attachments
I	Attachment	Action	Size	Date	Who	Comment
zip	Infer.zip	manage	15.6 K	03 May 2005 - 15:59	BastiaanHeeren	Sources for Exercise 2