[HN Gopher] GHC 9.0, supporting linear types
___________________________________________________________________
GHC 9.0, supporting linear types
Author : cosmic_quanta
Score : 174 points
Date : 2020-12-30 15:58 UTC (7 hours ago)
(HTM) web link (discourse.haskell.org)
(TXT) w3m dump (discourse.haskell.org)
| canjobear wrote:
| I would love to read something about the connection between
| linear types, linear logic, and linear algebra. This seems like a
| deep and important connection, considering that modern ML is
| looking more and more like applied linear algebra.
| layoutIfNeeded wrote:
| The category of finite dimensional vector spaces over finite
| fields is a model of linear logic.
| http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/30/slides/steve.pdf
| gautamcgoel wrote:
| Can someone please explain what you can do with linear types? I
| understand what they are (types which the compiler guarantees are
| used exactly once), but I don't understand why they're important.
| cultus wrote:
| To add to other user's comments, linear types are useful for
| reasoning exactly about (some) imperative constructs, which is
| really, really hard to do with standard type systems. That's
| why reliably guaranteeing e.g. why it's still difficult to
| ensure safe and timely disposal of database connections in
| Haskell (maybe not now) or Scala, despite their powerful type
| systems.
|
| There's many other such modal type systems/logics used for
| other special purposes like temporal logic.
| WJW wrote:
| The way I usually think about it is that it's like the Rust
| borrowing system but more powerful. If the compiler can be sure
| a type will be used exactly once, you could for example do
| automatic memory management by freeing the value directly after
| it is used. You can also fix a range of multithreading bugs
| with it, as other people have mentioned.
|
| Finally, it allows you to express more invariants about your
| data through the type system, hopefully reducing bug counts. As
| an example, soneone could "implement" a sorting function as
| `sort xs = []`. This has the correct type signature, but is not
| a correct implementation of sorting. With linear types you
| could express that the output has to access the values of the
| input. (Of course what we'd actually want is to express other
| invariants for sorting as well, but full dependent types are
| still some ways off)
| danidiaz wrote:
| According to the proposal, affine types and linear types "are
| not equi-expressive": https://github.com/ghc-proposals/ghc-
| proposals/blob/master/p...
| carterschonwald wrote:
| Yup!
|
| There's also quite a design space still to be explored for
| these ideas. Even / especially for languages like Haskell.
| marcosdumay wrote:
| All the use cases I've seen are about optimization.
|
| You can avoid a lot of copying and memory management if you
| know the value will be used a single time, and then generate
| another value, that will be used a single time again. It has a
| very large potential impact, mostly on IO.
| adamnemecek wrote:
| It's not just optimization but also correctness. You really
| don't want do a bit wise copy of say a file descriptor.
| mhh__ wrote:
| Haskell as a language is effectively an experiment to see how
| much unsafe stuff can be done in a compartmentalized and "safe"
| manner (see SPJ's "Haskell is useless"), so Linear Types are
| another road to go down to achieve that goal.
| tremon wrote:
| The following blog post is referenced in the proposal:
| https://www.tweag.io/blog/2017-08-03-linear-typestates/ . This
| is maybe a different aspect than what others have been trying
| to explain, but I found the socket-based example enlightening.
|
| _Type states_ allow the state of the socket (unbound, bound,
| listening, closed) to be expressed as a part of the type (a
| type annotation, if you will) so the compiler can verify that
| you 're not reusing a closed socket, or try to send data over
| an unbound socket.
|
| _Linear types_ then, allow to express in code how a type
| (annotation) changes over time (e.g., "bind() takes an unbound
| socket and returns it an a bound state") so the compiler can
| statically check that it's in a valid state for every
| operation.
| dllthomas wrote:
| The two most commonly referenced uses are safe mutation and
| better resource management.
|
| Safe mutation because when I have the only reference to a
| thing, the rest of the system shouldn't care whether I change
| it in place or make a new one.
|
| Better resource management because you can be sure opened files
| are closed exactly once and that nothing tries to use a file
| after close, even where a bracket pattern doesn't fit (or fits
| much more loosely).
|
| In both cases, you're not doing anything you couldn't _do_
| before, but it lets you do it safely. People speak of
| performance because (especially in Haskell) mutating without
| being confident nothing else can see is sufficiently full of
| footguns that the community happily (... and rightly, IMO) pays
| small performance penalties for security against them. This
| lets us remove those performance penalties in more cases.
|
| There's some room for the _compiler_ to notice that something
| is only referenced in one place and safely convert some things
| to mutation; again this doesn 't strictly need linear types,
| but linear types may let us do that reasoning locally instead
| of it requiring whole program analysis.
| tsuraan wrote:
| A specific safety article was written up by tweag.io, who wrote
| a pretty slick set of java bindings. Managing resources between
| two garbage collectors (ghc and jvm) is error-prone, so they
| used linear types to help prevent a bunch of the things a
| person can easily mess up. Their article is pretty good:
| https://www.tweag.io/blog/2020-02-06-safe-inline-java/
| whateveracct wrote:
| A lot of good stuff in this release! Both LinearTypes and
| QualifiedDo (which is useful for LinearTypes but also other uses)
|
| The ghc-bignum change is kind of boring, but it does help a lot
| with the long-standing problematic dependency on gmp.
|
| Not to mention the stage being set for QuickLook impredicativity.
| That's something that I've been wishing we've had for a long time
| now.
|
| Haskell remains at the bleeding edge of general-purpose
| programming - more than ever with each release.
| bjt wrote:
| The GMP change is the most exciting one for me!
|
| Years ago when I was really trying to get into Haskell, I
| wanted its binaries to be as portable as those from Go. I was
| so sad to see that this _one_ library made that impossible.
| garmaine wrote:
| What's the issue? GMP is pretty portable, no?
| whateveracct wrote:
| it's more about its license
| endgame wrote:
| GMP is LGPL, so if you distribute a binary to someone it
| has to be possible for the recipient to re-link it with an
| alternate libgmp (either via dynamic linking, or by
| providing .o files and a script)
| robocat wrote:
| My understanding from a quick google:
|
| The issue is that if you write a Haskell program, and you
| want to deploy it as a single executable, then GMP is
| included (statically linked), so the LGPL applies to the
| executable.
|
| The two obvious ways to meet the LGPL license restrictions
| are:
|
| * license your code in a way that is LGPL compatible (e.g.
| open source your code using GPL)
|
| * you could provide the app in a relinkable form (ie a big
| .o file) as per section 6.a
|
| Essentially there is no tidy way to distribute a closed
| source Haskell executable without removing the GMP library,
| which was the sole remaining LGPL dependency. It was not
| trivial to remove the dependency because of the library's
| quality (amongst other reasons).
|
| (Edited for clarity.)
| garmaine wrote:
| I don't understand what this has to do with portability.
| cercatrova wrote:
| People don't want to share the freedoms they got with
| their users. That's it. There's no reason commercial
| software can't be under GPL style licenses.
| whateveracct wrote:
| If I'm releasing an indie video game in Haskell, I'm not
| going to GPL it..
| [deleted]
| pwm wrote:
| Just the other day i was doing something with LogicT where
| QualifiedDo would have been super handy.
| tluyben2 wrote:
| That went pretty fast, on a ghc timescale. Well done! Promising
| for the future.
| whateveracct wrote:
| ~3 years since the Linear Haskell paper all told
|
| This included a pretty rigorous community review. The extension
| did get some pushback & serious debate, and I honestly think
| the entire process was handled wonderfully. It speaks well of
| GHC's community culture (speaking as a sideline observer.)
| chrisaycock wrote:
| I first became fascinated by linear [1] and uniqueness [2] types
| with Clean [3], a purely functional language that handles state
| and IO without monads.
|
| This Haskell extension uses linear types for resource safety and
| scoped effects [4]. For example, linear types can prevent use-
| after-free errors. Also, linear-typed arrays can perform in-place
| updates if there are no external pointers to the data.
|
| Similar to linear types is the _affine_ type, where a value is
| used at-most once. Rust 's borrow checker is based on this
| notion, so that values are "moved" rather than "copied".
|
| [1] https://en.wikipedia.org/wiki/Uniqueness_type
|
| [2] https://en.wikipedia.org/wiki/Substructural_type_system
|
| [3] https://clean.cs.ru.nl/Clean
|
| [4] https://arxiv.org/abs/1710.09756
| dmix wrote:
| Man, I wish I understood all of this stuff. I have a general
| enough notion from digging into Haskell and reading into types
| (including dependent types). I see the value of uniqueness just
| from using Typescript and having dumb clashes of type variable
| names, which may be unrelated.
|
| But like a lot of Haskell much of this still goes over my head.
|
| I'm so conflicted and my intuition is to leave this to the CS
| university types and focus on IRL productivity in my own field.
| But I want to invest more time into FP in the future.
|
| I'm also technically a "frontend developer" professionally :p
| yodsanklai wrote:
| > But like a lot of Haskell much of this still goes over my
| head.
|
| It's not that hard, but it's easier to get one concept at a
| time. I'm less familiar with Haskell, but languages like
| Scheme/OCaml are routinely used to teach programming to
| beginners.
|
| Also there's no need to see a dichotomy between "IRL
| productivity" and "CS/FP". Even if you don't use Haskell
| directly, ideas from FP make their way to mainstream
| languages, either as constructs, or libraries, or simply
| programming style.
|
| Overall, the more programming paradigms you know, the easier
| it gets to learn new languages.
| roflc0ptic wrote:
| I have a degree in geography, and learned to do web
| development largely on the job. It took me about 5 years
| before I ventured into learning functional programming, and
| in retrospect, I feel I could've been 5 years farther ahead
| today. It makes you a better programmer, and while it might
| only make you marginally better at the tasks you currently
| do, it will open up a wide expanse of other possibilities you
| didn't think yourself capable of.
| whateveracct wrote:
| > it will open up a wide expanse of other possibilities you
| didn't think yourself capable of
|
| Haskell has a tendency to make every problem seem exactly
| the same :)
| vsskanth wrote:
| How can linear types be used for something like doing a bunch of
| calculations on a DataFrame of unknown size ? ex: filter rows
| based on certain conditions, compute some averages, and then plot
| certain columns etc.
|
| Its hard to find real world use examples and learn about linear
| types when I search online. If anyone has links, that would help.
| jose_zap wrote:
| Some real world examples with links:
|
| - A safe streaming library where effects are guaranteed to only
| be performed once: https://www.tweag.io/blog/2018-06-21-linear-
| streams/
|
| - Efficient zero-copy network communication:
| https://www.tweag.io/blog/2017-08-24-linear-types-packed-dat...
|
| - Safe manual memory management and prompt resource release:
| https://www.tweag.io/blog/2020-02-06-safe-inline-java/
|
| - Explicit API design to guide developers on what function to
| call next when implementing a protocol like TCP:
| https://www.tweag.io/blog/2017-08-03-linear-typestates/
|
| - Add correctness proofs to already existing algorithm
| implementations like merge sort:
| https://www.tweag.io/blog/2018-03-08-linear-sort/
| vsskanth wrote:
| Thank you!
| whateveracct wrote:
| They'd mostly be used for creating a pure API around any
| mutability under the hood
|
| But we already had ST for that, so the real advantage of LTs
| over ST is you can type-safely "freeze" and "thaw" your mutable
| structure without copying.
|
| The mutable array example in the Linear Haskell paper is a
| simple comparison to what you're asking for.
| Kbsm wrote:
| Learn more about the new linear types extension in GHC here:
| https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91
| juancampa wrote:
| > Safe zero-copy data (de)serialization, a notoriously difficult
| endeavour that is in fact so error prone without linear types
| that most production systems today typically avoid it.
|
| I wonder how this compares to Rust's borrowing approach which can
| be used for the same goal. I don't know enough about Haskell to
| understand Linear types. Perhaps someone more knowledgeable can
| comment.
| platz wrote:
| GHC models linearity differently. Rust puts linearity on the
| types, GHC puts linearity on the arrows.
| https://i.imgur.com/s0Mxhcr_d.webp?maxwidth=640&shape=thumb&...
| ric2b wrote:
| What is "the arrow" in this context?
| tremon wrote:
| "the arrow" is an expression of a function operation, or
| rather, how a function transforms its arguments. In
| Haskell, the following signature: func :: A
| -> B
|
| declares a function _func_ that takes one argument of type
| _A_ and returns a value of type _B_.
|
| I'm guessing a bit, I feel this goes over my head, but
| here's my layman's interpretation:
|
| In Rust, in order to declare a linear type, you must do so
| when initializing the variable: let x =
| vec![1, 2, 3];
|
| Now _x_ is declared as move-only, so that the vector cannot
| be duplicated by assigning it to a second variable; after
| assignment, accessing _x_ will result in a compiler error.
|
| In Haskell, you declare a function func ::
| A %1 -> B
|
| to indicate that after this function call, accessing _A_
| should result in a compiler error.
| paavohtl wrote:
| I don't find this answer satisfactory, because you also
| need to specify in Rust whether or not a function moves
| its argument(s). // This moves the
| argument fn func(a: A) -> B { .. } func(x);
| // x is not accessible after this line //
| This borrows the argument, and therefore won't move it
| fn func(a: &A) -> B { .. } func(&x); // x remains
| accessible after this line
| the_duke wrote:
| Do you know the reasoning why?
|
| Not tying the linearity to the type seems quite a bit more
| confusing and error prone to me.
|
| If a type can be used in different ways, I'd rather have two
| different types.
| platz wrote:
| The core logic theory behind linearity on the arrows is
| provably sound and more well understood theoretically, and
| it fits better with Haskell's existing semantics.
|
| The rust way is probably more practically useful from a
| programmer's perspective, but it isn't as easily understood
| to be sound from a type theory perspective.
| the_duke wrote:
| So to be clear:
|
| Let's say a function returns a linear value. If I then
| feed this value into a function that does not specify
| linearity, all linearity is lost and the function can
| treat it as a regular non-linear type?
|
| If yes that would seem to require extreme discipline by
| the programmer to remain useful.
| mauricioc wrote:
| There is no such thing as a "linear value" per se, since
| linearity is on the arrow. But speaking of linear values
| makes sense when there's an ambient monad, and all of the
| restrictions you expect are enforced; see Section 2.7
| (and the last paragraph of Section 6.1) of
| https://arxiv.org/pdf/1710.09756.pdf for details.
| whateveracct wrote:
| No that's not the case. I am fairly sure that situation
| you describe results in a type error. The extension does
| in fact enforce linearity, and does not have such a
| trivial & universal escape hatch afaiu.
|
| Feel free to give GHC 9.0 a try with a minimal example of
| your scenario!
| ghostwriter wrote:
| There is a recent article about these scenarios, you may
| find it helpful -
| https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91
| Raphael_Amiard wrote:
| Affine types, which Rust more or less implements with its
| ownership system are very close to linear types, see
| https://en.m.wikipedia.org/wiki/Substructural_type_system#Af...
| sa1 wrote:
| Rust has affine types (values can be used upto 1 time), which
| are similar to linear types(values can be used exactly once).
| Affine types are slightly more general, but offer less
| guarantees about your program. To add back some guarantees,
| Rust also has lifetime analysis.
|
| So for most common use-cases, you will be able to use Rust and
| Haskell for similar guarantees. But I'm also eager to see what
| unique use-cases will be enabled by each of them.
___________________________________________________________________
(page generated 2020-12-30 23:00 UTC)