Granule, a statically-typed linear functional language with graded modal types
25 points by aziis98
25 points by aziis98
Tip: I think what everyone secretly wants (but nobody understands the cryptic substructural type system nomenclature of) is a language that has types that are linear in lifetime, not use. Exactly like Rust is affine in lifetime, not use. Add borrowing?
What some people call "move-only" and Wikipedia calles resource-linear: https://en.wikipedia.org/wiki/Substructural_type_system#Resource-linear_types
Could you explain this distinction between lifetime and use linearity more?
Like Rust without destructors (or panic): Think what Rust did to constructors from C++: Replaced them with normal functions. Now, do the same for destructors: A variable of a type that can hold a resource (not Copy) must end its lifetime exactly once in every code path, just like it must begin exactly once in every code path. Yes, the destruction problem is the time-symmetric equivalent of the construction problem! The program might as well run backwards.
So instead of the compiler (implicitly) inserting calls to destructors for variables of types that have destructors, the compiler verifies that the programmer has done so (explicitly). Except in this world, there are no constructors or destructors, just functions. Functions that through their signature create, consume and borrow variables. A variable begins its lifetime when a function creates (moves into) it, ends its lifetime when a function consumes (moves out of) it, and can be "used" (borrowed) 0 to infinity number of times inbetween.