Re:Idris 2: Quantitative Type Theory in Practice
by gadmm on Monday January 24, 2022 @09:22AM
(#30057878)
Baker's paper is visionary in that it announces a link between linear logic and move semantics for resources more than a decade in advance. As we know this was put into practice by C++ and Rust. Compared to linear types, it amounts to operating a change of perspective from the quantitative interpretation (is it copied? is it dropped?) to a qualitative one (how is it copied? how is it dropped?). This is very much in spirit of linear logic (though it takes a bit of work to relate these ideas to Girard's mathematics). It answers questions that linear types were never able to, such as how to mix linearity and control. I take this paper as an example that there is more to linear logic than linear types!
A good practical description of linear logic (but not types) is here: https://hashingit.com/elements/research-resources/1994-03-Fo...
Yes it's about how Forth implements linear logic without realizing it ;).