4 ms·
> the linear arrow says this: a function that has type A⊸BA⊸B is a function that has an AA available to compute with, but it can only use it once. Not twice, no
by _bxg1 6y ago
> the linear arrow says this: a function that has type A⊸BA⊸B is a function that has an AA available to compute with, but it can only use it once. Not twice, not zero times: just once.
Superficially this sounds a lot like Rust's FnOnce. Is there a relation there?
Edit: Actually it sounds like linear functions are more about using their arguments once, internally, as opposed to themselves being called once. So perhaps not. Still would appreciate any further commentary by someone with a better grasp on things than I have.
- archgoon 6y agoLinear types are stronger than FnOnce, in that a linear type must be used _exactly_ once. Rust doesn't enforce that if you pass in a function of type FnOnce that it is called.
- weavie 6y agoThats interesting. I don't quite understand how that would work. So can you work around that requirement by just going: if false then <use my type> else <do my things> Technically it is used exactly once, but really it will never be used..
- comex 6y agoThat wouldn't work, because the value must be used in all possible control paths. In this case, both the 'then' and 'else' branch would have to use the value.
- deleted 6y ago[deleted]
- maemre 6y agoLinear type systems often enforce that requirement by saying both branches need to use exactly the same linear values (or consume the same resources). So your example would be rejected by the type system. For example, the following function would not type check in a linearly-typed language because then branch is using x while else branch is not using x. -- Using Haskell-like syntax, '-o' is linear arrow, i.e. lollipop foo : Int -o Int -o Int foo x y = if y < 0 then x else 0
- nicoburns 6y agoRust's ownership system has Affine types (types which must be used 0 or 1 times), which are indeed closely related to Linear types, which must be used exactly once. Types marked with `#[must_use]` in Rust are pretty close to linear types. But must_use is a lint rather than being integrated with the type system. See also: https://gankra.github.io/blah/linear-rust/ https://gankra.github.io/blah/linear-rust/
- masklinn 6y ago> Types marked with `#[must_use]` in Rust are pretty close to linear types. But must_use is a lint rather than being integrated with the type system. An other issue with must_use is that it just requires use not “consumption” of the value, so if, say, you print it the lint is satisfied. Meaning it’s an issue for resources you’d want to be linear e.g. resources which really should be explicitly terminated because the termination can fail.
- baq 6y agoUh so how do you debug linearly typed code if you can’t log values? Or does ghc allow to cheat?
- masklinn 6y agoI don't know if GHC provides either, but either a borrowing or a dup feature would handle that (the latter would probably count as "cheat"). There may be other ways as well. Since linear types are a separate opt-in feature you'd probably need (as far as I understand) you'd need separate printers anyway, so you could probably "cheat" them in. Though I think the sort of structures you'd want to be linear would generally not be amenable to print-debugging anyway.
- platz 6y ago> We say that a function f is linear when f u is consumed exactly once implies that u is consumed exactly once (defined as follows). - Consuming a value of a data type exactly once means evaluating it to head normal form exactly once, discriminating on its tag any number of times, then consuming its fields exactly once - Consuming a function exactly once means applying it and consuming its result exactly once https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst#definition https://github.com/ghc-proposals/ghc-proposals/blob/master/p...
- platz 6y agoLinearity Design Space: https://i.imgur.com/s0Mxhcr.png https://i.imgur.com/s0Mxhcr.png