Linear types are merged in GHC | Hacker News Reader

Linear types are merged in GHC

tweag.io

219 pointstodsacerdoti80 comments

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/.

-XLinearTypes down, -XDependentTypes to go :)

Once that happens, the world will change :)

Wadler might argue that linear types being merged changed the world!

http://www.cs.ioc.ee/ewscs/2010/mycroft/linear-2up.pdf

Haskell still has sort of a way to emulate dependent types in many practical cases, without a ton of work or a huge performance hit [1].

Direct support could be nice, though.

[1]: http://okmij.org/ftp/Computation/lightweight-static-guarante...

Tweag is onto that too. :)

See https://www.reddit.com/r/haskell/comments/gtnayl/whats_the_s... for a recent update.

> the linear arrow says this: a function that has type A⊸BA⊸B is a function that has an AA available to compute with, but it can only use it once. Not twice, not zero times: just once.

Superficially this sounds a lot like Rust's FnOnce. Is there a relation there?

Edit: Actually it sounds like linear functions are more about using their arguments once, internally, as opposed to themselves being called once. So perhaps not. Still would appreciate any further commentary by someone with a better grasp on things than I have.

Linear types are stronger than FnOnce, in that a linear type must be used _exactly_ once. Rust doesn't enforce that if you pass in a function of type FnOnce that it is called.

Thats interesting. I don't quite understand how that would work.

So can you work around that requirement by just going:

    if false 
    then <use my type> 
    else <do my things>

Technically it is used exactly once, but really it will never be used..

That wouldn't work, because the value must be used in all possible control paths. In this case, both the 'then' and 'else' branch would have to use the value.

Just curious, what is considered as 'using' the value?

Passing it as a parameter to a function or returning it

Or applying it if that value is a function. I believe the broader definition would be that it has to appear in an "evaluated" term.

Linear type systems often enforce that requirement by saying both branches need to use exactly the same linear values (or consume the same resources). So your example would be rejected by the type system. For example, the following function would not type check in a linearly-typed language because then branch is using x while else branch is not using x.

    -- Using Haskell-like syntax, '-o' is linear arrow, i.e. lollipop
    foo : Int -o Int -o Int
    foo x y = if y < 0 then x else 0

Rust's ownership system has Affine types (types which must be used 0 or 1 times), which are indeed closely related to Linear types, which must be used exactly once.

Types marked with `#[must_use]` in Rust are pretty close to linear types. But must_use is a lint rather than being integrated with the type system.

> Types marked with `#[must_use]` in Rust are pretty close to linear types. But must_use is a lint rather than being integrated with the type system.

An other issue with must_use is that it just requires use not “consumption” of the value, so if, say, you print it the lint is satisfied. Meaning it’s an issue for resources you’d want to be linear e.g. resources which really should be explicitly terminated because the termination can fail.

Uh so how do you debug linearly typed code if you can’t log values? Or does ghc allow to cheat?

I don't know if GHC provides either, but either a borrowing or a dup feature would handle that (the latter would probably count as "cheat"). There may be other ways as well.

Since linear types are a separate opt-in feature you'd probably need (as far as I understand) you'd need separate printers anyway, so you could probably "cheat" them in. Though I think the sort of structures you'd want to be linear would generally not be amenable to print-debugging anyway.

> We say that a function f is linear when f u is consumed exactly once implies that u is consumed exactly once (defined as follows).

- Consuming a value of a data type exactly once means evaluating it to head normal form exactly once, discriminating on its tag any number of times, then consuming its fields exactly once

- Consuming a function exactly once means applying it and consuming its result exactly once

https://github.com/ghc-proposals/ghc-proposals/blob/master/p...

Linearity Design Space: https://i.imgur.com/s0Mxhcr.png

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

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.

To use linear types for everything will require new libraries, no?

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

There is `linear-base`[1] for this.

[1] https://github.com/tweag/linear-base

I wasn't suggesting this would "ruin the ecosystem". Rather, I was suggesting we might end up with two ecosystems.

