6 ms·

Well. There goes the library ecosystem until everyone finally realizes this extension doesn't do what they want. sigh To expand a bit further: This extensio

Well. There goes the library ecosystem until everyone finally realizes this extension doesn't do what they want. sigh To expand a bit further: This extension allows annotating function types with linearity information. The problem is that those modified function types control what is allowed to happen inside them. They have no impact on how values are used outside them. This is the big difference between linear typing and uniqueness typing. Uniqueness typing lets you say "this function is the only thing using this value." It's possible to use this extension to assemble something sort of like uniqueness, but the ergonomics are pretty awful and no one bothered working through all the ugly details like exception handling in the context of a real application. I really don't believe this is ever going to be better than existing techniques. But it's absolutely going to make the library ecosystem permanently worse, as lots of packages will get linearity annotations added. Lots of forks will arise without them, for the people who don't want the hassle. Finding the library you actually want is just going to get even more complicated. I still don't understand how this happened. Every strong objection was just ignored. What's the point of even having a public comment process when it makes no difference to the outcome?

pgustafs 6y ago
From https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types : "The centrepiece of our design is to avoid code duplication. Crucially, the same types can be used in linear and non-linear contexts. For example, the linear-base library uses the same types as base. So libraries developed with linear-base will be compatible with libraries developed with base."
- tuukkah 6y ago
  Why can't base and linear-base be the same implementation too?
  - nimih 6y ago
    The proposal discusses this briefly[1]. The idea seems to be that datatypes themselves remain identical (constructors being linear by default, even with -XNoLinearTypes), but functions are allowed to have more precise signatures. edit: I'm not knowledgeable enough about this stuff to know if the idea is to just refine the type signature but keep implementations identical, or whether implementations themselves need to change. [1] https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst#base https://github.com/ghc-proposals/ghc-proposals/blob/master/p...
    - tuukkah 6y ago
      Thanks for the pointer! Emphasis mine: "Because linear functions only strengthen the contract of unrestricted functions, a number of functions of base can get a more precise type. However, for pedagogical reasons, to prevent linear types from interfering with newcomers' understanding of the Prelude, this proposal does not modify base. Instead, we expect that users will publish new libraries on Hackage including more precisely typed base functions. One such library has already started here."
      - srtjstjsj 6y ago
        Prelude needs to change its name to Pedagogue. It's drifting ever farther from how people use the language to solve real problems.
pjmlp 6y ago
From the looks of it this isn't done anyway, just a stepping stone to get to the final destination. Just like value types, modules and concepts in other languages, sometime big bangs require incremental additions to the stable language instead of big bangs.
- whateveracct 6y ago
  This is the core argument of the detractors. They say they -XLinearTypes isn't Enough. They want a Big Bang. But it was already very hard work to get this incremental step. A Big Bang is even more work. And the detractors don't have a semblance of an alternative :/ but that hasn't stopped thousands of words of FUD from being spilled online.
  - pjmlp 6y ago
    That is why we cannot have nice things, when those pushing their ideas don't have an hard skin to fight against those kind of issues. Though job. :\
creata 6y ago
* So is it appropriate to say that in linear types a callee says "I will use this exactly once", and in uniqueness types a callee says "I need exclusive access to this"? * Is there an obvious way to translate from one to the other? * Rust's type system sounds a lot closer to uniqueness types than linear or affine types. So why do so many people in this thread say that Rust has affine types?
- akiselev 6y ago
  > * Rust's type system sounds a lot closer to uniqueness types than linear or affine types. So why do so many people in this thread say that Rust has affine types?* Rust enforces exclusive access through ownership, which is orthogonal to linear/affine typing. Linear types must be used, affine types must be used at most once. Rust's compiler doesn't force code to use types like Futures or Result, at best it emits a warning, so a missing await or match statement can compile without doing what the code is intended to do. In a linear type system, you can mark Futures and Results so that the compiler throws an error when they're created but not consumed by an operation like awaiting or error handling.
