An exciting looking preprint by , , and clarifying the difference between linear types and uniqueness types: starsandspira.ls/docs/esop22-dr
read image description
ALT
2
11
48
Conversation
I see lots of confusion out there with regards to the differences between linearity and uniqueness, and I've been pretty confused too, so I'm glad they are trying to clarify things! It's going to take me longer to digest the technical stuff, but it seems helpful so far!
1
2
I like the these quotable sections that they added:
🥴 “Misconception 1. Linearity and uniqueness are two different words for the same concept / linearity and uniqueness are essentially the same.”
🥴 “Misconception 2. Linearity and uniqueness are “dual” to one another.”
1
1
🤩 “Takeaway: Linearity and uniqueness behave dually with respect to composition, but identically with respect to structural rules, i.e., their internal plumbing.”
1
1
Anyway, I think it's exciting to see that we might be able to combine these together in languages like Granule, along with supporting other things like relevant and affine types. Something like this could be rather handy for systems programming!
![Figure 2. from the paper. The relationship between the various flavours of substructural type is shown, demonstrating how they can all be represented using Granule's modalities.
A directed graph is drawn as follows:
• unrestricted types (written as either `a [0..∞]`, or `a [Many]`, or `!a`) are uniqueness types (written as `*a`) that forget the guarantee of no contraction. they are non-linear and non-unique.
• affine types (written as `a [0..1]`) are unrestricted types that restrict contraction.
• relevant types (written as `a [1..∞]`) are unrestricted types that restrict weakening.
• linear types (written as either `a [1]` , or just `a`) are formed either by affine types that restrict weakening, or relevant types that restrict contraction.](https://pbs.twimg.com/media/FIJjBEnUYAEb-Nz?format=jpg&name=large)
read image description
ALT