LinearTypes guarantee that all values are used exactly once if the result is used exactly once. If an exception is thrown, the result won't be used once and the memory would leak.

One cheap way is to also track the memory with the GC. This is similar to using GC finalizers on file handles - closing handles via GC is inefficient and slow but it's only the last resort.

Another option is to use exception handlers to guarantee that the Ressource is freed. Either one handler per Ressource which destroys all advantages of linear types, or one handler in total and some mutable memory to track the still open resources.

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.

If one needs absolute performance, then their only option is bare metal, as the OS can also induce every kind of delay, including RTOS, so manual == performance goes a long way until it is actually true.

There's a pretty wide area between the current situation and completely bare metal, a gap wide enough to fit the vast majority of performance sensitive applications today. It's not like you have to stop at bare metal either in a world as the hardware can introduce some latency on its own. You really need an FPGA or ASIC to take this to its logical conclusion.

Just like exists a gap between allocating memory like crazy, and taking care where it is allocated from, and what kind of data structures are used before assuming that malloc()/free() are faster than the alternatives without taking into consideration what happens between calling them and the kernel round-trip that takes place.

So, while Haskell isn't D or Nim, there also also more than just one way to allocate memory when performance fine tuning is called for.

And yes, in Fintech that is exactly what they do, reach out for FPGAs and measure cable lengths as well, while on high integrity computing all allocations are static, either at compile time or as part of the application startup, nothing else is allowed.

A unikernel library could put your key process front and center, only providing a unified way to access the hardware.

Things become more interesting when you start to need concurrency. You can of course do it manually, too, controlling every fiber switch (I've seen this done in an engine controller, where all the computatios should complete within one rotation of the shaft.)

Funny how you mentioned unikernel. There's a Haskell unikernel whose development began more than a decade ago: https://github.com/GaloisInc/HaLVM

A hot take: I'd argue that in that case Haskell is not the right tool for the job, anything with assembler support is (C++/Rust).

Haskell is still awesome in doing practical computer science and an eye opener in the power of types, but you are going to throw most of the power away of you start to rely on things that are not formally verified. As soon as you are in "this is semi-correct and semi-defined" you might as well use another tool and let Haskell try to focus on the "100% correct, given x,y and z"-crowd.

I know, I know this is a very simplified view, and it's not 100% correct, but that is what I want Haskell to strive for.

The thing is, Haskell's pretty much the only language with anything approaching a "sufficiently smart compiler". And it performs its optimisations by having a great deal of knowledge it gets from the type system. No, it isn't faster than Rust, but it's an open research problem and I think it's awesome people are still working on it when most platforms have given up.

Besides, it turns out that linear types are useful _without_ performance optimisations: they're very good for modelling state machines e.g. socket lifecycles.

I agree

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?

https://en.wikipedia.org/wiki/Substructural_type_system#Line...

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.

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.

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.

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 × 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.)

Are vector spaces really the right category? In particular the product and coproduct of vector spaces are isomorphic (both isomorphic to the direct sum).

It depends on what you mean by right category. It is true that vector spaces identify certain constructs that linear logic distinguishes, but it doesn't identify everything so it still has some interesting content. Finding models that don't make unnecessary identifications is one of main lines of research in the field.

They're not the right category for computation, but they are a valid interpretation of linear typing. They're one of Girard's original inspirations for linear logic. The resource interpretation came later.

Is there an explanation out there about the vector space model? Perhaps one that relates to Gir87's phase semantics?

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.

> this requires you to discard the intuition that a linear function looks like a line when plotted

To be more precise, linear functions correspond to lines/planes/etc passing through the origin since f(0)=0

So I can't make a linear function that returns a number cubed?

Math.pow(x,y) cannot be made into a linear function?

no.

Why would mult(x,y) be linear then if x has to be used more than once in order to do the actual multiplication?

Sorry, I got confused on the meaning linear.

As explained in the other answer, it's possible to implement the power function which is "type-linear" on each argument, but that function will not otherwise be linear (ie, the mathematical meaning of linear) on its arguments.

