Home » forums » LtU Forum

Tradeoffs between Unique Types and Monads

Hello everyone,

I am currently trying to understand what the trade-offs are between uniqueness typing and monads. On the surface uniqueness typing seems a little easier to grasp and read (code wise), but it seems there is a lot of fascination with Monads.

I was curious how one would judge whether to use one or the other in order to model side-effects in a pure functional language. Which strategy gives the most 'bang-for-the-buck' in regards to language semantics but also in regards to learning curve?

Thank you everyone in advance for being so helpful. =)

Regards,

-M.

By mjstahl at 2005-12-14 04:01 | LtU Forum | previous forum topic | next forum topic | other blogs | 18434 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Monads

Uniqueness typing is interesting, but it doesn't even begin to cover all the uses of monads. So your question is ill-stated unless you restrict it specifically to their overlap.

That said, implementation(semantics)-wise monads for IO and some other things simply require adding primitive operations to the language. Further, monads are abstract and thus more of the details of how are supressed. Uniqueness typing, obviously, requires a more sophisticated type system, but this does pay off in some other ways. There are things you can do with uniqueness typing that are awkward for monads.

Learning-wise, to just start off and use monads is dead simple. Or at least certainly no more complex than using uniqueness types. However, monads are a more general concept and are used in a variety of ways (and can model side-effects e.g. continuations that uniqueness typing cannot). Even then my impression is that the main difficulties people complain about are trying to think up (or understand) how to make a monad that models some particular effect and not so much the idea of monads in general. I.e. they confuse the difficulty with coming up with a way to model, say, exceptions or continuations with a difficulty of the idea of a monad itself. While these aspects can be difficult they are somewhat independent of the monad concept. To help there a look at how these effects are modeled in denotational semantics is probably most useful. However, in practice this still isn't particularly necessary as there are libraries of monads and monad transformers that make the need to "implement" a particular monad "from scratch" unnecessary.

By Derek Elkins at Wed, 2005-12-14 16:44 | login or register to post comments

Monads == uniqueness typing?

Although I understand monads and uniqueness typing, I do not seem to grasp their differences, if there are differences. To me, they are both mechanisms for forcing sequencing of operations and thus being able to replace values instead of creating new ones (the sequencing guarrantees that the previous value goes unneeded). Does anyone have a link that explains the differences? or better yet can explain the differences themselves?

By Achilleas Margaritis at Wed, 2006-10-11 15:29 | login or register to post comments

Monads /= uniqueness typing

Well, if I understand correctly, uniqueness typing is one of the so-called "sub-structural" type systems. They are called this because they are obtained by eliminating some of the structural rules that one is usually allowed to use on type judgement environments. For example, you get linear types by restricting the permutation structural rule. See Advanced Topics in Types and Programming Languages for more on sub-structural typing.

Monads are more of a design philosophy than a feature of a type system. It happens to be possible to encode side-effect sequencing using monads; one way to do this is to invent a dummy data item representing the "state of the world", and carefully regulating the ways in which this token can be created and consumed. It also happens that monads have a nice representation as type operators in type systems related to F_omega.

Both techniques can be used to persuade a compiler to generate code that performs side-effects in the right order. Other than that, it doesn't seem to me that they have a lot in common.

By Rob Dockins at Wed, 2006-10-11 16:56 | login or register to post comments

I still not understand why they are considered different.

The practical outcome is the same. Maybe the idea comes from a different context, but the result is that both approaches do exactly the same thing: they serialize computations, thus allowing the compiler to perform side effects.

By Achilleas Margaritis at Thu, 2006-10-12 09:44 | login or register to post comments

But they're not...

But the practical outcomes are not the same. For one, you cannot use uniqueness types to model continuations.

By genneth at Thu, 2006-10-12 10:33 | login or register to post comments

Thanks. But...

Can a variable of a unique type (which is assignable) be used to capture a program's state and then use that to restore the program's state, effectively modelling a continuation?

And is that the only difference between monads and unique types?

By Achilleas Margaritis at Thu, 2006-10-12 12:04 | login or register to post comments

The foundations are totally

The foundations are totally different. Monads happen to support a notion of sequencing, and unique types enforce a particular one. There isn't sensible syntactic sugar for unique types that generalises let and letrec, and monads don't need explicit support from the type system. Monads can't express anything genuinely new to a language without support for specific monads from the run-time system, though they make a good model for understanding what you already know how to do. To the best of my knowledge (I may be missing a technique or two) uniqueness types don't offer the same kind of control over side-effects that monads do - try encoding and enforcing the state usage patterns of the Reader and Writer monads with them. But you can't easily use monads to enforce 'conservation' properties either.

They're different tools, they do different things and I've got uses for both, potentially at the same time.

By Philippa Cowderoy at Thu, 2006-10-12 14:15 | login or register to post comments

Well...

...I am not a Clean programmer, nor a Haskell one, but from what I have understood so far I think it is quite feasible to do the analogous of Reader and Writer monads in Clean. All it takes is to create a few unique types and some 'conversion' functions between them.

I wish someone could elaborate on this - it would be really helpful.

By Achilleas Margaritis at Thu, 2006-10-12 15:34 | login or register to post comments

Actually you could use

Actually you could use monads in practicaly any language, even thougt you need some kind of macro system or syntax extension to make them look nice. They realy are just a way to make pure implementations of impure effects. They don't need any compiler suport, the compiler sees nothing but pure functional code.

Unique types are nearly the opposite. They allow impure implementations to look pure functional on the outside. And in some sense they are just compiler optimisations, that isnt even visible outside of the compiler. (assuming that the unique type could be infered.)

The tricky bit is that Haskell have some monads that don't have pure implementation. And a pure implementation of the IO monad would actualy require something like unique types. So thats a connection. But they realy are far from the same.

By Felicia Li Svilling at Thu, 2006-10-12 18:36 | login or register to post comments

A pure implementation of the

A pure implementation of the IO monad only requires unique types to make it provably safe within the type system. I'm not sure I find this an entirely meaningful notion for something that allows a system to eg fire an ICBM at its own location.

By Philippa Cowderoy at Fri, 2006-10-13 01:39 | login or register to post comments

With a pure implementation i

With a pure implementation i meant an implementation that only used pure features (but i see that it can be interpretated in other ways.) And I think the standard definition of a pure feature is a feature that is guaranteed (by the typesystem) to not have any unpure side effects.

By Felicia Li Svilling at Fri, 2006-10-13 12:42 | login or register to post comments

Sure. It's also possible to

Sure. It's also possible to give a denotational semantics to IO, at which point you can indeed describe as a pure function the process of nuking your own host system. The result is a universe in which your host system's been vapourised.

By Philippa Cowderoy at Fri, 2006-10-13 12:47 | login or register to post comments

I can't see how you'd get

I can't see how you'd get the constraints compared to plain old State. With Reader, state changes only propagate 'inwards', in a manner similar to lexical scope. But once you go out again, you can use that over and over again - you just don't get to return the current environment outwards. How would you enforce that?

By Philippa Cowderoy at Fri, 2006-10-13 01:30 | login or register to post comments

Perhaps...

...by using the lexical scope or closures? the uniquely typed variable does not need to escape the scope of the function it belongs to...and with closures, it can be moved to any desired point as a 'black box' without actually be visible to the outward environment.

By Achilleas Margaritis at Fri, 2006-10-13 09:19 | login or register to post comments