4 ms·
Although linear typing is certainly interesting, I think linear typing on its own is not enough. That is, you basically end up with something like Austral where
by YorickPeterse 2y ago
Although linear typing is certainly interesting, I think linear typing on its own is not enough. That is, you basically end up with something like Austral where you use linear types _plus_ some form of compile-time borrow checking, at which point we're back at borrow checking (did I mention it seems inevitable?) :)
- agentultra 2y agoYou did! And maybe it is inevitable? I don't know. It'd be interesting to see different theories evolve, for sure. Maybe something in separation logic will make it's way into mainstream type theory and into compilers at some point. What's cool is how much we're starting to see folks push the boundaries these days. :)
- Kinrany 2y agoWouldn't the borrow checking be simpler when built on top of linear types?
- YorickPeterse 2y agoI don't think the choice of linear vs affine makes much of a difference, but I could be mistaken.