In Rust for instance, affine types are used to restrict usage of values linearly, which means that a value passed as argument will be by default moved from caller to callee: The value will not be available anymore to the caller. This has some consequences for instance for binary operators on values which require special care when moved (structures, arrays): with the restriction explained above, a value cannot be passed more than once to a function, and thus doing something like 'mult(x,x)' (where x is eg. a matrix) will not work because x appears twice, but may only be moved once. The solution offered by the language, called "borrowing" is to use references for the arguments: a borrowed value is no longer being moved; instead, it remains in the scope of the caller, and the callee only receives a reference. References may be created and duplicated, allowing multiple uses of the same piece of data.

Forgive me but if we actually have to implement mathematics from pure computational theory, wouldn't type-linear functions be equivalent to actual mathematical linear functions?

Well, if copies may be borrowed, as it is the case in Rust, I suppose that a type-linear function, as I called it, doesn't have to be computationally linear. The `mult` example we discussed could not be applied twice to the same value, unless it is declared as borrowing its parameters from the caller.

Elaborating on this, with a function signature like the following:

    fn mult(x : Vec<f32>, y : Vec<f32>) -> Vec<f32> {
       // matrix product implementation 
    }

arguments x and y cannot point to the same value, because a value cannot be moved twice. A call like

    mult(a,a)

will generate an error.

Conversely, with the following signature:

    fn mult(x : &Vec<f32>, y : &Vec<f32>) -> Vec<f32> {
       // ...
    }

the call:

    mult(&a,&a)

will typecheck, because values are passed by reference.

Now, nothing prevents one to implement the function square, based on the second version of mult:

    fn square(x : Vec<f32>) -> Vec<f32> {
        return mult(&x,&x)
    }

which is type-linear on its parameter x, but computationally is not linear.

Clearly your original question was spot on.

I see what you mean with the copying. I just thought based on OPs comments there would have been a strong correspondence between lambda calculus numbers (Church encoding) and the operations on them, and actual type-linear functions.

You're taking the intuition a little too far, I think. If we're talking about linear types, Math.pow can be linear because you can _copy_ the value x as many times as you want. As far as memory management is concerned, the x that was passed in was only used once (to make however many copies).

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.

The original name was because the logic seemed to do with time. If some proposition p is true, and then some event q comes along and we can derive "if p and q then r" then now we know that r is true, but we can no longer be sure that p is still true. Maybe the derivation of r was an event or it transformed the nature of p in some way and we can't go back. People don't really think of linear logic as being temporal (one thing happening after another) anymore, the "resource interpretation" is more common, although still not 100% accurate. In this view, p is a resource that is consumed by q when r is derived. The logic/axioms are the same in both cases, it's just what people's subjective intuition says the logic describes. If linear logic finds its way into mainstream programming, it will probably be just in the simplified sense of "use-once function" like you called it, which is a little bit like calling lambda calculus using functions without names.

The proposal is described here:

https://github.com/ghc-proposals/ghc-proposals/pull/111

I wanted to try this out, but getting nightly GHC was a bit harder than expected. Threw up a repo on how to set up nightly binary on buster and compile with -XLinearTypes:

https://github.com/rjeli/hs-linear-example

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.

I hope they implement this in Agda as well.

Actually I wonder if its not already possible to implement it since it has had levels of universes for quite a while. Is that, with dependent types, not powerful enough?

