CMSC 22300, Spring 2012
Take Home Final (for graduating students)
Due Midnight, Wednesday, May 30.

1. [20] Prove that the Maybe and Reader monads satisfy the algrebraic
laws for monads.  The proofs proceed by expanding the definitions
of the monad operations and symbolic evaluation.  The laws are:

  1. return x >>= f    ==  f x
  2. mv >>= return     ==  mv
  3. (mv >>= f) >>= g  ==  mv >>= (\x -> (f x >>= g))

----------------------------------------------------------------------
  An alternate composition operator for monads is:

    (>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)
    f >=> g  =  \x -> (f x >>= g)

  In terms of this operator, the monad rules turn out to have the
  simpler forms:

  1. return >=> f       ==    f
  2. f >=> return       ==    f
  3. (f >=> g) >=> h    ==    f >=> (g >=> h)

  If you prefer, you can verify these versions of the laws, using
  definitions of >=> derived from the corresponding definition of
  >>= for Maybe and Reader.
----------------------------------------------------------------------
Use file name "prob1.txt".


2. [15] Option monad (option/Maybe chaining)

In SML, define monad operatons (>>= (or "chain") and return) for the
option type constructor (the ML analogue of the Maybe monad). Use
these to rewrite the following nested explicit case analysis in a
streamlined form using option monad operations:

  fun repl env =
      case TextIO.inputLine TextIO.stdIn
	 of NONE => NONE
	  | SOME line =>
	    (case (T.tokenize(S.fromString line))
	       of NONE => NONE 
		 | SOME (toks,_) =>
		   (case (P.stmt toks)
		      of NONE => NONE
		       | SOME(s,_) =>
			  let val (res,env') = V.evalStmt env s
			   in printStmt res;
			      repl env'
			  end))

where

   TextIO.inputLine : TextIO.instream -> string option
   T.tokenize : token list reader
   P.stmt : expr parser

   type 'a reader = char stream -> ('a * char stream) option
   type 'a parser = token list -> ('a * token list) option

[This is a simplified version of the REPL function for the
calculator. You do not need to compile and test your solution.]
---------
Use file name "prob2.sml".


3. [30] Regular expressions (over characters) can be represented by the
following data type:

   data RE = Empty       -- the empty r.e., matches immediately
                         --   without consuming any characters
           | C Char      -- singleton character: C c matches the
                         --   character c
           | Seq RE RE   -- sequencial composition: Seq A B matches A
	                  --   followed by B  (normally written AB)
           | Alt RE RE   -- alternative composition: Alt A B matches 
                         --   either A or B (normally written A|B)
           | Star RE     -- Kleene star: Star R matches zero or more
                         --   repetitions of R (normally written R*)

We can define various utility functions to build regular expression
values, for instance, (reChars cs) matches any character in the list cs:

   reChars :: [Char] -> RE
   reChars = foldr (\c -> \re -> Alt (C c) re) Empty

   digits :: RE
   digits = reChars ['0'..'9']

   reString :: String -> RE
   reString = foldr (\c -> \re -> Seq (C c) re) Empty

Write a function

   recognize :: RE -> Reader String

translating an RE value into a reader monad action such that
(recognize re) returns a string that is the longest prefix of
the input stream that matches the regular expression. Thus if
the input stream starts with ['a','b','c','d',...] and the
regular expression is (a | ab), the reader should finish with
Just("ab",['c',...]).

Note that this is rather similar to a tokenizer reader, except that we
are looking for the longest match rather than the first match in
alternatives.
-------------
Use file name "prob3.hs" (or "prob3.sml" if you prefer to do the
problem in SML).


4. [15] Give a fully detailed manual typing of the following
definition (in the style of "working-typing-examples.txt" on
the Handouts page):

   fun f (x,p,u) =
       let fun g (y,z) = if p(y) then z else x::nil
	in g (3,u)
       end;

---------
Use file name "prob4.txt".


5. [30] Lambda Calculus
The pure lambda calculus can be represented as follows:

type var = string

datatype exp
  = Var of var
  | Abs of var * exp
  | App of exp * exp

Examples are 

    x       (Var "x")
    λx.x    (Abs ("x", Var "x"))
    x y     (App (Var "x") (Var "y"))
    (λx.λy.x)(λu.u)
            (App(Abs("x",Abs("y",Var "x")), Abs("u",Var "u")))

A β-redex is an expression of the form (λx.M)N, and it can be
reduced by "β-reduction" to [N/x]M (substitute the argument
expression N for x in the body expression M):

    (λx.M)N  -->β  [N/x]M

Care must be taken when defining substitution to avoid free
variable capture, as in:

   [λx.y / u]λy.uy  =  λy.(λx.y)y   (Wrong!)

We use α-conversion (change of bound variables) to avoid the
capture:

   [λx.y / u]λy.uy  =  [λx.y / u]λz.uz    (λy.uy == λz.uz)
                    =  λz.(λx.y)z

An expression is in normal form if it contains no β-redexes
(i.e. subexpressions of the form (λx.M)N).

Implement the following (in SML):

a) capture avoiding substitution:

    val subst : var * exp * exp -> exp  (subst(x,N,M) = [N/x]M)

b) test for normal form:

    val isNormal : exp -> bool

And, for 10 points extra credit:

c) an evaluator that uses β-reduction repeatedly to reduce
an expression to normal form:

    val eval : exp -> exp

This should use "normal order reduction", which means that the
left-most, outermost β-redex should be reduced at each step.
[Note: The eval function will not always terminate.  Can you
give an example which does not?]

-------------
Use file name "prob5.sml".