9 ms·

Haskell GHC 9.0.1-alpha

124 points by harporoeder 6y ago

gautamcgoel 6y ago
Can someone explain what this means, practically speaking? I know Haskell fairly well, but am not familiar with linear types. These are types that can be used only once, right?
- adamnemecek 6y ago
  Yes, it's useful for reasoning about resources (file handles, sockets, memory buffers) etc.
- dleslie 6y ago
  They must be used once and exactly once, no more or less. I liked this paper: http://www.cs.utexas.edu/~hunt/research/hash-cons/hash-cons-papers/BakerLinearLisp.pdf http://www.cs.utexas.edu/~hunt/research/hash-cons/hash-cons-... And previous discussion: https://news.ycombinator.com/item?id=20369522 https://news.ycombinator.com/item?id=20369522
- T-R 6y ago
  My understanding is that the current implementation is only groundwork for possible future performance benefits, since there are no changes to the runtime system or garbage collector, and that their current intended use is mostly for allowing library authors to encode safe session/resource handling in the type system. So, new libraries can make it a type error to fail to properly close a connection or release a shared resource. Simon Peyton Jones talk: https://www.youtube.com/watch?v=t0mhvd3-60Y https://www.youtube.com/watch?v=t0mhvd3-60Y
  - whateveracct 6y ago
    You can write safe memory management libraries in userspace with the existing extension. That can help reduce GC pressure by moving data off-heap and allow for safer & more efficient FFI bindings. As someone who has been exploring doing gamedev in Haskell, that all is very exciting and the use-cases are constantly obvious to me. It is entirely up to userspace to leverage this new feature. It doesn't do anything on its own outside of the type-checker. And to use it, your library will probably have to do some unsafe coercion under the hood (just like ST uses unsafePerformIO under the hood to do pure mutability.)
    - dllthomas 6y ago
      Right, my understanding is that in a sense it doesn't "enable new performance", because operationally speaking it's all stuff you could do anyway. What it does is move a lot of potential approaches from "absurdly unsafe" to "perfectly fine", so whatever your threshold for safety it's likely to move some speed improvements over the line if you care much about speed.
