This was just posted the other day on the "Morning Paper" blog: https://blog.acolyer.org/2018/01/24/linear-haskell-practical-linearity-in-a-higher-order-polymorphic-language
The "linear function arrow" concept reminds me a bit of the destructor logic laid out for Nim, especially the "sink" annotation.
Is there any insight in their linear calculus that could be applied to the Nim destructor calculus?
Perhaps proving linearity makes the case for the note in "Flaw 1" to use a sink parameter.
"Flaw 2" is harder because Exceptions are not a thing in pure functional languages like Haskell... You could model an exception as a linear monad that takes all "sink" variables in the environment at the time as arguments, but that is basically equivalent to the hidden boolean flag discussed on the wiki page.
Is there any insight in their linear calculus that could be applied to the Nim destructor calculus?
There are certainly lots of similarities but I haven't studied Haskell's solution enough to be able to answer this question. :-)
I haven't studied Haskell's solution enough to be able to answer this question.
:-D lol. That's a good reason