Meta-comment: there is no way I can read that paper and write up an informed & useful comment by the time this leaves the front page. I’d post more research stuff here if this was possible.
On the blog post, I have to question the use of linear types rather than affine types. For those unfamiliar with the distinction, affine types allow you to drop the resource, and linear types don’t. The extra power afforded by linear types is only semantically meaningful in a language where no expressions diverge. In other words, their example
client cannot forget to call receive, resulting in the server blocking on send
is only true in the syntactic sense, the client can of course loop and not call receive. The paper may address this issue, will have to read it to see.
For those interested in reading more about the state of the art on substructural type systems, this paper at ICFP 2016 is pretty cool. The main idea is that there is a lot of similarity between linear arrows and unrestricted arrows, and to use type classes to abstract over both possibilities. This enables better type inference.
That is super neat, outside of the token used for syntax, wonder what release this is scheduled to get into, 8.4 I presume?