nimih 6y ago
It seems inconsistent to claim both a) this proposal/implementation has bad ergonomics and doesn't solve real problems, and b) the library ecosystem will become irreparably fragmented as library authors rush to incorporate it or provide linear forks. Surely if enough people are expending the effort to bring -XLinearTypes to a non-trivial portion of the extant Haskell universe, it is by definition both useful and at least somewhat ergonomic?
- whateveracct 6y ago
  It is inconsistent. -XLinearTypes detractors have been making this paradoxical argument for months now. If it's useful, people will use it to build libraries. If it's not, it's all fine. The FUD from Haskellers depresses me. My consolation is I'll get to build useful shit with -XLinearTypes on GHC mainline now - things detractors told me weren't possible because they were too busy complaining about its imperfection.
  - kreetx 6y ago
    The detractors are just a minority, right? Where do they criticize(?), reddit and the mailinglists have seemed pretty clean.
    - whateveracct 6y ago
      There have been multiple reddit posts full of long essay comments against the extension. Including a text post itself about it. They are clearly a minority though. But very vocal.
- dllthomas 6y ago
  It may be inaccurate but it's not inconsistent. Things can sound like a good idea, be embraced enthusiastically by people who haven't had a chance to work with them, and only later reveal serious ergonomic issues once people have a chance to use them in anger.
mrkeen 6y ago
> this extension doesn't do what they want It seems that you are the one wanting Linear types to be Uniqueness types instead. > no one bothered working through all the ugly details like exception handling in the context of a real application. Citation needed? > it's absolutely going to make the library ecosystem permanently worse, as lots of packages will get linearity annotations added > Lots of forks will arise without them, for the people who don't want the hassle How would the situation be different for Uniqueness types?
whateveracct 6y ago
> I really don't believe this is ever going to be better than existing techniques. The paper has examples of how it's better than existing method (such at the ST trick). Took me like an hour to read the entire thing months ago. Strong objections weren't ignored - they just weren't especially compelling. And when pressed for an alternative, nobody could come close to something of the rigor of what was merged. This entire comment is FUD and the fact that it's at the top of HN is such a PITA. Now I'm gonna have to hear even more people copy-paste argue against the extension instead of making real progress. This isn't going to make the library ecosystem worse. Please just edit that statement of "fact" out of your comment for all our sakes. That's all okay though. I'll go make some video games with type-safe manual memory management thanks to this extension :) that's the power of not complaining when things aren't as perfect as you can imagine them.
- auggierose 6y ago
  Which paper?
  - whateveracct 6y ago
    "Linear Haskell" https://www.microsoft.com/en-us/research/uploads/prod/2017/12/linear-haskell-popl18-with-appendices.pdf https://www.microsoft.com/en-us/research/uploads/prod/2017/1... It's pretty long but it's pretty easy to just random-access read the examples for motivation. Both the Socket and the mutable array examples are great.

pgustafs 6y ago

From https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types : "The centrepiece of our design is to avoid code duplication. Crucially, the same types can be used in linear and non-linear contexts. For example, the linear-base library uses the same types as base. So libraries developed with linear-base will be compatible with libraries developed with base."

tuukkah 6y ago
Why can't base and linear-base be the same implementation too?
- nimih 6y ago
  The proposal discusses this briefly[1]. The idea seems to be that datatypes themselves remain identical (constructors being linear by default, even with -XNoLinearTypes), but functions are allowed to have more precise signatures. edit: I'm not knowledgeable enough about this stuff to know if the idea is to just refine the type signature but keep implementations identical, or whether implementations themselves need to change. [1] https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst#base https://github.com/ghc-proposals/ghc-proposals/blob/master/p...
  - tuukkah 6y ago
    Thanks for the pointer! Emphasis mine: "Because linear functions only strengthen the contract of unrestricted functions, a number of functions of base can get a more precise type. However, for pedagogical reasons, to prevent linear types from interfering with newcomers' understanding of the Prelude, this proposal does not modify base. Instead, we expect that users will publish new libraries on Hackage including more precisely typed base functions. One such library has already started here."
    - srtjstjsj 6y ago
      Prelude needs to change its name to Pedagogue. It's drifting ever farther from how people use the language to solve real problems.

pjmlp 6y ago

From the looks of it this isn't done anyway, just a stepping stone to get to the final destination. Just like value types, modules and concepts in other languages, sometime big bangs require incremental additions to the stable language instead of big bangs.

