Hacker News Reader

Comment by greg7mdp | Hacker News Reader

Incredible work, congrats, the evolution of GHC is quite impressive. A better description of what linear types can be useful for is at https://www.tweag.io/blog/2017-03-13-linear-types/.

View on HN

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

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

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.

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

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.

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

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

-XLinearTypes down, -XDependentTypes to go :)

Once that happens, the world will change :)

Wadler might argue that linear types being merged changed the world!

http://www.cs.ioc.ee/ewscs/2010/mycroft/linear-2up.pdf

Haskell still has sort of a way to emulate dependent types in many practical cases, without a ton of work or a huge performance hit [1].

Direct support could be nice, though.

[1]: http://okmij.org/ftp/Computation/lightweight-static-guarante...

Tweag is onto that too. :)

See https://www.reddit.com/r/haskell/comments/gtnayl/whats_the_s... for a recent update.

Reply on news.ycombinator.com