[HN Gopher] Linear types are merged in GHC
___________________________________________________________________
Linear types are merged in GHC
Author : todsacerdoti
Score : 82 points
Date : 2020-06-19 13:02 UTC (9 hours ago)
(HTM) web link (www.tweag.io)
(TXT) w3m dump (www.tweag.io)
| greg7mdp wrote:
| 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/.
| whateveracct wrote:
| -XLinearTypes down, -XDependentTypes to go :)
| gnulinux wrote:
| I hope they implement this in Agda as well.
| phibz wrote:
| Wow very cool stuff. I'm wondering if these ideas could be
| integrated into the rust type system.
| steveklabnik wrote:
| It's unclear if Rust can ever get linear types:
| https://gankra.github.io/blah/linear-rust/
| cosmic_quanta wrote:
| The proposal is described here:
|
| https://github.com/ghc-proposals/ghc-proposals/pull/111
| cryptonector wrote:
| Note that the focus here is to make it safe to have mutable data
| around, not to have manual memory management.
|
| Next up I hope: -
| https://www.youtube.com/watch?v=0jI-AlWEwYI
| https://github.com/lexi-lambda/ghc-proposals/blob/delimited-
| continuation-primops/proposals/0000-delimited-continuation-
| primops.md
| kccqzy wrote:
| I think for people who need absolute performance, manual memory
| management seems inevitable. No amount of GC tuning or hacks
| (such as the wonderful compact regions) would be satisfactory.
|
| This enables more kinds of programs to be written in Haskell,
| whereas your day-to-day typical server programs can just use GC
| as they currently do.
| whateveracct wrote:
| You can build safe abstractions for manual memory management in
| userspace with LinearTypes. In fact Haskell already has plenty
| of manual memory management modules in its stdlib - it's just
| that they live in IO.
|
| You can do the unsafePerformIO internally and expose a pure API
| made safe by some combination of LinearTypes and the ST trick.
| cryptonector wrote:
| To use linear types for everything will require new
| libraries, no?
| whateveracct wrote:
| Depends in your definition of "everything"
|
| If you want to manually manage all memory, then yes you'll
| have to not use `base` and any pure functional data
| structure.
|
| There's been a lot of "this feature is going to ruin the
| ecosystem" FUD but it's not much more that that imo
| xvilka wrote:
| There is `linear-base`[1] for this.
|
| [1] https://github.com/tweag/linear-base
| AnimalMuppet wrote:
| This has been bugging me for a while: Why are type names what
| they are? I get why sum types and product types are named what
| they are.
|
| But linear types? A value can be used only once? Cool. We call
| that "linearity"? Um, what? What's _linear_ about that?
| nitroll wrote:
| Because you can see their usage as a series of "points" linked
| to exactly one other point, that forms a "line", as opposed to
| other systems where you could have more of a graph or tree.
| tathougies wrote:
| They're linear because they can only be used once. If you draw
| out the set of 'references' to the object in a timeline it'll
| always be a line, whereas with a non-linear object, it could be
| any DAG.
| neel_k wrote:
| Vector spaces and linear maps between them form a model of the
| linearly-typed lambda calculus. That is, each type can be
| interpreted as a vector space, with each well-typed term
| representing a linear map between vector spaces.
|
| 1. The linear tensor product A [?] B gets interpreted as the
| tensor product of vector spaces.
|
| 2. The linear function space A [?] B gets interpreted as the
| vector space of linear functions between A and B.
|
| 3. The Cartesian product A x B gets interpreted as the direct
| product of vector spaces (i.e., the categorical product).
|
| 4. The sum type A + B gets interpreted as the direct sum of
| vector spaces (i.e., the categorical coproduct).
|
| 5. The exponential !A gets interpreted by the Fock space
| construction.
|
| This explains why the choice of name is sensible, but I don't
| actually know if that was the reason why Jean-Yves Girard named
| it so. If memory serves, he invented linear logic after
| thinking about Berry's notion of stable functions, but I don't
| know for sure when the vector space model was invented. (It's
| not in his 1987 paper, but it can't have appeared very long
| after that.)
| pickdenis wrote:
| This is the intuition I have: In algebra, a function or
| operator f(x) is generally thought of as linear if f(a * x + b
| * y) = a * f(x) + b * f(y). A linear function f(x) can only
| "use" x once in a multiplication. For example, the function
| f(x) = 1 is not linear (f(1+1) != f(1)+f(1)) as it only uses x
| zero times[0]. Similarly, the function f(x) = x * x is not
| linear. On the other hand, if x is only used once (after
| factoring), the function can be linear. Indeed, f(x) = k * x
| satisfies the linearity condition so long as k does not "use"
| x. Note that this is obviously not a sufficient condition, it's
| just an intuition.
|
| [0]: this requires you to discard the intuition that a linear
| function looks like a line when plotted.
| kinghajj wrote:
| https://en.wikipedia.org/wiki/Substructural_type_system#Line...
| empath75 wrote:
| That doesn't really answer his question.
|
| https://math.stackexchange.com/questions/2339147/why-is-
| it-c...
|
| Apparently there is some connection to vector spaces in the
| structure of linear logic which linear types are based on.
| bitdizzy wrote:
| The reasoning is sort of a technical analogy. Linear Logic was
| discovered by an analysis of the structure of Coherent Spaces,
| which are a model of Intuitionistic logic distilled from Scott
| domains. Jean-Yves Girard realized that function spaces A => B
| can be decomposed into two finer constructions as !A -o B where
| `A -o B` is a space of functions whose properties resemble
| linear functions between vector spaces and `!A` resembles the
| Fock space construction on a vector space.
|
| There are two ways this resemblance manifests.
|
| First off, the basic elements of a coherent space are called
| cliques which are analogous to vectors in a vector space. The
| functions constituting the coherent space A => B preserve
| directed unions of cliques but the linear functions of A -o B
| preserve _arbitrary_ unions of cliques which is strongly
| analogous to preserving arbitrary linear combinations of
| vectors.
|
| Second off is that you can build a symmetric monoidal category
| out of coherent spaces and vector spaces are the archetypal
| symmetric monoidal category. There are models of fragments of
| Linear Logic where the linear functions are literally
| polynomials of degree 1, but in its full generality it doesn't
| quite match exactly with linear algebra.
|
| Nonetheless the metaphor goes deep and you can even capture
| notions of differentiability in extensions to the logic.
|
| For a technical exposition you can read this paper by a guy
| who's applying this sort of stuff to machine learning:
| https://arxiv.org/abs/1407.2650 I apologize if this is all too
| obscure to justify the name. Linear Logic's applications to
| programming were sort of secondary to its proof theoretic
| novelty at its inception.
| centimeter wrote:
| Awesome! Very impressive work! I can't wait until the kinks are
| ironed out and we start seeing resource management APIs using
| this.
|
| It surprised me how useful Rust's affine types were for resource
| management APIs, so I'm sure we'll see some cool applications in
| Haskell.
___________________________________________________________________
(page generated 2020-06-19 23:00 UTC)