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".
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
> 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.
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.
It's not as complicated as the lingo. A type is just metadata about variables and values tracked by the compiler on the static code, as it compiles it.
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.
Wow this was a great break down. I've never really heard it in this sort of fashion and it's an interesting approach to teaching types. Language and 'lingo' really does muddy the waters educationally.
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.
Yes I tried Purescript in the early days and it was buggy as hell with little documentation (even blog post tutorials or githubb repos to learn from). So I decided to wait a couple years before checking it out again, which is coming soon I hope...
I love Elm but if the poster wants Haskell-ish experience purescript is much more similar. Otoh Elm is simpler and therefore might be a better next step. But since they already seem to have Haskell experience I’d generally recommend purescript if they just want to learn. If they’re choosing a technology for a production product then that’s a completely different consideration
I just want to say I concur with this. I don't consider Elm a full alternative to Purescript, even though I understand the draw.
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.
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.
Yes me too, and shout out to https://gitlab.haskell.org/users/hsyl20 behind this work, who has been doing the unglamorous work of refactoring away decades of tech debt in GHC like no person ever before, to the best of my knowledge.
(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.)
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).
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.
Why not? I mean out of all the commercial projects that could be open sourced, games are actually great to have under GPL, because the assets (art, animations, etc) are are still under copyright but the code and logic isn't, which isn't as important to a game as to, say, enterprise CRUD software. Plus with open source game code, modders could make much out of your game.
Because the requirement to make replacing the LGPL code possible means that there is no possible way of preventing cheaters in online play.
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.)
If your attempts to prevent cheating rely on a "trusted" client, you're going to have cheaters whether or not your code is LGPL. The only right way to stop cheaters is to run game logic on the server.
A lot of cheats are visual cues and only alter the rendering, not the game logic: wallhacks or texture hacks for instance. You also have auto-aim cheats, etc. Running the game logic on the server, which you should do, will not help in these cases.
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.
Can't you fix wallhacks by just having the server not send the position of things that the client doesn't have line-of-sight to?
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?
> Can't you fix wallhacks by just having the server not send the position of things that the client doesn't have line-of-sight to?
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.
LeagueSharp (developers of cheating tools for League of Legends) is said to have had a revenue of several million dollars per year for their subscription services. I would say that this classifies as serious business.
It's non trivial. A lot of games require trusted clients because of client side latency compensation. Also any game that requires mechanical skill (e.g. aim in an fps or actions per minute in rts) is susceptible to cheating even if all logic is serverside.
Of course trusted clients are problematic, but there is no simple solution.
But just not releasing the source code doesn't even stop those kinds of cheats. Even games that make you install a privacy-invading kernel driver to play still get cheaters.
Yeah. Realistically, this is like trying to reprogram your opponents brain to prevent them from cheating at basketball... even if you make it work, it is morally untenable: you need a referee.
Some actually did, back in the day of point and click adventures. But nowadays games obfuscate everything as much as they can for DRM and anticheat purposes. If you consider your own customers your enemies, of course you wouldn't open anything to them
Let us not act as if the LGPL be the only free software licence that exists.
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.
Aren't GPL-incompatible licenses generally considered poor choices even if they're FOSS, since they lead to the ZFS-on-Linux problem? (And trying to sidestep the issue with permissive licenses just leads to proprietary forks.)
> 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.
Perhaps it was, but it is very difficult to create a strong copyleft licence that is not the GPL that is compatible with the GPL, and that goes for any strong copyleft licence in every direction, so much so that GPLv2 is not compatible with GPLv3.
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.
"Bully"? As if people were supposed to specifically review licenses they create, whether they're compatible with every GPL clause. Nobody needs to care about GPL, it doesn't deserve special treatment.
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.
You're mixing up freedom and power. It's impossible to have a license more free than the GPL. The extra thing that permissive licenses give you isn't more freedom, but rather the power to withhold freedom from others. See https://www.gnu.org/philosophy/freedom-or-power.en.html for more details.
GPLv2 does not permit code be incorporated into a GPLv3 licensed project.
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 does address version incompatibility, the problem is that some popular projects flat out refuse to follow their guidance.
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.
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.
> 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?
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.
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.
Which kind of proves where the BSDs would be if there wouldn't be any Linux to contribute to, given the unstoppable upstream contributions to BSD variants from World + Dog.
I mean I agree with you, but what does that have to do with portability? I don’t see how this affects which computer architectures and OS environments a project can be compiled for.
I agree portability isn't the right word here. But dealing with libgmp's license was a pain in the ass for commercial development - theoretical possibility of doing commercial FOSS notwithstanding.
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)
> Haskell remains at the bleeding edge of general-purpose programming - more than ever with each release.
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).
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.
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.
I’ll also add that you can achieve some of these effects without linear types, but linear types are more flexible. For example, a classic way to work with a file in Haskell is to use the function withFile:
Yeah, this is what I meant by "the bracket pattern" and a canonical case where it "doesn't fit" - I appreciate your spelling it out for those who are less familiar :)
Negative consequences are whatever use-after-close errors you make trying to use the thing you returned. ... but I certainly agree that it's not an error that's made very often, and the flexibility is the bigger point.
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.
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)
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.
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/
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.
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.
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.
> 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.
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.
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.
This has been expressed, but I do not think it is true. Yes, the original linear logic doesn't have anything like a "linear kind", but that's mainly because it's a logic not a type theory. The classic A → B = !A ⊸ B could be interpreted as something like A → B = GC A ⊸ B, i.e. making the ! an in-language type constructor not some sort erased modality.
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!
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.
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.
The general idea is that the discipline is automatically enforced via the type system, e.g. you have a library which provides a type FragileAndDangerousResource, but the only way to interact with such a thing is via (linear) functions along the lines of
withFADR :: (FragileAndDangerousResource #-> a) -> a
addToFADR :: Int -> FragileAndDangerousResource #-> FragileAndDangerousResource
In other words, linear types are purportedly useful precisely because they make it reasonable to ask for that extreme discipline on the programmer's part, because the compiler is right there to tell them when they screw it up--ideally with a helpful error message.
withFADR :: (FragileAndDangerousResource #-> Unrestricted a) -> Unrestricted a
One can't tag "linear" values in the type system but one can tag non-linear "unrestricted" values. See "borrow" in Section 7.2, page 5:26 of https://arxiv.org/pdf/1710.09756.pdf
Yeah, that seems right. I'd also believe you if you told me that the second arrow also needs to be linear, since I can't really give a good reason why it should be one way or the other off the top of my head.
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.
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!
There are a number of Haskellers with similar misgivings. The authors of the current extension thought that this fit most nicely with the current language / implementation.
I don't see how, in the presence of unrestricted function types, you can tag values as linear unless you have a separate kind for linear values. I'd be interested to know how Rust does it.
"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.
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
From 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`.
For 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.
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.
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.
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.
It'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).
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.)
If 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.
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.
> 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.
> But why are we counting how many times we "touch" the list?
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.
Sorry: you seem to be misunderstanding me, but I do not know how to express myself better.
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.
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.
Thanks!
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?
I'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.
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