1. 54

  2. 9

    Great news! I am eager to try this!

    Turn on -XLinearTypes, and the first thing you will notice, probably, is that the error messages are typically unhelpful: you will get typing errors saying that you promised to use a variable linearly, but didn’t. How hasn’t it been used linearly? Well, it’s for you to puzzle out. And while what went wrong is sometimes egregiously obvious, it can often be tricky to figure the mistake out.

    So, basically, GHC just got its own “Syntax error” a la OCaml… just a bit more specialized :p.

    1. 11

      Maybe it’s just me, but to me OCaml’s errors are terse and unhelpful and GHC’s errors are… verbose and unhelpful. ;)

      There are interesting papers that show working ways to improve both, but I wonder why none of those improvements are in the mainline compilers.

      1. 2

        Good error reporting is easiest if it’s built into the compiler front end from the start. If a new algorithm comes along to improve the error information it’s almost never going to be a simple job to drop it into an existing compiler.

        You need type information & parse information from code that’s potentially incorrect in both spaces, so any error algorithm usually has to be tightly integrated into both parts of the compiler front end. That tight integration usually means that improving compiler errors is a significant amount of work.

        1. 3

          It varies. What puzzles me is that a lot of time ready to use, mergeable patches take much longer to merge than they should.

          Like this talk: https://ocaml.org/meetings/ocaml/2014/chargueraud-slides.pdf

          1. 1

            Do you also have a link for a patch for the improved error messages?

            A lot of work has been going on to move OCaml to a new parser and improve error messages. Even though there is a lot still needed to be done, latest releases have started improving a lot. Maybe we can still extract some useful bits from that effort and try again

            1. 2

              Turns out it was even made into a pull request that isn’t merged yet: https://github.com/ocaml/ocaml/pull/102

              1. 1

                Thanks. It is quite an informative PR actually, and explains why the change is not there yet and once can infer why it is easier to add informative messages in new languages and complier but it may be quite hard to retrofit them to seasoned ones

      2. 7

        Would you be kind enough to give me an ELI5 about what linear types are and what you can do with them?

        1. 29

          In logic, normal implication like A implies B means whenever you have A, you can derive B. You have tautologies like “A implies (A and A)” meaning you can always infinitely duplicate your premises.

          Linear implication is a different notion where deriving B from A “consumes” A. So “A linearly implies B” is a rule that exchanges A for B. It’s not a tautology that “A linearly implies (A and A).”

          The classic example is you can’t say that “$3 implies a cup of coffee” but “$3 linearly implies a cup of coffee” makes sense. So it’s a logical form that reasons about resources that can be consumed and exchanged.

          Same in functional programming. A linear function from type A to type B is one that consumes an A value and produces a B value. If you use it once with an A value then you can’t use it again with the same A value.

          This is nice for some performance guarantees, but also for encoding safety properties like “a stream can only be read once” etc.

          1. 6

            Keynote: Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language https://skillsmatter.com/skillscasts/11067-keynote-linear-haskell-practical-linearity-in-a-higher-order-polymorphic-language

            1. 5

              It can be used to model protocols with type signatures. The following is in theory what you should be able to do.

              data ConsoleInput
                  = Input String ConsoleOutput
                  | ExitInput
              data ConsoleOutput
                  = PrintLines ([String] ⊸ Console)
                  & PrintLastLines ([String] ⊸ ())
              greet :: ConsoleOutput ⊸ ()
              greet console
                  = let PrintLines f = console
                    in step2 (f ["name?"])
              step2 :: ConsoleInput ⊸ ()
              step2 ExitInput = ()
              step2 (Input input console)
                  = let PrintLastLines f = console
                    in f ["hello " ++ input]

              If you combine it with continuation passing style, you get classical linear logic and it’s a bit more convenient to use.

              If you model user interfaces with types, they should be quite useful.

              I’m also examining and studying them: http://boxbase.org/entries/2020/jun/15/linear-continuations/

              1. 1

                Wikipedia gives a reasonable overview. The closest analogy would be something like move semantics – for example ownership in Rust can be considered as manifestation of linear types.

                1. 6

                  Rust ownership is linear affine types. Linear types are similar but differ in the details. A shitty way of understanding it is affine types mimic ref counting and prevent you from having a ref count < 0. Linear types are more a way of acting like RAII in that you might create a resource but just “know” that someone later on in the chain does the cleanup.

                  Which I’m sure sounds similar but affine types allow for things like resource leaks but linear types should guarantee overall behavior to prevent it.

                  This all assumes my understanding and explanation is apt. I’m avoiding a ton of math and i’m sure the shitty analogy doesn’t hold up but behaviorally this is how I have it in my brain.

                  1. 2

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

                    1. 2

                      I’m personally of the stance that the 2020 linear ghc stuff is more <= 1 usage, and kinda misses out on a lot of really fun expressivity that can fall out of making full classical linear logic first class. But that’s a long discussion in its own right , and I’ve yet to make the time to figure out the right educational exposition on that front

                      1. 1

                        it definitely seems more limited in scope/ambition compared to the effort ongoing for dependent types, for better or worse. Can’t say I know much about what first class linear logic would look like, but perhaps now there will be more discussion about such things.

                        1. 2

                          The really amazing thing about full linear logic is it’s really sortah a rich way to just do mathematical modelling where everything has a really nice duality. The whole thing about linearity isn’t the crown jewel (though wonderfully useful for many applications ), it’s that you get a fully symmetric bag of dualities for every type / thing you can model.

                          The paper that really made it click for me was mike shulmans linear logic for constructive mathematics paper. It’s just a fun meaty read even at a conceptual level. There’s a lot of other work by him and other folks that taken together just point to it being a nice setting for formal modelling and perhaps foundations of category theory style tools too!

                      2. 1

                        Not sure I can agree that Uniqueness types are the same as Linear types. Care to explain they’re similar sure but not the same thing and your… screenshot of a powerpoint? isn’t very illustrative of whatever point you’re trying to make here.

                        And from my experience with Idris, I’m not sure I’d call what Rust has Uniqueness types.

                        1. 1

                          They are different rows in the matrix because they are different, of course.

                          it’s from this presentation about progress on linear ghc a little over a year ago https://lobste.rs/s/lc20e3/linear_types_are_merged_ghc#c_2xp2dx skip to 56:00

                          What is meant by Uniqueness types here is “i can guarantee that this function gets the unique ptr to a piece of memory” https://i.imgur.com/oJpN4eN.png

                2. 2

                  Am I the only one thinking this is not how you ship language features?

                  If the compiler can’t even report errors correctly, the feature shouldn’t ship.

                  1. 15

                    If the compiler can’t even report errors correctly, the feature shouldn’t ship.

                    Its more this is an opt-in feature with crappy error reporting for now using computer programming design features not in use in most programming languages. Its going to have rough edges. If we required everything to be perfect we’d never have anything improved. Linear types like this also might not have a great way to demonstrate errors, or the domain is new so why not ship the feature for use and figure out what kind of error reporting you want based on feedback.

                    1. 13

                      Many people do not realize that haskell is a research language and GHC is one of the main compilers for it. This is an experimental feature in a research language. If it works out well, then it will be standardized.

                      1. [Comment removed by author]

                        1. 15

                          You have an experimental feature and advertise as such, disable by default. It is not like it will become widely use anytime soon. I don’t get the outraged comments to be honest.

                          1. 14

                            This is utterly unprofessional

                            I disagree. While good diagnostic messages are important in the long term, I think you can permit yourself to have less useful messages in the short term. Of course once shipped, you should dedicate time and resources to improving it.

                            I can’t even remotely imagine how people thought this would be a good idea to ship if it isn’t even clear whether good error reporting is even technically possible.

                            I think the reason is simple: to get feedback on the feature, how useful it is (regardless of the error messages), etc. Based on that you can then decide how to move on, what to focus on, etc.

                            1. 4

                              This is utterly unprofessional – my private hobby project has higher standards than this.

                              Your private hobby project is almost 30 years old, and is used in production in any number of areas as well I take it?

                              As goalieca notes, GHC/Haskell is a research langugage, its got a ton of extensions that you can opt in for, but accept that things can have rough edges largely because its near the bleeding edge of language design. This is one of them.

                              There is literally no point in having this feature if it turns out that nothing can be done about error reporting.

                              Of course there is a point, it is to explore Linear Types in spite of the error reporting. Advice from early “hair shirt” adopters will likely drive the error reporting or work towards a better system. I’m just pointing out that error reporting may not yet be even thought of as a concept of how Linear type systems are used.

                              I’m not saying it isn’t possible, I’m saying it might not even be worth considering yet. Sometimes you have to implement things before you can fully know how to do it right. Same reason why Haskell will eventually move from a lazy language to a strict language. Only after you get decades into a design might you find out it was a dead end. But until you try it, nobody will ever know. In those conditions explain how you expect to learn the tacit knowledge to be “professional”? Someone somewhere has to do the work, this is how it happens.

                              If you ever wondered why software is in such an utter state of disrepair, it’s because of shit like this.

                              To be blunt, your axiomatic thinking is not helping matters, this is what research IS. It is ugly, incomplete, and the only way to move forward. This is the exploration of computer science concepts never implemented anywhere in an existing langauge. Of course its won’t be pretty, it took 4 years to get to “it compiles and we can use it, lets make it a POC/MVP and get feedback from people that see value from it”.

                          2. 5

                            Other people have sort-of said it, but not clearly enough I think. This is not a language feature being added. It is a feature-flagged experimental feature of a particular compiler. Most such compiler extensions never make it into real Haskell, and the ones that do take years after they are added to a compiler to make it to a language spec.

                            1. 4

                              for all practical purposes isn’t “real Haskell” defined by what ghc implements these days?

                              1. 2

                                Yes, all the other implementations are dead. They still work, but they won’t run most modern Haskell code, which usually uses a bunch of GHC extensions.

                                1. 1

                                  You might say “isn’t it not popular to write standards-compliant Haskell these days?” and you’d be right. Of course it’s often trendy to write nonstandard C (using, say, GNU extensions) or nonstandard HTML/JavaScript. However, ignoring the standard being trendy doesn’t mean the standard doesn’t exist, or even that it isn’t useful. I always make sure my Haskell is Haskell2010, and I try to avoid dependencies that use egregious extensions.

                                2. 2

                                  Honestly curious: are there any other Haskell compilers out there? Are they used in production?

                                  Also, what is a definition of a true Haskell? I always thought it’s what’s in GHC.

                                  1. 5

                                    There’s a Haskell which runs on the JVM - Frege. But it makes no attempt to be compatible with the version of Haskell that GHC impements, for good reasons. Hugs is a Haskell interpreter (very out of date now, but still works fine for learning about Haskell.) There a bunch of other Haskell compilers, mostly research works that are now no longer in development - jhc, nhc98 etc etc.

                                    But GHC is the dominant Haskell compiler by far. I don’t think there are any others in active development, apart from Frege, which isn’t interested in being compatible with GHC.

                                    (“True Haskell” is the Haskell defined in the Haskell Report, but real world Haskell is the Haskell defined by what GHC + your choice of extensions accepts.)

                                    1. 2

                                      There are other compilers and interpreters. None of them is anywhere near as popular as GHC, and usually when one does something interesting GHC consumes the interesting parts.

                                      There is definitely a standard, though: https://www.haskell.org/onlinereport/haskell2010/

                                      The whole reason language extensions are called “extensions” and require a magic pragma to turn on is that they are not features of the core language (Haskell) but experimental features of the compiler in question.

                                    2. 1

                                      In short, GHC Haskell is a language designed by survival-of-the-fittest.

                                      1. -2

                                        If you haven’t noticed, the language spec is dead.

                                      2. 3

                                        Overly terse error messages are bad, but they are better than wrong error messages. Some things are much harder to give helpful error messages for than others.

                                        I wish people spend more time improving error reporting, at least in cases when the way to do it is well understood. There is no reason for say TOML or JSON parsers to just say “Syntax error”. But, YAML parsers are pretty much doomed to give unhelpful errors just because the language syntax is ambiguous by design.

                                        And then some errors are only helpful because we know what their mean. Consider a simple example:

                                        Prelude> 42 + "hello world"
                                        <interactive>:1:1: error:
                                            • No instance for (Num [Char]) arising from a use of ‘+’
                                            • In the expression: 42 + "hello world"
                                              In an equation for ‘it’: it = 42 + "hello world"

                                        How helpful is it to a person not yet familiar with type classes? Well, it just isn’t. It’s not helping the reader to learn anything about type classes either.

                                        1. 1

                                          I’ve seen some good suggestions on r/haskell for improving the wording of these errors.

                                        2. 2

                                          The error they’re talking about is a kind of type error they’ve not worked with. It’s produced if you forget to construct or use a structure. I I’m guessing it’s technically “proper” but the produced error message may be difficult to interpret.

                                          They’ve ensured it’s a feature you can entirely ignore if you want to. Everybody’s not convinced they need this.

                                          I otherwise dunno what they’re doing and I’m scratching my head at the message. Something like “Oh cool you’ve done this… … … So where are the types?”

                                          1. 2

                                            So you never got a C++ template error in the good olden days? Seriously though, it just got merged. It’s not released or “shipped” in any means.

                                            1. 0

                                              So you never got a C++ template error in the good olden days?

                                              No, because I looked at the language, figured out that the people involved completely lost their fucking mind, and moved on.

                                              Seriously though, it just got merged. It’s not released or “shipped” in any means.

                                              They took 4 years to arrive at the current state, which I’ll approximate at roughly 10% done (impl unfinished, spec has unresolved questions, documentation doesn’t really seem to exist, IDE support not even on the radar).

                                              So if you assume that there will be a Haskell version in the next 36 years, then this thing is going to end up in some Haskell release sooner or later.

                                              1. 2

                                                So if you assume that there will be a Haskell version in the next 36 years, then this thing is going to end up in some Haskell release sooner or later.

                                                Could you elaborate on this? If practical users of linear types will only use them if they have good error messages, and early testers want to work out the kinks now, what’s wrong with having a half-baked linear types feature with no error messages permanently enshrined in GHC 8.12?

                                        3. 2

                                          This is incredible! I had no idea this effort was going on! Can anyone speak to the performance implications? I assume the back-end is making minimal use, currently, but am I correct in thinking that, in theory, this could enable performance of ergonomic linear Haskell to meet or exceed the performance of C/C++/Rust?

                                          1. 8

                                            Linear types do not suddenly turn Haskell into a language in which performance is easy to reason about. In particular, (a) it is still a lazy language, (b) it still does not allow you to control how much indirection is used in the representation of your data structures, (c) it still has features like polymorphic recursion, which restrict the compiler’s ability to monomorphize all types and get rid of the vtables in polymorphic code.

                                            1. 1

                                              Since you don’t seem to be someone who is interested in the language at all, I find it odd that you are responding here about completely different concerns that you have, that i’ll add, aren’t even related to the article topic.

                                              1. 2

                                                First of all, I only meant to reply to a specific question. I did not intend to do any of the following: (a) suggest Haskell is a bad language to use, (b) suggest any of the raised “issues” [if they could be called that] is a terribly big deal for most use cases, (c) hurt anyone’s feelings.

                                                Second, I am interested in all languages with substructural types. More precisely, I am interested in lightweight tools for algorithm verification, and there is a qualitative jump from what you can verify without substructural types, to what you can verify with them.

                                                1. 1


                                              2. 1

                                                Ahh, yeah, those are all still potential sources of performance problems. At the very least, this should be a good stepping stone and way to experiment with linear types. I’m excited to read more about it and play with it.

                                              3. 2

                                                I’m no expert but here is the original paper (2018)! https://doi.org/10.1145/3158093

                                                One of the performance applications is making read and write operations work on the bits of packed (serialized) ADTs. So it removes a need to have a decoded copy of that data via serialization/deserialization. They have a graph on how this improves summing and mapping over a binary tree.