whateveracct 6y ago
This is the core argument of the detractors. They say they -XLinearTypes isn't Enough. They want a Big Bang. But it was already very hard work to get this incremental step. A Big Bang is even more work. And the detractors don't have a semblance of an alternative :/ but that hasn't stopped thousands of words of FUD from being spilled online.
- pjmlp 6y ago
  That is why we cannot have nice things, when those pushing their ideas don't have an hard skin to fight against those kind of issues. Though job. :\

creata 6y ago

* So is it appropriate to say that in linear types a callee says "I will use this exactly once", and in uniqueness types a callee says "I need exclusive access to this"? * Is there an obvious way to translate from one to the other? * Rust's type system sounds a lot closer to uniqueness types than linear or affine types. So why do so many people in this thread say that Rust has affine types?

akiselev 6y ago
> * Rust's type system sounds a lot closer to uniqueness types than linear or affine types. So why do so many people in this thread say that Rust has affine types?* Rust enforces exclusive access through ownership, which is orthogonal to linear/affine typing. Linear types must be used, affine types must be used at most once. Rust's compiler doesn't force code to use types like Futures or Result, at best it emits a warning, so a missing await or match statement can compile without doing what the code is intended to do. In a linear type system, you can mark Futures and Results so that the compiler throws an error when they're created but not consumed by an operation like awaiting or error handling.

nimih 6y ago

It seems inconsistent to claim both a) this proposal/implementation has bad ergonomics and doesn't solve real problems, and b) the library ecosystem will become irreparably fragmented as library authors rush to incorporate it or provide linear forks. Surely if enough people are expending the effort to bring -XLinearTypes to a non-trivial portion of the extant Haskell universe, it is by definition both useful and at least somewhat ergonomic?

whateveracct 6y ago
It is inconsistent. -XLinearTypes detractors have been making this paradoxical argument for months now. If it's useful, people will use it to build libraries. If it's not, it's all fine. The FUD from Haskellers depresses me. My consolation is I'll get to build useful shit with -XLinearTypes on GHC mainline now - things detractors told me weren't possible because they were too busy complaining about its imperfection.
- kreetx 6y ago
  The detractors are just a minority, right? Where do they criticize(?), reddit and the mailinglists have seemed pretty clean.
  - whateveracct 6y ago
    There have been multiple reddit posts full of long essay comments against the extension. Including a text post itself about it. They are clearly a minority though. But very vocal.
dllthomas 6y ago
It may be inaccurate but it's not inconsistent. Things can sound like a good idea, be embraced enthusiastically by people who haven't had a chance to work with them, and only later reveal serious ergonomic issues once people have a chance to use them in anger.

mrkeen 6y ago

> this extension doesn't do what they want It seems that you are the one wanting Linear types to be Uniqueness types instead. > no one bothered working through all the ugly details like exception handling in the context of a real application. Citation needed? > it's absolutely going to make the library ecosystem permanently worse, as lots of packages will get linearity annotations added > Lots of forks will arise without them, for the people who don't want the hassle How would the situation be different for Uniqueness types?

whateveracct 6y ago

> I really don't believe this is ever going to be better than existing techniques. The paper has examples of how it's better than existing method (such at the ST trick). Took me like an hour to read the entire thing months ago. Strong objections weren't ignored - they just weren't especially compelling. And when pressed for an alternative, nobody could come close to something of the rigor of what was merged. This entire comment is FUD and the fact that it's at the top of HN is such a PITA. Now I'm gonna have to hear even more people copy-paste argue against the extension instead of making real progress. This isn't going to make the library ecosystem worse. Please just edit that statement of "fact" out of your comment for all our sakes. That's all okay though. I'll go make some video games with type-safe manual memory management thanks to this extension :) that's the power of not complaining when things aren't as perfect as you can imagine them.

auggierose 6y ago
Which paper?
- whateveracct 6y ago
  "Linear Haskell" https://www.microsoft.com/en-us/research/uploads/prod/2017/12/linear-haskell-popl18-with-appendices.pdf https://www.microsoft.com/en-us/research/uploads/prod/2017/1... It's pretty long but it's pretty easy to just random-access read the examples for motivation. Both the Socket and the mutable array examples are great.