28 ms·
GHC 9.0, supporting linear types
- juancampa 6y ago> 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.
- Raphael_Amiard 6y agoAffine 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#Affine_type_systems https://en.m.wikipedia.org/wiki/Substructural_type_system#Af...
- sa1 6y agoRust 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.
- platz 6y agoGHC 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&fidelity=medium https://i.imgur.com/s0Mxhcr_d.webp?maxwidth=640&shape=thumb&...
- the_duke 6y agoDo 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 6y agoThe 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 6y agoSo 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.
- whateveracct 6y agoNo 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 6y agoThere is a recent article about these scenarios, you may find it helpful - https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91 https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91
- mauricioc 6y agoThere 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 https://arxiv.org/pdf/1710.09756.pdf for details.
- ric2b 6y agoWhat is "the arrow" in this context?
- tremon 6y ago"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 6y agoI 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
- Ericson2314 6y agoFrom the perspective of Rust, Linear Haskell is going to seem quite weird, and I say that as Haskeller wishing that language extension was more like Rust. I'm not really sure how to explain it, but basically only functions that are themselves linear can have linear parameters, It's vaguely like "`Fn(A) -> B` only if `A: Copy`", and `FnOnce(A) -> B` only if `A: !Copy`, except there is no `Copy` or `!Copy` and the only say to determine it is `Fn` vs `FnOnce`.
- KirillPanov 6y agoFor the most part they accomplish the same goals, but in very different ways. Linear types have a simpler mathematical underpinning and are much easier to prove things about. However they are notoriously difficult to use for actual programming, especially in larger projects. Rust's borrow checker is approximately affine types plus regions. Its proof theory gets very complicated if you spell out all the details. However mere mortals can actually write large, complex, and correct programs with it, as has now been empirically demonstrated many times.
- gautamcgoel 6y agoCan 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.
- marcosdumay 6y agoAll 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 6y agoIt’s not just optimization but also correctness. You really don’t want do a bit wise copy of say a file descriptor.
- mhh__ 6y agoHaskell 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.
- dllthomas 6y agoThe 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.
- chrisaycock 6y agoI 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 https://en.wikipedia.org/wiki/Uniqueness_type [2] https://en.wikipedia.org/wiki/Substructural_type_system https://en.wikipedia.org/wiki/Substructural_type_system [3] https://clean.cs.ru.nl/Clean https://clean.cs.ru.nl/Clean [4] https://arxiv.org/abs/1710.09756 https://arxiv.org/abs/1710.09756
- dmix 6y agoMan, 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
- roflc0ptic 6y agoI 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 6y ago> 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 6y agoHow 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.
- whateveracct 6y agoThey'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.
- jose_zap 6y agoSome 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/ 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-data/ 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/ 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/ 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/ https://www.tweag.io/blog/2018-03-08-linear-sort/
- vsskanth 6y agoThank you!
- taktoa 6y agoIt's not "linear" as in linear algebra (well, it is technically, but only in the abstruse sense that the category of the vector spaces and linear maps is a model of linear logic).
- canjobear 6y agoI 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 6y agoThe 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 http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/30/slides/steve.pdf
- drdeca 6y agoThanks! I notice that that translation there doesn’t seem to describe the operation par , only oplus, otimes, amp, linear implication, and the of-course operators. Do you know if the par operator can be expressed with this vector spaces over finite fields setup?
- whateveracct 6y agoA 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.
- pwm 6y agoJust the other day i was doing something with LogicT where QualifiedDo would have been super handy.
- bjt 6y agoThe 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 6y agoWhat’s the issue? GMP is pretty portable, no?
- whateveracct 6y agoit's more about its license
- endgame 6y agoGMP 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 6y agoMy 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.)
- tluyben2 6y agoThat went pretty fast, on a ghc timescale. Well done! Promising for the future.
- whateveracct 6y ago~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.)
- Kbsm 6y agoLearn more about the new linear types extension in GHC here: https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91 https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91
- KirillPanov 6y agoI used to love Haskell, even hacked on GHC internals. But it's pretty telling that Haskell is only getting (pre!)-production-quality substructural types five years after Rust did.
- alexmingoia 6y agoLinear types! Wonderful. And QualifiedDo is elegant and convenient. I imagine many libraries will begin to take advantage both of these extensions.
- rundmc 6y agoShameless plug / comment thread hijack: https://tontine.com https://tontine.com is an award winning Fintech making the global pension system functional and is looking to add more senior Haskellers as well as some junior Haskellers ahead of our upcoming launch in 27 countries. Please get in touch if you are interested to use your Haskell skills to make a positive change in the world.
- tome 6y agoI was reading about this company a few weeks ago. Looks like a really interesting idea!
- lambda_obrien 6y agoI'm really excited to use linear types to try to speed up stream processing! I love Haskell but some of the fusion stuff that speeds up stream libraries can be slow to compile and not that fast anyways.
- creata 6y agoIf I have a list I can only use once, how can I get its length? In Rust, read-only borrows accomplish that, but I don't see a counterpart in Haskell. I feel like getting the length of a list shouldn't count as "using" it.
- mrkeen 6y ago> In Rust, read-only borrows accomplish that Things are already quite 'read-only' in Haskell ;) If you want to touch a list twice, don't mark it as linear. That said, reading a list length (in O(n) time) and then performing an operation on it is usually an anti-pattern. Kind of like scanning a file to count how many lines it has, and then doing something to each line. So linearity could help you ensure that you don't make this mistake.
- creata 6y ago> That said, reading a list length (in O(n) time) and then performing an operation on it is usually an anti-pattern Of course it's unnatural for Haskell lists, but replace "list" with "Array" (or even just the height of a tree, which is merely O(log n)) and I feel that this is a very common and acceptable use. > If you want to touch a list twice, don't mark it as linear. But why are we counting how many times we "touch" the list? Wouldn't it be nice to have some set of operations which get data out of the list without "touching" it? Anyway, the other commenter points out that you can return the array as you compute its length, and yes, that is a common trick with linear types (Idris' experimental linear arrays do the same). But isn't it better to express in the type system that you will use something "nondestructively"? As an added bonus, it'd probably be more ergonomic than constantly reassigning the list.
- mrkeen 6y ago> But isn't it better to express in the type system that you will use something "nondestructively"? That is how regular functions & data work now. It's completely ergonomic, no linearity required.
- 6y ago
- pjmlp 6y agoNice, this is the path I see going forward for mainstream languages, combining GC implementations with linear types.