Linear Types vs. Uniqueness Typing

Having a limited understanding of type theory, a question popped into my head. Linear types and Uniqueness seem to having a large number of striking similarities, but I imagine they are different in a few ways.

Can someone help me understand the trade-offs when using one or the other (or can one use both?) in the development of programming languages? This of course could range from the difficulty of implementation, to expressiveness, to efficiency.

Best regards,

MJ Stahl

Comment viewing options

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

Dana Harrington's thesis

You may be interested in Dana Harrington's thesis. He compares uniqueness and linear typing in one of the first chapters. I'm not sure that this is the advice you're looking for, but it might give you some theoretical background.

Link no longer there

Can this information be found somewhere else? Can somebody summarize the
difference here (preferably in simple words)?

URL is broken, available on


Nice find. I had tried Google and came up empty. I didn't know that stored PostScript files. Good to know.