GHC 9.0, supporting linear types
discourse.haskell.org
discourse.haskell.org
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
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
Haskell has a tendency to make every problem seem exactly the same :)
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.
Purescript is more in line with the harder core FP or frontend Haskell I was seeking.
On another note, Rust does types and pattern matching quite well where I see that as another draw away from Haskell. But I feel like Haskell is the motherland for this stuff so might as well figure it out eventually.
Normally types are used to indicate the set of values a variable is allowed to contain or not. And that info can be used by the compiler to detect mismatch in the code, like if a value is being assigned to a variable that doesn't match its type.
But like I said, this is all just metadata about variables and values. So what else could you track and enforce? Well you could also track that some values are never assigned to more than one variable. That would be Uniqueness types. A value of such type is supposed to always have a unique variable pointing to it. So you can't have two variables pointing to it, if you did, the compiler would throw an error.
Linear types are similar, with some small differences in the edge case. Specifically, you can cast a value that is non linear to be linear. In effect it means a value that is made linear can not have more references to it after it has been made linear, but it could have many references pointing to it from before it was made linear. Where as a value of a unique type would not allow that.
To recap, Uniqueness guarantees that a value has no other references to it, while linearity guarantees that no more references can be made to a value.
Finally you have Affine types, which are also just a small difference to the above two. One detail I ommited is Linear and Unique types will also fail if the value is never assigned to any variable. They basically enforce that a value having a linear or unique type must be used at least once. An Affine type is like a linear type that doesn't have to be used at all, thus they say it needs to be used at most once.
I'll add one more, Ownership types, like in Rust. Those are like a mix of unique and affine. In that a value with an ownership type can only be refered to by its current owner, but doesn't have to be. It's different to unique types in that the owner is free to refer to it many times, but no other owners can refer to it at the same time.
So you see, all of this is just lingo to say, could we come up with some constraints around how many references to the same values we're allowed to have. Then create a type for them so we can tell the compiler to enforce those constraints on values of that type.
Now it gets complicated to actually find a way to implement a compiler to track these types and enforce their constraints. That's where the research and challenge is. And it's also tricky to figure out how the programming language can use these and how to make them pleasant to use and not feel like annoying constraint that prevent you from doing things easily.
I appreciate you writing this out for me. I understand the 3 types you described quite clearly.
The compiler stuff I fortunately won't have to care as much about (unless I do this fulltime or go even harder core into types) but I appreciate your approach to it.
I believe learning Rust has helped me understand Haskell and the utility of even basic things like Maybe/Option types. Compared to like Go or whatever I want it plus pattern matching in every language I use now (pattern matching is another thing I gleaned from Erlang/Elixir as extremely useful).
Anyway, I'll find time at some point down the road to understand this better.
Holy crap! That's amazing and I hadn't thought of that!
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.
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.
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.)
Because like everyone else, I am using 20 different pieces of proprietary middleware which have licenses that are incompatible with GPL. (Not just that I can't GPL them, but which cannot be shipped as part of a distribution where some of the code is GPL.)
Of course trusted clients are problematic, but there is no simple solution.
Running the rendering itself on the server (Stadia) would probably help, but even then with a hacked client you could add auto aims, and alter the visual stream.
And as for auto-aim, can't cheaters do that no matter how draconian your anti-cheat measures are, by, e.g., connecting a fake USB mouse connected to a camera pointed at their screen?
No, at least not for real-time games. Latency compensation means that the client needs more data than the player "should" see.
> And as for auto-aim, can't cheaters do that no matter how draconian your anti-cheat measures are, by, e.g., connecting a fake USB mouse connected to a camera pointed at their screen?
If you can make a USB device that does that, I'm sure you have better things to spend your time on that trivial matters like cheating in games.
Still... the proposal by the poster I replied to basically amounts to something close enough to general AI so as to be world-changing stuff, IMO. :)
Even among free software advocates there are problems and they might favor another free software licence, even another copyleft licence, and that can't be done in this case.
There is a reason that many large projects in fact craft their own licence rather than relying upon another template, as they do not meet their needs.
Strong copyleft licences are generally not compatible with each other; GPLv2 is not even compatible with ̀GPLv3.
https://sfconservancy.org/blog/2016/feb/25/zfs-and-linux/
> We believe Sun was aware when drafting CDDLv1 of the incompatibilities; in fact, our research into its history indicates the GPLv2-incompatibility was Sun's design choice. At the time, Sun's apparent goal was to draw developers away from GNU and Linux development into Solaris. Not only did Sun not want code from GNU and Linux in Solaris, more importantly, Sun did not want technological advantages from Solaris' kernel to appear in Linux.
Given Sun's goal, no matter what GPL said, I am sure that they would have figured out a cute way to engineer their license to be incompatible.
It's rare to find two strong copyleft licences that are compatible with each other — advocates of strong copyleft typically phrase their arguments as if there only be one strong copyleft licence in existence, as this is the major problem that is hard for them to overcome that is seldom sung.
Other licenses not compatible with GPL:
- Apache License (only version 2 is compatible and only with version 3 of GPL);
- GPL (v2 vs v3), as other comments already mentioned.
Are the authors of those licenses bullies? No. Nobody needs to care about your favourite flavour of copyleft.
World+Dog has generally switched to Apache or BSD licenses for most things.
Which are, for most any dimension anyone cares about, more free than *GPL.
There are things that I, as Joe Developer downloading some software can do with BSD licensed code that I can do that I can’t with copylefted code. I am...more free to do with it as I wish.
No amount of GNU/Bloviating will make that not true.
GPLv3 does not permit code be incorporated into a GPLvv licensed project.
The M.I.T. licence, for instance, permits both.
This is something the F.S.F. always fails to address in these talks; they speak proudly how the GPL guarantees that code never end up in properietary software, which is true, but only because that is a special case of code not ending up in essentially any project with only a slightly difference licence, including proprietary software.
the GPL guarantees that the code be off limits to proprietary software, permissive free software, other copyleft than the GPL, and even other versions of the GPL, and this is something they bury, and continually fail to address.
The FSF uses the approach of asking people to release programs under “GNU GPL version N or any later version.” This licensing is compatible with version N, and also with N+1 (because it offers version N+1 as an option). When you combine code under “GPL 3 or later” with code under “GPL 2 or later”, the license of the combination is their intersection, which is “GPL 3 or later”.
Licensing under GPLv2+ only allows one's code to be used in all GPL projects, not other copyleft licences, but that's not the full problem: it does not allow one to use code of anything other than GPLv2+. At this point one can't use GPLv2 or GPLv3 code any more, only GPLv2+ code.
Furthermore, licencing under GPLv+ puts blind faith into the F.S.F.; it irrevocably licenses one's code under a licence that doesn't exist yet.
When GPLv4 is eventually released, the software is now released under it, and GPLv4 might contain provisions one doesn't agree with, but one can't revoke it now.
IT's absolutely not a solution.
The CDDL was intentionally written to be incompatible with the GPL. Which other copyleft licenses do you have in mind, and what advantages do they have over GPL-compatible licenses?
> When GPLv4 is eventually released, the software is now released under it, and GPLv4 might contain provisions one doesn't agree with, but one can't revoke it now.
If you release your code under a permissive license, it's basically guaranteed to be compatible with the future GPLv4, so you're in that situation anyway.
What strong copyleft licence do you know that is compatible with any GPL?
The F.S.F. indeed alleges that it was intentional, and perhaps it was, but every single strong copyleft licence is pretty much incompatible with every other — one must go out of one's way to make them compatible and even it's typically an asymmetric compatibility.
Advantages? They obviously do things differently and there's probably a reason why big companies tend to craft their own licence rather than relying upon a template.
Examples:
- Eclipse Public Licence - Mozilla Public Licence 0.1 and 0.2 - Apple Public Licence - Common Development and Distribution Licence - GPLv2 — yes, it should be mentioned as an example
> If you release your code under a permissive license, it's basically guaranteed to be compatible with the future GPLv4, so you're in that situation anyway.
You assume that the only option one have is GPLv2+ or a permissive licence.
Linux is simply released under GPLv2, exactly because Linus Torvalds and many others in it disagree with some of the GPLv3 provisions; ZFS is simply released under the CDDL, and FixFox simply under the MPL.
They have their reasons to choose other licences than GPLv3, because they disagree with some of the provisions thereof.
Besides, it hardly matters that Darwin has an outdated FreeBSD as part of its hybrid kernel.
As long as a relinkable form of the closed source executable and/or sources of the LGPL library/ies it uses are provided in an acceptable way (per LGPL terms) then distributing a closed source executable should not be problematic.
https://gitlab.haskell.org/ghc/ghc/-/issues/17957 for example. You would think the Haskell compiler in Haskell would be a shining example of a pure functional programming, but you would be wrong!
(GHC most predates more modern ideas about how programs should leverage pure functional languages. I also speculate early on there was an "innovation budget" idea, conscious or otherwise, that if the language was novel, and the compilation analyses (e.g. strictness analysis) were novel, that was enough, and the domain-agnostic architecture of the compiler should be proven and bog-standard.)
This is worth pointing out one more time. As far as I'm concerned it's the most expressive language I've ever used, and is what I pick if I want to write correct software and am OK spending some time yak shaving (not that you have to with Haskell, I just know that I will).
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.
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.
withFile :: FilePath -> IOMode -> (Handle -> IO r) -> IO r
open file A
do stuff
open file B
do stuff
close file A
do stuff
close file B
There's many other such modal type systems/logics used for other special purposes like temporal logic.
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)
There’s also quite a design space still to be explored for these ideas. Even / especially for languages like Haskell.
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.
Now one can have mutation by simply returning the mutated value which internally can be implemented as mutation since the type system guarantees that the original value never be used after.
Conceptually, it's purely functional programming where a function consumes a value and returns a new one, under the hood it's understood to be mutation which is possible due to these constraints.
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.
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.
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.
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.
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.
Feel free to give GHC 9.0 a try with a minimal example of your scenario!
withFADR :: (FragileAndDangerousResource #-> a) -> a
addToFADR :: Int -> FragileAndDangerousResource #-> FragileAndDangerousResource
withFADR' :: (FragileAndDangerousResource #-> IO ()) -> IO ()
lid :: forall a. a #-> a
withFADR lid
withFADR'' :: (FragileAndDangerousResource #-> ()) -> ()
---
[1]: I'm assuming that's what you're going for with `withFADR`.
I admittedly don't really have a great intuition for how to work with this machinery, since I haven't had a chance/excuse to actually play around with it, to be honest; I'm just going off of a SPJ talk on this stuff I watched many months ago, which I mostly understood at the time, and the paper associated with the GHC implementation, which I understood substantially less of.
withFADR :: (FragileAndDangerousResource #-> Unrestricted a) -> Unrestricted a
I'm not expert at this stuff, but when I was interrogating this before, I found the thesis behind https://ncatlab.org/nlab/show/linear-non-linear+logic as a quite old example (1994, only a few years after the first LL paper from Girard in 1987) of separating the linear and non-linear worlds as two categories with an adjudication between them. This is very compatible with linearity in the types.
That all said, I will admit that the "quantitative type theory" line of research gives the current LinearHaskell a big leg up on integrating with dependent types. See https://ncatlab.org/nlab/show/linear-non-linear+logic for the latest plans on that.
I certainly have no retort. My big complaint about the status quo is we can't even have things like Rust's `Box`, but I have no idea what the operational semantics of `f : pi (b : Box<T>) ...` might be, let alone the static semantics!
func :: A -> 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];
In Haskell, you declare a function
func :: A %1 -> B
// 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 lineI'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`.
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.
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.
Its hard to find real world use examples and learn about linear types when I search online. If anyone has links, that would help.
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.
- 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/
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.)
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.
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.
That is how regular functions & data work now. It's completely ergonomic, no linearity required.
Edit: for reference, I'm looking for an analog of the let! construct from "Linear types can change the world!" and the borrowing usage from the Linear Haskell paper.
Well, right, exactly. Why did you ask for that? Probably there's a reason.
If I understand correctly, you are really asking why this needs to apply to all operations, and I think laziness is probably the answer. If I've asked for a linear list because I want to somewhere change it inline, and I ask for the length and "then" do something that changes that length, the value the length function returns would seem to depend on when (at run time) the change is forced vs the question (and they could possibly be overlapping, if you have sent the length to another thread!). That's not what we want.
Requiring you to pass back a "new" list forces the ordering - either my modification is of the list before I took the length, or the list after. In terms of sequencing, that's exactly what we want.
I do agree that it is a bit disappointing that the types don't tell us that length returns list unchanged.
Do you know if the par operator can be expressed with this vector spaces over finite fields setup?