I remember asking this question on agda subreddit a while ago (maybe 3 years ago? I don't know) and they told me it's not possible. However, they implemented Cubical type theory and a few other stuff (universe levels? Has it been implemented last couple years?) so maybe it's possible now.m

I love doing algebra proofs with agda as a hobby but I'm by no means, even remotely, experienced in everything agda capable of.

Awesome work!

I still kind of wish that something RAII-like that is safe in the presence of exceptions and & types had made it in. But considering the immense amounts of work and effort that this has taken adding some more sweeping changes is somewhat of a pipedream.

The current version definitely looks practically useful, though kinda awkward given the syntax and polymorphism restrictions.

Wow very cool stuff. I'm wondering if these ideas could be integrated into the rust type system.

It’s unclear if Rust can ever get linear types: https://gankra.github.io/blah/linear-rust/

FWIW, from having built types like this in C++ before, the thought process at the end of how to handle assignment feels better to me to implement where instead of assigning Some(step1()) directly to token, you construct a new value and then "swap" (which is a C++ concept that is supposed to be guaranteed noexcept) the token variable and the value variable; you then would have until the end of the scope to call some function that asserts the value is None. Regardless, I agree with footnote 3: if you want to claim that linearity is somehow a bad default, then you should take a long hard look at move-only... but I like move-only, and I like linearity! ;P FWIW, I don't think this is that hard: require all values to be forgotten, allow types to provide deconstructors called on unwind / scope exit, require that deconstructor to eat the value, and if a type doesn't have a deconstructor then the user has to eat the value (and you get all the cool behavior of not being able to hold it across a panic without having some way to guarantee it will get eaten, such as by holding it in a container that has a deconstructor that will eat it). This would be epic and would be a pretty awesome sell to get me on Rust ASAP despite the devastating decision to not have implicit error propagation ;P. Like, seriously: I have way more concerns about linearity issues in my codebase--ensuring proper deconstruction of non-memory resources in an asynchronous context (which is where this gets hard)--than I do with my memory correctness... I can't begin to explain how much time I have spent over the past two months chasing deadlocks or premature synchronous deconstruction of an object that absolutely must deconstruct synchronously... I have these "deconstructor bombs" (as mentioned in this article as supposedly an ok solution: no, they really really suck...) throughout my codebase, but I have found it infuriating to come up with rigorous local heuristics to ensure that everything always gets closed in the right asynchronous context :( and so I would be willing to jump through almost any hurdle to use a language that could simultaneously promise me tight memory usage (which sadly Haskell isn't great at, due to its garbage collector, but I am going to seriously look at it again I guess?) and linear types (preferably universally, similar to focusing on movable types).

> FWIW, from having built types like this in C++ before, the thought process at the end of how to handle assignment feels better to me to implement where instead of assigning Some(step1()) directly to token, you construct a new value and then "swap" (which is a C++ concept that is supposed to be guaranteed noexcept) the token variable and the value variable; you then would have until the end of the scope to call some function that asserts the value is None.

For this specific case Rust has mem::swap and Option::replace (though the essay probably predates the latter), however the essay really seems to be using this as just an example of entire rust constructs becoming impossible to use, and / or having to be replaced by significantly less convenient ones e.g. every reassignment having to become a mem::swap + a check means a single-line statement becomes 3 different statements (possibly a utility function implementing that).

> require that deconstructor to eat the value, and if a type doesn't have a deconstructor then the user has to eat the value

But the point of the panic issue is that the user can't consume the value in that case isn't it? Though I don't understand why gankro didn't mention the option of a fallback `Drop` for use during unwinding (which would probably default to a deconstructor bomb).

> I can't begin to explain how much time I have spent over the past two months chasing deadlocks or premature synchronous deconstruction of an object that absolutely must deconstruct synchronously…

That's already the case for Rust? Drop always occurs at end-scope at most.

Moving objects to other threads in order to free them asynchronously is a specific pattern (mostly useful for large collections of heap-allocated objects), I don't think it's something Rust will ever do for you as much of the language relies on RAII, which itself relies on synchronous destruction.

> I have these "deconstructor bombs" (as mentioned in this article as supposedly an ok solution: no, they really really suck...)

Note that they're only mentioned as a solution for unwinding affecting a linear value, because panic can be recovered from. Essentially the deconstructor bomb would be as if every linear type had an implicit Drop which panics: drop would never be invoked during "normal" explicit deconstruction, and a double panic (panicing during unwinding) is already an abort.

> or this specific case Rust has mem::swap and Option::replace (though the essay probably predates the latter), however the essay really seems to be using this as just an example of entire rust constructs becoming impossible to use, and / or having to be replaced by significantly less convenient ones e.g. every reassignment having to become a mem::swap + a check means a single-line statement becomes 3 different statements (possibly a utility function implementing that).

I am trying to explain why the semantics of this way of doing the replacement is cleaner and requires less weird special cases in the code (such as this object that is temporarily dead and suddenly revived) than the way in the article (which I see as a strawman designed to make me dislike linear types).

> But the point of the panic issue is that the user can't consume the value in that case isn't it? Though I don't understand why gankro didn't mention the option of a fallback `Drop` for use during unwinding (which would probably default to a deconstructor bomb).

The whole point of linear types is to make it so that this is a compile-time error, so I don't really understand your objection. If it helps, I will try this in a different tense: if the type doesn't (in the continual sense) manage to provide a deconstructor which eats the object (and could be used on unwind), then either the user had to have (in the past tense) or the code didn't (in the past tense) compile if there were (at the time of compile) any codepaths without nothrow that could cause such an unwind.

> > I can't begin to explain how much time I have spent over the past two months chasing deadlocks or premature synchronous deconstruction of an object that absolutely must deconstruct synchronously…

> That's already the case for Rust? Drop always occurs at end-scope at most.

I think I lost an "a-" there, so I'm hoping that if I said "must deconstruct asynchronously" this makes more sense? Otherwise I'm reading the rest of your message as actually kind of insulting my intelligence a bit (that's ok ;P I don't feel particularly intelligent today anyway ;P), so I'm going to assume this missing "a" was a serious problem and kind of shift the discussion to focusing back on the problem statement instead of trying to address any of it directly.

So, I've been doing C++ development since before it was standardized, which I note only to make it clear that I am so painfully fully bought into RAII that I can't even begin to describe how poor my mental opinion of manual management of anything is at this point. With such background, I'm also mostly working on distributed systems that aren't just multi-threaded but are also multi-machine. That said, I don't want this to sound like some complex corner case: most of my actual code is simple stuff like "I want to do API calls using HTTPS" or like "I want to build a VPN/proxy". (Notably, I have spent a lot of time also coding such systems in Erlang.)

I thereby end up in situations where I'm simultaneously dealing (but never "handling" if I can possibly avoid it) weird distributed error cases (and thereby am somewhat dissatisfied with Rust having adopted the data structure from systems that use monads for error handling without the actual syntax part that makes that awesome while simultaneously attempting to claim that exceptions are somehow any less "monadic", when they are just the syntax part without the data structure; so like, neither expose the monad, but Rust forces me to reify it constantly... but I semi-digress).

The issue is then when you are dealing with all three of what should be monads in a more powerful language at the same time: error propagation (whether manually by way of Maybe types or automated by exception/panic), deterministic finalization (RIAA, which isn't often described as a monad but definitely is one), and asynchronous execution (without threads). You are thereby inside of an asynchronous function (which in both Rust/C++ you have to manage manually using async/await) and need deterministic finalization (which in both Rust/C++ you can have automated using deconstructors), and yet errors can happen (which makes the problem obvious but is not at all requires for the problem to happen).

As a basic example, you finish your SSL request, and now need to deconstruct the SSL connection, which means you want to close the socket... only no, you first need to do an asynchronous SSL CloseNotify, so you have to await that behavior before you allow that socket object to deconstruct. If you let the object deconstruct before you await the CloseNotify, you haven't really completed the protocol. This is also a great case, as while HTTP itself mitigates this (and even in my system I eventually decided to just close this socket by force), you aren't really supposed to trust where the end of the data you got from the server is (and so in the abstract thought process you can't really return from this function until you've finished this CloseNotify; this means that trying to fire-and-forget this to a background thread--which is essentially the analogy of garbage collection--is not a valid solution).

I thereby end up with abstractions that look like an asynchronous "using" statement for that case, to prevent me from constructing the object without showing that I'll asynchronously deconstruct it, and I have primitives now for the cases where it is safe to shift to another thread (these are generally cases where I already had a shared pointer to something needing this behavior), or the case where it is primarily (and permanently) owned by another object (though this only half-solves the problem as the order of operations hasn't generalized yet)... and I've set it up so you have to explicitly say "I know what I'm doing" by mixing in another subclass in order to instantiate this object at all outside of one of my more "guaranteed" mechanisms, and yet the problem remains, and is just all over anything that involves networking: you have to be able to guarantee that you have completed asynchronous deconstruction of the object (which might fail! this makes the whole problem harder, but doesn't really change its character at all) before allowing a synchronous deconstruction.

I have seen attempts in both the Rust and C++ communities to then define what an "asynchronous deconstructor" would look like (fwiw, the C++ one looks a lot better), but they frankly all miss the mark (and lead to other soundness issues, which is why they are stuck in design phases and when they come out will likely have tons of compromises... the Rust proposal doesn't even look truly asynchronous) as the core problem here is really one that comes down to linear types: you need to guarantee that the object's lifetime doesn't end--at compile time, or you are just throwing deconstructor bombs at the problem--before you've finished its asynchronous deconstructor "somehow" (and that can be by any number of techniques, and is all up to the developer).

And then, as I noted: this has been the #1 source of subtle bugs in the systems that I build, as this is essentially "fearless concurrency" taken to the extreme of "fearless networking" (though to really approach that you have to have a serious conversation about "what is an error, anyway?" that I'm not sure the Rust community will ever accept ;P). So yeah, like: it is super disappointing to hear that Rust might just never end up with linear typing because I guess people understand the need for it about as little as C++ programmers appreciate the need for lifetime analysis (which is ironically in a design space very related to linear types, and why I'd expect that if I go to all that trouble I'd also be given a solution to my asynchronous deconstructor problem that didn't involve deconstructor bombs; like, I will again say that I loved that footnote #3 ;P).

> I am trying to explain why the semantics of this way of doing the replacement is cleaner and requires less weird special cases in the code (such as this object that is temporarily dead and suddenly revived) than the way in the article (which I see as a strawman designed to make me dislike linear types).

I've always read that article as exposing linear types as more complicated than just slapping a attribute, at least within the context of Rust, but it might just be a naive view of it.

> The whole point of linear types is to make it so that this is a compile-time error, so I don't really understand your objection. If it helps, I will try this in a different tense: if the type doesn't (in the continual sense) manage to provide a deconstructor which eats the object (and could be used on unwind), then either the user had to have (in the past tense) or the code didn't (in the past tense) compile if there were (at the time of compile) any codepaths without nothrow that could cause such an unwind.

But the point of using linear types is that there are constrains which the normal drop does not fulfil or allow for e.g. the deconstruction is failible, or requires additional data, or (as seems to be your case) needs to be moved off-thread. During an unwind, these things are not guarantee or even available at all (how would unwinding know what parameters to provide? How can it report errors to a caller which doesn't exist?). Otherwise the regular Drop would work fine.

> I think I lost an "a-" there, so I'm hoping that if I said "must deconstruct asynchronously" this makes more sense?

It does make a lot more sense yes.

> As a basic example, you finish your SSL request, and now need to deconstruct the SSL connection, which means you want to close the socket... only no, you first need to do an asynchronous SSL CloseNotify, so you have to await that behavior before you allow that socket object to deconstruct. If you let the object deconstruct before you await the CloseNotify, you haven't really completed the protocol. This is also a great case, as while HTTP itself mitigates this (and even in my system I eventually decided to just close this socket by force), you aren't really supposed to trust where the end of the data you got from the server is (and so in the abstract thought process you can't really return from this function until you've finished this CloseNotify; this means that trying to fire-and-forget this to a background thread--which is essentially the analogy of garbage collection--is not a valid solution).

Ah I see, even in the original I think I'd have misunderstood what you meant by asynchronous deconstruction because I wasn't thinking of the "async" context when I read your comment.

Anyway thanks for the expounding on your issues and their relevance to linear typing.

I am pessimistic about this one, but we'll see.

It’s obviously ok to be pessimistic, but at least explain why.

Do you think the feature is not going to be very useful in a practical setting?

Do you fear people are going to use it all over the place in libraries and make life harder for their users?

Is there something wrong with this feature in a theoretically basis. Does it need more thought?

Do you think the implementation is broken or not finished? Does it need more work?

Something else?

Yes to almost all of that. The proposal process has exhausted me, but I suppose I will write it again, since your questions there serve as excellent section headings :).

> Do you think the feature is not going to be very useful in a practical setting?

Yes. For one example, you cannot write anything like `malloc :: Word -> LinearPtr Void`. With, `malloc :: Word -o Ptr Void`, since Word is not duplicable, `Ptr Void` would be. The "solution" is to CPS everything, which is pointed out in the paper and they say it's OK cause some big honking monad can take care of that, but I don't buy it, and I don't believe in "zomg all the effects" monads either.

Haskell is supposed to lead they way with type system features, but I think we are the ignorant followers on this one (At least Go outsourced generics!!). There's so much that can be learned from Rust, and yet I don't think this feature learns those lessons. In particular, anyone that spent any time with Rust would realize that borrowing / borrow checking is super important for making something actually usable.

Unfortunately, regions/lifetimes are far less studied theoretically! So the first step would be not making some linear proposal that cherry-picks theory to make for an easier implementation, but go back to the ivory tower and figure out what the hell this borrow checking is and how to understand it better.

> Do you fear people are going to use it all over the place in libraries and make life harder for their users?

Yes, it is a fact that lot of Haskell users are magpies driven by boredom with the rest of the industry. That's certainly how I was when starting Haskell! I think there is a tendency to be attracted to shiny new features and have fun with them, which is fine itself. But this will lead to a bunch of PRs to all the core libraries, which is understandable too, since no feature works except for at scale.

However, if this proves to be a bad feature as I fear, then we will be left with a bunch of newly-complicated core libraries on this debt-end route. And no language ecosystem I know I think has a good story for deprecating and cleaning up failed experiments in a timely matter. I think we are just too small and disorganized a community to risk our ecosystem like this.

> Is there something wrong with this feature in a theoretically basis. Does it need more thought?

Yes, I think linear types should be a separate kind, like runtime reps. Right now there is just a linear arrow with normal types. If you recall the relationship between --> in the language and |- in the meta language, it feels to me that the meta language has no kept up.

I really do believe more in affine types, but think linearity is useful for fixing Rust's Drop to be a dual to Copy and Clone (Types are linear by default, you can right a designated destructor (like Clone) for RAII, or furthermore (in some cases) use a built-in special no-opt destructor (like Copy).

https://arxiv.org/abs/1803.02796 is a paper from the OCaml community that I think is on much better footing.

> Do you think the implementation is broken or not finished? Does it need more work?

No. I haven't looked at the implementation but this doesn't worry me as much. I think the features were chosen to make an implementation without even more effort tractable---I'm sympathetic as it's enough work as it is and I do commend Tweag for marshaling the resources for our commons at this scale even though I do not agree with what is actually being done. Cleaning up GHC is easier than cleaning up the library ecosystem, and in this case a smaller implementation helps.

Love it, the productivity of tracing GC with the tools to do more fine grained resource management when needed, congratulations!

Is there a short and simple explanation, for what "linear types" are?

GHC?

Glasgow Haskell Compiler https://en.m.wikipedia.org/wiki/Glasgow_Haskell_Compiler

A Haskell compiler whose implementation of Haskell has essentially become the language itself. They add lots of experimental features for their users to play around with, such as linear types it would seem. Language extensions like this might make it into the official language, but probably not. I'd say don't use it in production, but if you're using Haskell, you're probably an academic, hobbyist, or mad scientist.

To be honest I was 80% sure it was Haskell but I do hate acronyms being used without sufficient context for the average reader to understand them. The post should have had the word "Haskell" in it. It certainly helps understand what "linear types" probably means.

Reply on news.ycombinator.com