Rust'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/

> 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.

Uh so how do you debug linearly typed code if you can’t log values? Or does ghc allow to cheat?

I 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.

> 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/p...

Linear 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.

Thats 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..

Linear 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

That 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.

Just curious, what is considered as 'using' the value?

Passing it as a parameter to a function or returning it

Or applying it if that value is a function. I believe the broader definition would be that it has to appear in an "evaluated" term.

Linearity Design Space: https://i.imgur.com/s0Mxhcr.png