Lambda the Ultimate

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.

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.

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

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?

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.

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

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.

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.

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.

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.

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