flubert 6y ago
Any pointers to a comparison between Clean's uniqueness typing and GHC's linear types? And is Rust the motivating factor behind linear types cropping up lately? I see Idris is now getting them as well.
- necubi 6y ago
  Rust has affine types (can be used no more than once), but not linear types (must be used exactly once). Linear types would be a nice feature for rust, and there's been some discussion about how to add them, but as far as I know there hasn't been any real progress there. Affine types in Rust are anything with move semantics; for example you can create a method that consumes itself like this: impl A { fn use(&mut self) { // takes a mutable reference to self, so it // can be used again later } fn consume(self) { // moves self into this function, which means // it cannot be used again } }
  - throwaway17_17 6y ago
    I don’t understand how a usage pattern where some variable (representing a semantic object) is said to have an affine type but it can be used more than once. Can you explain how such a type is not just a regular non-substructural type?
    - necubi 6y ago
      Sorry, that wasn't very clear. `&mut self` in the first method ("use") is an example of a non-affine type, `self` in the "consume" method is an affine type which cannot be re-used.
  - atombender 6y ago
    What's the importance of having to use a value? I.e. isn't this the same as discarding it? Or is related to things like resource finalizers — i.e. once you open a file, you have to "consume" it in order for it to be closed?
    - 6y ago
smabie 6y ago
I'm not super well versed on this stuff, but aren't affine types strictly superior? Though I suppose linear types might be better for tracking system resources?
- throwaway17_17 6y ago
  I am fairly well read on substructural type theories, if you could explain what you mean by ‘strictly superior’ then maybe I could formulate some points of interest, but as the question stands, I don’t think there is any justification for claiming that affine types are better than linear types.
  - smabie 6y ago
    Okay maybe compare and contrast them? In what cases are affine types better and in what cases are they worse (than linear types)?
    - lpage 6y ago
      As GP alluded to, there’s not really a proper ordering. If you’re talking ease-of-reasoning from a formal methods standpoint, linear types (or ordered types for that matter) are “superior” to affine types. By extension, when compiling to machine code for real-world computing architectures, linear types have advantages. They lend themselves to aggressive compiler optimization, instruction and data cache-friendly access patterns, and automatic parallelization and vectorization opportunities. All of those things boil down to proving equivalence, so the ability to mathematically reason about code has both testing and performance implications. Affine types are less foreign to most developers. The safe fragment of Rust’s ownership model is an example of an affine type system...and that’s already a bit of a lift for folks new to the borrow checker. Affine types are harder to reason about than linear types, but still much easier to reason about than the Normal [1] (in the proper noun sense) types used in most PLs. [1] https://en.wikipedia.org/wiki/Substructural_type_system https://en.wikipedia.org/wiki/Substructural_type_system
- deleted 6y ago
  [deleted]
chowells 6y ago
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...
platz 6y ago
FYI, because I know it will be brought up; GHC models linearity differently than Rust, so you can't compare the two against each other, even though you think you would be able to do that. Rust puts linearity on the types, GHC puts linearity on the arrows. https://imgur.com/s0Mxhcr https://imgur.com/s0Mxhcr https://skillsmatter.com/skillscasts/11067-keynote-linear-haskell-practical-linearity-in-a-higher-order-polymorphic-language https://skillsmatter.com/skillscasts/11067-keynote-linear-ha...
- Tehnix 6y ago
  Rust doesn’t have linear types, but rather affine types, and present quite different designs.
- hardwaresofton 6y ago
  Talks that might be informative for the curious: https://www.youtube.com/watch?v=t0mhvd3-60Y https://www.youtube.com/watch?v=t0mhvd3-60Y https://www.youtube.com/watch?v=uxv62QQajx8 https://www.youtube.com/watch?v=uxv62QQajx8
- srtjstjsj 6y ago
  Your first link says that Rust puts linearity on the kinds (types of types, not types of data).
banuguler 6y ago
Want to work on Haskell all day? Co–Star is hiring. Downloaded every 4 seconds, kids compare the app to their therapist, best friend, and a board meeting with the universe. → https://www.costarastrology.com/jobs https://www.costarastrology.com/jobs or email tim (at-squiggle) costarastrology.com
- bojo 6y ago
  It’s not that what you do is bad, just the wrong place and time. This is a thread about GHC 9.x and linear types.
  - AnimalMuppet 6y ago
    Eh, I could classify getting kids into astrology as "bad".
danidiaz 6y ago
Besides potentially enabling new types of APIs, I simply like that this extension lets you write more precise type signatures. A function with type [a] %1 -> [a] can do less things that a function with type [a] -> [a].
flumpcakes 6y ago
Are there are books/video lectures that explain linear types how they are useful in a programming language? How do people that don't have PhDs bridge the gap in their knowledge from what's commonly taught/used (OOP and it's design patterns) to thinking in terms of monads/monoids/functors/etc. ?
- pyrale 6y ago
  SPJ usually makes great introductions about new things being introduced to GHC. Here's one about linear types: https://www.youtube.com/watch?v=t0mhvd3-60Y https://www.youtube.com/watch?v=t0mhvd3-60Y > How do people that don't have PhDs bridge the gap in their knowledge from what's commonly taught/used (OOP and it's design patterns) to thinking in terms of monads/monoids/functors/etc. In my own experience, you just practice, and munch new knowledge bits by bits. The crucial point here is that you don't need to know _all_ of haskell to be productive using it. So you learn the basics, start using monads without understanding the Monad abstraction (it's really not something you need to understand to use), and after a while it just clicks. And once you're confortable with this basic knowledge, you learn new things when you need them. As a result, I (and many other paid haskellers) have a job writing haskell without having a PhD, without learning category theory, or without a deep math bagage.
- hans1729 6y ago
  >How do people that don't have PhDs bridge the gap in their knowledge from what's commonly taught/used (OOP and it's design patterns) to thinking in terms of monads/monoids/functors/etc. ? I can just speak for myself. Started programming via vocational training (apprenticeship for the title 'computer science expert' in germany) about 4 years ago. Learned programming with python, which I loved for the productivity it gave me, the whole superpower yadiya. Was assigned some webrelated tasks, so I got in touch with javascript. My style in these languages was actually 'functional' without me knowing about functional programming - but only to some extent. Mutability, nonstatic typing etc. So, wanting to become a better programmer, I googled things like "advanced python", which yielded things like decorators, generators and metaclasses. In some video about map, filter and reduce something in me clicked - I didn't want to hide attributes and state in classes and objects anymore. It's not modular, it's not atomic, it's not beautiful. I came across Rich Hickeys talks [1] and immediately saw that I'm ...home. The paradigms just click with me, I can't imagine falling back to impurity and oop (unless it can't be avoided for whatever reasons). (I still don't write clojure though, for now I'm still enjoying playing around in python and haskell where I can (you may substitute python with js)) And, honestly - if you have the curiosity to learn Haskell, do you really need a phd? I've taught myself bits of maths in the last four years (higher mathematics - number theory (not tech related, just curiosity), graph theory, category theory etc), just driven by curiosity. That being said: If you'd ask me about these topics on the street, I wouldn't claim to be a mathematician, far from it. I just satisfied my curiosity. I want to understand. Not some math or haskell in specific, but life, logic, control flow, systems theory... Having this urge, diving deeper into mathematical concepts once you need them doesn't feel like a burden. I don't even have my A-levels, so I'm probably as far from a phd as you'll find on HN, but that wouldn't stop me from exploring, from learning, from progress. Sorry if that was too personal and too much text, I just felt like I'm in the rare position to be able to answer something in depth on HN :-) [1] https://github.com/tallesl/Rich-Hickey-fanclub#talks https://github.com/tallesl/Rich-Hickey-fanclub#talks Some more links that I used: Functor, aplicative, and monad: https://typeslogicscats.gitlab.io/posts/functor-applicative-monad.html https://typeslogicscats.gitlab.io/posts/functor-applicative-... Category theory for programmers: https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbm...

124 points by harporoeder 6y ago

Can someone explain what this means, practically speaking? I know Haskell fairly well, but am not familiar with linear types. These are types that can be used only once, right?

adamnemecek 6y ago
Yes, it's useful for reasoning about resources (file handles, sockets, memory buffers) etc.
dleslie 6y ago
They must be used once and exactly once, no more or less. I liked this paper: http://www.cs.utexas.edu/~hunt/research/hash-cons/hash-cons-papers/BakerLinearLisp.pdf http://www.cs.utexas.edu/~hunt/research/hash-cons/hash-cons-... And previous discussion: https://news.ycombinator.com/item?id=20369522 https://news.ycombinator.com/item?id=20369522
T-R 6y ago
My understanding is that the current implementation is only groundwork for possible future performance benefits, since there are no changes to the runtime system or garbage collector, and that their current intended use is mostly for allowing library authors to encode safe session/resource handling in the type system. So, new libraries can make it a type error to fail to properly close a connection or release a shared resource. Simon Peyton Jones talk: https://www.youtube.com/watch?v=t0mhvd3-60Y https://www.youtube.com/watch?v=t0mhvd3-60Y
- whateveracct 6y ago
  You can write safe memory management libraries in userspace with the existing extension. That can help reduce GC pressure by moving data off-heap and allow for safer & more efficient FFI bindings. As someone who has been exploring doing gamedev in Haskell, that all is very exciting and the use-cases are constantly obvious to me. It is entirely up to userspace to leverage this new feature. It doesn't do anything on its own outside of the type-checker. And to use it, your library will probably have to do some unsafe coercion under the hood (just like ST uses unsafePerformIO under the hood to do pure mutability.)
  - dllthomas 6y ago
    Right, my understanding is that in a sense it doesn't "enable new performance", because operationally speaking it's all stuff you could do anyway. What it does is move a lot of potential approaches from "absurdly unsafe" to "perfectly fine", so whatever your threshold for safety it's likely to move some speed improvements over the line if you care much about speed.

flubert 6y ago

Any pointers to a comparison between Clean's uniqueness typing and GHC's linear types? And is Rust the motivating factor behind linear types cropping up lately? I see Idris is now getting them as well.

necubi 6y ago
Rust has affine types (can be used no more than once), but not linear types (must be used exactly once). Linear types would be a nice feature for rust, and there's been some discussion about how to add them, but as far as I know there hasn't been any real progress there. Affine types in Rust are anything with move semantics; for example you can create a method that consumes itself like this: impl A { fn use(&mut self) { // takes a mutable reference to self, so it // can be used again later } fn consume(self) { // moves self into this function, which means // it cannot be used again } }
- throwaway17_17 6y ago
  I don’t understand how a usage pattern where some variable (representing a semantic object) is said to have an affine type but it can be used more than once. Can you explain how such a type is not just a regular non-substructural type?
  - necubi 6y ago
    Sorry, that wasn't very clear. `&mut self` in the first method ("use") is an example of a non-affine type, `self` in the "consume" method is an affine type which cannot be re-used.
- atombender 6y ago
  What's the importance of having to use a value? I.e. isn't this the same as discarding it? Or is related to things like resource finalizers — i.e. once you open a file, you have to "consume" it in order for it to be closed?
  - 6y ago

smabie 6y ago

I'm not super well versed on this stuff, but aren't affine types strictly superior? Though I suppose linear types might be better for tracking system resources?

throwaway17_17 6y ago
I am fairly well read on substructural type theories, if you could explain what you mean by ‘strictly superior’ then maybe I could formulate some points of interest, but as the question stands, I don’t think there is any justification for claiming that affine types are better than linear types.
- smabie 6y ago
  Okay maybe compare and contrast them? In what cases are affine types better and in what cases are they worse (than linear types)?
  - lpage 6y ago
    As GP alluded to, there’s not really a proper ordering. If you’re talking ease-of-reasoning from a formal methods standpoint, linear types (or ordered types for that matter) are “superior” to affine types. By extension, when compiling to machine code for real-world computing architectures, linear types have advantages. They lend themselves to aggressive compiler optimization, instruction and data cache-friendly access patterns, and automatic parallelization and vectorization opportunities. All of those things boil down to proving equivalence, so the ability to mathematically reason about code has both testing and performance implications. Affine types are less foreign to most developers. The safe fragment of Rust’s ownership model is an example of an affine type system...and that’s already a bit of a lift for folks new to the borrow checker. Affine types are harder to reason about than linear types, but still much easier to reason about than the Normal [1] (in the proper noun sense) types used in most PLs. [1] https://en.wikipedia.org/wiki/Substructural_type_system https://en.wikipedia.org/wiki/Substructural_type_system
deleted 6y ago
[deleted]

chowells 6y ago

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

platz 6y ago

FYI, because I know it will be brought up; GHC models linearity differently than Rust, so you can't compare the two against each other, even though you think you would be able to do that. Rust puts linearity on the types, GHC puts linearity on the arrows. https://imgur.com/s0Mxhcr https://imgur.com/s0Mxhcr https://skillsmatter.com/skillscasts/11067-keynote-linear-haskell-practical-linearity-in-a-higher-order-polymorphic-language https://skillsmatter.com/skillscasts/11067-keynote-linear-ha...

Tehnix 6y ago
Rust doesn’t have linear types, but rather affine types, and present quite different designs.
hardwaresofton 6y ago
Talks that might be informative for the curious: https://www.youtube.com/watch?v=t0mhvd3-60Y https://www.youtube.com/watch?v=t0mhvd3-60Y https://www.youtube.com/watch?v=uxv62QQajx8 https://www.youtube.com/watch?v=uxv62QQajx8
srtjstjsj 6y ago
Your first link says that Rust puts linearity on the kinds (types of types, not types of data).

banuguler 6y ago

Want to work on Haskell all day? Co–Star is hiring. Downloaded every 4 seconds, kids compare the app to their therapist, best friend, and a board meeting with the universe. → https://www.costarastrology.com/jobs https://www.costarastrology.com/jobs or email tim (at-squiggle) costarastrology.com

bojo 6y ago
It’s not that what you do is bad, just the wrong place and time. This is a thread about GHC 9.x and linear types.
- AnimalMuppet 6y ago
  Eh, I could classify getting kids into astrology as "bad".

danidiaz 6y ago

Besides potentially enabling new types of APIs, I simply like that this extension lets you write more precise type signatures. A function with type [a] %1 -> [a] can do less things that a function with type [a] -> [a].

flumpcakes 6y ago

Are there are books/video lectures that explain linear types how they are useful in a programming language? How do people that don't have PhDs bridge the gap in their knowledge from what's commonly taught/used (OOP and it's design patterns) to thinking in terms of monads/monoids/functors/etc. ?

pyrale 6y ago
SPJ usually makes great introductions about new things being introduced to GHC. Here's one about linear types: https://www.youtube.com/watch?v=t0mhvd3-60Y https://www.youtube.com/watch?v=t0mhvd3-60Y > How do people that don't have PhDs bridge the gap in their knowledge from what's commonly taught/used (OOP and it's design patterns) to thinking in terms of monads/monoids/functors/etc. In my own experience, you just practice, and munch new knowledge bits by bits. The crucial point here is that you don't need to know _all_ of haskell to be productive using it. So you learn the basics, start using monads without understanding the Monad abstraction (it's really not something you need to understand to use), and after a while it just clicks. And once you're confortable with this basic knowledge, you learn new things when you need them. As a result, I (and many other paid haskellers) have a job writing haskell without having a PhD, without learning category theory, or without a deep math bagage.
hans1729 6y ago
>How do people that don't have PhDs bridge the gap in their knowledge from what's commonly taught/used (OOP and it's design patterns) to thinking in terms of monads/monoids/functors/etc. ? I can just speak for myself. Started programming via vocational training (apprenticeship for the title 'computer science expert' in germany) about 4 years ago. Learned programming with python, which I loved for the productivity it gave me, the whole superpower yadiya. Was assigned some webrelated tasks, so I got in touch with javascript. My style in these languages was actually 'functional' without me knowing about functional programming - but only to some extent. Mutability, nonstatic typing etc. So, wanting to become a better programmer, I googled things like "advanced python", which yielded things like decorators, generators and metaclasses. In some video about map, filter and reduce something in me clicked - I didn't want to hide attributes and state in classes and objects anymore. It's not modular, it's not atomic, it's not beautiful. I came across Rich Hickeys talks [1] and immediately saw that I'm ...home. The paradigms just click with me, I can't imagine falling back to impurity and oop (unless it can't be avoided for whatever reasons). (I still don't write clojure though, for now I'm still enjoying playing around in python and haskell where I can (you may substitute python with js)) And, honestly - if you have the curiosity to learn Haskell, do you really need a phd? I've taught myself bits of maths in the last four years (higher mathematics - number theory (not tech related, just curiosity), graph theory, category theory etc), just driven by curiosity. That being said: If you'd ask me about these topics on the street, I wouldn't claim to be a mathematician, far from it. I just satisfied my curiosity. I want to understand. Not some math or haskell in specific, but life, logic, control flow, systems theory... Having this urge, diving deeper into mathematical concepts once you need them doesn't feel like a burden. I don't even have my A-levels, so I'm probably as far from a phd as you'll find on HN, but that wouldn't stop me from exploring, from learning, from progress. Sorry if that was too personal and too much text, I just felt like I'm in the rare position to be able to answer something in depth on HN :-) [1] https://github.com/tallesl/Rich-Hickey-fanclub#talks https://github.com/tallesl/Rich-Hickey-fanclub#talks Some more links that I used: Functor, aplicative, and monad: https://typeslogicscats.gitlab.io/posts/functor-applicative-monad.html https://typeslogicscats.gitlab.io/posts/functor-applicative-... Category theory for programmers: https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbm...