Exceptions with monads ...


--------------------------------------------------------

I am continuing to use literate Haskell ...  

There is an important high-order class defined in Haskell called
Monad (which unfortunately in the prelude is now defined based
on having an "Applicative" which in turn is defined on having a
"Functor"!).

Let me go ahead and set up the success or fail type as a monad --
which is a bit complicated (in my humble opinion unnecessarily so!!) due
to these inter-dependencies which have been enforced by the prelude.
(This is perhaps a by-product of the industrialization of Haskell).

Let us not worry too much about what it all means at the momment but
rather try to see what the effect of having an exception monad for
programming.  We will exemplify it on the code for unification ...


> data SF a = SS a | FF
>    deriving (Eq,Show)

> instance Functor SF where
>       fmap f FF = FF
>       fmap f (SS x) = SS (f x)

> instance Applicative SF where
>         pure x = SS x
>         FF <*> _ = FF
>         (SS f) <*> m = fmap f m

> instance Monad SF where
>         return x = SS x
>         (SS x) >>= k = k x
>         FF >>= _ = FF

Here is the rewritten sflist and the helper functions myhead and mytail:

> sflist:: [SF a] -> (SF [a])
> sflist [] = SS []
> sflist (a:as) = do a' <- a
>                    as' <- sflist as
>                    return (a':as')

The "do" syntax is what we must understand.  We may read the last phrase
of the code above as:

"do, get the successful part of a, assign it to a' now recursively get the
successful part of as, assign it to as' now return (as successful) a':as'"

Note how the tracking of the failure condition (or the exception) is now
automatically handled.  This makes the code look a little neater ... and is
easier to understand.


Now let us rewrite the unification program using the success or fail monad
which we have now set up.  First as before -- no change -- we need expressions
and substitution:

> data Exp f v  = Opn f [Exp f v]
>               | Var v
>    deriving (Show,Eq)

> foldExp:: (f -> [c] -> c) -> (v -> c) -> (Exp f v) -> c
> foldExp opn var (Var v) = var v
> foldExp opn var (Opn f args) = opn f (map (foldExp opn var) args)

> type Sub f v = (v,Exp f v)
> type Subs f v = [(v,Exp f v)]

> substitution:: Eq v => (Exp f v) -> (Sub f v) -> (Exp f v)
> substitution t (v,s) = foldExp Opn (\w -> if v==w then s else Var w) t

> substitutions:: Eq v => (Exp f v) -> (Subs f v) -> (Exp f v)
> substitutions t = foldr substitution t 

> e1 = Opn "add" [Opn "mult" [Var 1,Var 2],Var 1]
> e2 = Opn "mult" [Var 6,Var 7]
> e3 = Opn "add" [Var 1,Opn "mult" [Var 6,Var 7]]
> e4 = Opn "add" [Var 1,Opn "mult" [Var 1,Var 2]]
> e5 = Opn "add" [Var 9,Var 10]
> subs1 = [(1,e2),(2,e1)]

Here is our occurs check (also unchanged):

> occurs_check::(Eq f,Eq v) => (Sub f v) -> (SF (Subs f v))
> occurs_check (v,t)| t == (Var v) = SS []
>                   | occurs v t = FF
>                   | otherwise = SS [(v,t)]
>     where
>           occurs v = foldExp (\_ -> foldr (||) False) ((==) v)

Here is the matching function (note the last phrase):

> matching::(Eq f,Eq v) => (Exp f v,Exp f v) -> (SF (Subs f v))
> matching ((Var v),t) = occurs_check (v,t)
> matching (s,(Var v)) = occurs_check (v,s)
> matching ((Opn f1 args1),(Opn f2 args2))
>   | f1 == f2 && (length args1) == (length args2)
>         = do ssubs <- sflist $ map matching $ zip args1 args2
>              return (concat ssubs)
>   | otherwise = FF

In the linearizing we can use the exception monad more significantly to our advantage:

> linearize:: (Eq v, Eq f) => (Subs f v) -> (SF (Subs f v))
> linearize subs = linearize_helper [] subs
>      where
>         linearize_helper:: (Eq v,Eq f) => (Subs f v) -> (Subs f v) -> (SF (Subs f v))
>         linearize_helper (lin_subs) [] = SS lin_subs
>         linearize_helper lin_subs (sub:subs) =
>             do nsubs <- subout sub subs 
>                linearize_helper (sub:lin_subs) nsubs  -- reify sub!

Substituting out also is made much neater using the exception monad:

> subout:: (Eq f,Eq v) => (Sub f v) -> (Subs f v) -> SF (Subs f v)
> subout _ [] = SS []
> subout sub@(x,t1) ((y,t2):rest)
>            | x==y =      do msubs <- matching (t1,t2)
>                             subouts <- subout sub rest
>                             linearize (msubs++subouts)
>            | otherwise = do subst <- occurs_check (y,(substitution t2 sub))
>                             subouts <- subout sub rest
>                             return (subst ++ subouts)

This leaves the unify functions themselves:

> unify t1 t2 = do subs <- matching (t1,t2)
>                  linearize subs

and the parallelized  substitutions:

> parallelize:: Eq v => (Subs f v) -> (Subs f v)
> parallelize = foldr subsubstitutes [] where
>   subsubstitutes:: Eq v => (Sub f v) -> (Subs f v) -> (Subs f v)
>   subsubstitutes sub subs = sub:(map (\(x,s) -> (x,substitution sub s)) subs) 
>
> punify t1 t2 = do lin_subs <- unify t1 t2
>                   return (parallelize lin_subs)

Using the exception monad makes the code a bit neater ...