Uniqueness typing vs Monads
Roland Olsson
The last year or so, I have tried to mostly stick to a purely functional
style when programming in ML, for example avoiding ref's and always using
pure arrays and hash-tables.
Some bugs I have encountered would have been eliminated at compile-time or
write-time instead of run-time with uniqueness typing as in Clean or with
monads as in Haskell.
My code could easily be annotated with uniqueness types whereas a complete
rewrite would be required for monadic style.
Why were monads chosen instead of uniqueness types in Haskell? Do they
have any advantages?
Below is an example of an ML function that produces a list of all
subexpressions of an expression E together with the symbols occuring in
each subexpression and the depth at which it occurs. The variable SoFar is
a state that should have a uniqueness type, which would have prevented a
bug like writing
[ ( E, Set, Depth ] instead of ( E, Set, Depth ) :: SoFar
Have I missed something here? What is the "best" way to write state
transforming code as the one below in a pure way?
fun subs( E : exp, Depth : int, SoFar : ( exp * S.set * int )list )
: ( exp * S.set * int )list =
(* The state SoFar should have a uniqueness type . *)
case E of
app_exp{ func, args = [], ... } =>
let
val Set = if is_variable func then S.singleton func else S.empty
in
( E, Set, Depth ) :: SoFar
end
| app_exp{ func, args, ... } =>
let
(* A state for foldl has the same type as the range type of subs. *)
val (SoFar, Set ) =
foldl
( fn( Arg, (SoFar, Set) ) =>
case subs( Arg, Depth+1, SoFar ) of SoFar as (_,Set',_) :: _ =>
( SoFar, S.union( Set, Set' ) ) )
( SoFar, S.empty )
args
in
( E, S.insert(func,Set), Depth ) :: SoFar
end
| ...
--
Roland Olsson
Department of Computer Science
Ostfold College
Norway
Erik Zuurbier
> Why were monads chosen instead of uniqueness types in Haskell? Do they
> have any advantages?
Trying to understand this, takes a lot of pysychology, which is not my
mug of coffee. Monads do have a disadvantage though. For one, they are
less expressive than uniqueness types, when you have to handle two
objects in parallel or interleaved, where each should be handled in a
single threaded way. To overcome this problem in the case where two
files should be manipulated in an interleaved way, Haskell's designers
resorted to file handles. The result of this was that it was possible
to write some Haskell code that consecutively:
1) opens a file x
2) closes file x
3) write something to file x
Of course this can't possibly work, so Haskell generated a run time
error. With uniqueness types, this error would be caught at compile
time, particularly during type checking.
I wonder if Haskell has improved on this since this example scared me
away.
Regards Erik Zuurbier
j feingold
are for, but they are far more versatile than that. Monads can model
exceptions, concurrency, backtracking calculations (MonadPlus),
generic computations over data structures (Functor), and probably
other things that I haven't seen.
Check out the instance of Monad for Maybe in Haskell. Basically,
whenever a computation returns Nothing, all further computations are
bypassed and the Nothing value is propagated instead. It is
relatively easy to make a data type like Maybe but replace the Nothing
with a data constructor that carries exception information.
I wrote a Monad that has stateful computation with exceptions
together. This one is for an embedded database:
-- Models the result of a function: it either returns a value or
throws an exception.
data Result a = Return a | Throw String
-- This has the classic form used in a state monad, with the addition
of Result in the return type.
data DB a = DB (Database -> (Database, Result a))
instance Monad DB where
return x = DB (\ s -> (s, Return x))
fail e = DB (\ s -> (s, Throw e))
(>>=) (DB c) f =
DB $ \ s ->
let
(s', r) = c s
DB c' =
case r of
(Return x) -> f x -- continue the computation
(Throw e) -> fail e -- propagate the exception (rethrow)
in
c' s'
Not all that complex and exceedingly powerful.
Here is an excellent, straightforward introduction to the topic.
Albert Lai
> Monads can model stateful computations, which is what uniquness types
> are for, but they are far more versatile than that. Monads can model
> exceptions, concurrency, backtracking calculations (MonadPlus),
> generic computations over data structures (Functor), and probably
> other things that I haven't seen.
I am not really adding to this; I am saying this point but in a new
way! A monad is a tool for seperating concerns. We always emphasize
that a monad can model all of the above; we seldom mention that it
does so with great encapsulation.
Suppose you have an algebraically defined type of expressions ---
numbers, variables, expression op expression --- and you wish to write
an evaluator for it, which involves a state (assignment of variables
to values). Then you wish to introduce a division operator and have
exception in case of division by zero. Then you wish to log the
execution trace of the evaluation process bottom-up. Then you wish to
change that to top-down. Then you wish to introduce an extra state
variable to count the number of divisions.
Philip Wadler's Marktoberdorf Lecture "Monads for Functional
Programming" (*) describes how to do this with minimum intrusion. The
main algorithm of the evaluator never changes. You just change the
implementation of the monad and its utility functions, cleanly, for
every of the changes listed above.
In imperative procedural programming, we pride ourselves greatly in
doing this: if a main program uses a stack, we draw the module
boundary so that to change the implementation of the stack from array
to list, or to add accounting of stack operations, or to log traces,
or to produce funny cartoons for kids during each stack operation, we
never need to modify the main program.
In imperative procedural programming, we don't consider procedures and
pointer types to be in competition!
(*) You can find out more about this lecture from
http://www.research.avayalabs.com/user/wadler/topics/monads.html