> is Rust the motivating factor behind linear types cropping up lately?
Philip Wadler wrote "Linear Types Can Change the World!" while he was working on Haskell back in 1990. I vaguely remember there were some mentions of possibly adding it a year or two before Rust was publicly announced, but it seemed like it was going to be far off at the time. I wouldn't be surprised if Rust contributed to a lot of the interest in it - Simon Peyton Jones did specifically say that he had "Rust Envy" for shipping something similar to linear types in one of his talks.
You say "of course... I'd have to learn one or more flavors/styles of it", and that seems like a reasonable assumption, but it's not accurate in practice - the extensions largely just add features, so you just turn them on if you're using that feature; there's not much of a separate style for coding around not using one. It's like, if your Java project used a Singleton class, you might feel a need to document it, but if it doesn't, it doesn't mean you have a separate "Singleton-less" style, you just didn't feel the need to use one.
Which isn't to say they're not an issue - Haskell really needs a new language standard to clean up that mess, but they don't really fragment the ecosystem the way that, say, the Python 2 vs 3 split did.
To share more on where I'm coming from, one example: when I look at things like Yesod's "Hello world" section in "Getting Started", the first thing I see is 4 pragmas: https://www.yesodweb.com/book/basics and I just don't have much information on what those are, how commonly they're used[0], whether (and why) I need them to use Yesod, etc.
I have a kneejerk reaction to that since I want to be able to understand the code I'm seeing and I'm not sure what's going on behind the scenes. But kneejerk reactions are bad, so I'll give them the benefit of the doubt next time!
[0] Well, I definitely understand OverloadedStrings and TemplatHaskell to be very widely used, and think I get their gist.
TemplateHaskell and QuasiQuotes are very closely related. They're where that square bracket syntax comes from:
[whamlet|Hello World!|]
I would say that they're closer to the situation you're concerned about - they're very much like C++ templates, and equally controversial for exactly the same reasons. Still, I don't usually think of C++ templates, or Haskell ones, as being a different style per-se, just an advanced feature to use sparingly, mostly just when they'll save you from writing a bunch of boilerplate.
For completeness - Overloaded strings are the Haskell parallel to Python's b-string, f-string, u-string, etc. TypeFamilies are "let me write functions over types", which sounds like it would be dramatic enough to introduce a different coding style, but since it, like other extensions, needs to play nicely with the type inference, it doesn't conflict with other extensions, so things mostly just work as you'd expect. Since extensions generally work nicely together, most people just turn on "the usual" extensions for the whole project (all the more reason we need a new standard), and only add explicit pragmas in files to call out heavyweight things like TemplateHaskell. In tutorials you're more likely to see them all listed at the top, though, to be clear about what's being used.
Careful decisions can scale with abstractions, if they're made with some rigor.
In Python, for example, whenever I'm doing operations on lists, I need to consider every function in isolation - will this break for an empty list (zip), or will it break when given a generator (anything that traverses twice)? If I pass a callback with side effects, how will it behave differently if someone calls it twice?
In a a more rigorous ecosystem, I can instead only worry about edge cases on classes of functions/data types - In Haskell, when doing the same operations, I can generally assume that traversal functions were written with consideration for functor/foldable/traversable laws, and those laws tell me how I can safely compose or swap them out without breaking expectations around those edge cases. Higher Kinded Types let code be constrained to work strictly with those abstractions, so I mostly just need to worry about "does this typecheck" and, very rarely, "is this an unlawful traversal". With things like linear and dependent types entering this mix, library authors can communicate even more subtle expectations at compile time instead of leaving users to try to anticipate them or find them at runtime - when you do need to explicitly consider edge cases, the turnaround time on discovering them is important.
I don't disagree - these sorts of questions can be worked out to an academic degree with rigorous proofs. Databases and data guarantees around them are very widely applicable and have been isolated from business logic in modern applications due to the heavy complexity of that logic - once upon a time it was common for applications to "roll their own database" i.e. build some custom data storage approach that worked well enough (hopefully) for their purposes. I worked on a MUD based off a legacy that began in the 80s that used flat-file storage as a primary data storage method and race conditions abounded.
However, databases are cost effective to build and distribute, but implementing that level of rigorous proofs for your e-commerce app is not only generally undesired but often increases the difficulty in reaching profitability and can sink a company. Working on system development isn't limited to academic concerns, if you're guiding project development you have to make really hard calls about correctness vs. cost and I say this as someone who likes to be a perfection and do things the right way whenever possible.
So I don't disagree that careful decisions can scale with abstractions - it isn't the case that it is impossible to build a well designed large system, but it will be expensive and at the end of the day we all (probably?) need to balance cost of investment vs. value of that investment - or are having someone higher up the chain making that decision for us.
I think learning to program for correctness has a cost, but it's a skill that stays with you. Once you know how to properly model things in a composable way you can definitely work just as fast or even faster as when you gave no care for correctness. And frankly, shipping an incorrect program isn't really necessarily a worthy tradeoff as you are simply deferring problems to the user or to later down the line. And you don't need rigorous proofs to enjoy the correctness protections from strongly typed languages like Haskell. The language does that for you, you just have to learn to model in them which is a one time thing.
I didn't need an academic degree to start working in Haskell and learn abstractions such as "Traversal" or any of the others. Most of them are painfully simple compared to the impression one gets from their names and the jargon that comes with the territory.
However the benefits of sticking with those names and jargon is that it only needs to be explained once. Analogies and metaphors help when you're starting out but you don't need to keep them around. It makes speaking precisely with colleagues in the ecosystem easier.
Proofs are on another level. I've also written proofs and they require much more rigor than you will find in Haskell. It can still be done without a degree but I agree -- not useful for most line-of-business applications.
However the power-to-weight ratio of learning the abstractions available in Haskell is smooth. It takes effort to acquire but it pays off in spades. That's where the "scale" comes from.
Polymorphism combined with composition means that once I know a type implements "Traversal" I can use the entire language of traversals with those data types without knowing anything else about the value I'm working with. The more things that implement traversal the more rich my program becomes.
You do get this idea of composition in the form of generics or template metaprogramming, not lost on me there. Type classes in Haskell, in my humble opinion, are better at consistency, keeping things coherent, and requiring less nominal boilerplate.
There are significant advantages to having the entire Nixpkgs package set in a mono repository. While I think Flakes are quite interesting for a number of reasons, I hope it doesn't result in the primary package set getting split up too much. They conceptually act a lot like Git submodules, and going overboard with that is a very easy way to make your life miserable, and significantly increase development turnaround for changes that "cross" package sets. A group of packages just being "conceptually related" isn't a high enough bar to move things out.
As a long time contributor, I'd much, much rather see our bug reporting, triage, and discovery/resolution strategies improve first -- long before going as far as splitting up the mono-repository. That's the part that's frustrating for users (their reports get lost, forgotten, duplicated) -- not the fact the default set merely has a lot of packages.
I think at very least (and easy to implement) nix needs a bot that closes old tickets. The number of open issues is ridiculous and basically it makes easier for an issue to be overlooked and further increase the count. The number of open issues also causes some people think nix is very buggy and not suitable in production or even exploring.
There are probably some people who see a 3k bug report number and think that, but realistically tons of projects have thousands of open tickets for any number of things from legitimate bugs to duplicates to actual user questions. Linux, projects like LLVM, etc. It's natural when you have a project that is in active every-day use by literally thousands and thousands of people. Nixpkgs is simply a big project! But the actual numbers might tell another story.
For reference, the LLVM bug tracker has exactly ten thousand open bugs as of this writing, and I assume that number is only so perfectly rounded because Bugzilla search refuses to return any more results in a single page that already brings scrolling in Chrome to its knees. You won't find any lack of praise for LLVM's high quality and extensible nature, though -- they can all be true at once!
The nixpkgs label tracker isn't highly accurate since auto-labeling only started earlier as of this year, but as of this writing, of the 3k open issues, about 500 of them are directly marked as bugs, while 41 are marked as regressions. There are 200 enhancement requests, and 50 open packaging requests. So of 3,300 bugs, about 800 can be quickly classified, and about half of those are actual bugs. This is a very ballpark number (GitHub search doesn't allow XOR). Considering nixpkgs is literally shipping thousands of other software projects, I think this is pretty good -- even though I wouldn't argue it could be cleanly extrapolated to the whole set of bugs, because of a long tail of old bugs.
In terms of cadence, over the last month there were ~466 new PRs, and ~1,600 merged PRs. ~220 closed issues vs 215 new ones. This is done by nearly 350 contributors. I would think this is also very good and the sign of a healthy project with hundreds of active developers. IMO, if just a raw number of "3,000 open github issues" has to mean anything ("this software is unstable"), then these numbers have to mean something too. It's just that GitHub doesn't "helpfully" post them on every single page concerning your project...
But I do agree we should have better mechanisms for discovery and keeping things clean. Duplicates certainly happen and are annoying, and nobody likes drudging through 1,000 of the oldest open reports to close old stuff, etc. Some of this is also limited by GitHub and other things, unfortunately.
Personally as a developer (not a user!), I think bots that close old tickets are often very annoying (to everyone) and rarely do much other than feed a human desire to hit "inbox zero", but this desire is not (to my knowledge) based on any actual scientific criteria that leads to better software development or happier, better cared for users. It is more a way of externalizing a deep human desire for "cleanliness" and using it as a yardstick for "quality" rather than evaluating the numbers for yourself. You can also find tons of 0-issue repositories on GitHub, but this doesn't mean they're actually good, or they do what you want -- and I doubt most of them have as much momentum as we do.
There are, that was response from one of my colleague after mentioning Nix to him. Having 3k open bugs, don't help with anything there's no way all of them will ever be addressed and important ones could get lost between them.
I don't think closing such bugs is "feed a human desire to hit "inbox zero"" even with that you'll never get there. From my perspective it is all about not losing track of important issues. Having bots close tickets makes sure that only tickets are opened are ones that someone cares about. There are tickets that are from 2013, a lot changed since then, they might no longer be relevant anymore.
I personally hate it when a bot closes an issue I wrote. What's the point of closing unresolved issues? Just assign them a label (it could be a "stale" label like some projects do). Otherwise it just feels like hiding your mess under the bed. Other sorting tools can provide the same list as automatically closing bugs would achieve. The opposite isn't true, unless assigning a specific label when manually closing an issue.
SAT solvers are starting to be used as tooling for functional languages - Liquid Haskell uses one for refinement types[1], and Djinn uses one for suggesting functions given a type[2]. Similarly to Djinn, Edwin Brady gave a presentation on using an SMT solver to do live code suggestions/implementation inference in the successor to Idris[3].
I've worked in Elm a decent bit, and used PureScript a little.
Elm is a very opinionated language - it's very deliberately missing some abstraction power (typeclasses), and some functions that are the bread-and-butter of every functional programmer have steadily been getting removed from the base libraries, so if you're used to Haskell, you'll find yourself falling back to duplicating code by hand a lot. Elm also makes certain stylistic choices into parse errors - "where" clauses are strictly forbidden, and indentation preferences are strictly enforced. It's basically taken an awkward edge-case from Haskell's indentation rules and made it not only a requirement, but a prerequisite to seeing if there are any other errors in your program. The back-and-forth trying to get the compiler to accept things that would just work in Haskell, but don't because of someone's stylistic preferences, is absolutely maddening.
PureScript, from the bit I've used it, is like a strict version of Haskell with row polymorphism, a feature Haskellers have been hoping for for a while. I've chosen Elm over PureScript in the past because of PureScript's dependency on Bower (which I think has changed since then), but that's the only reason.
> indentation preferences are strictly enforced. It's basically taken an awkward edge-case from Haskell's indentation rules and made it not only a requirement, but a prerequisite to seeing if there are any other errors in your program.
Some parsing is less efficient than Haskell because Elm doesn't have 20+ years of PhDs working on it, but there is no such thing as compiler-enforced formatting. I can't think of compiler errors regarding format that are the expression of a choice, as you put it, rather than the expression of less manpower.
Likewise, `where` clauses aren't forbidden, they are simply not implemented, which, given that you can already use `let.. in`, is not especially shocking.
The omission of where clauses was explicitly a stylistic choice[1].
This is perfectly valid Haskell:
#!/usr/bin/env stack
{- stack script --resolver lts-12.19 -}
data Test = Test {count :: Int}
test = let
something = Test {
count = 5
}
in 5+(count something)
main = putStrLn $ show test
To get the equivalent Elm to compile, it must be indented like this:
test = let
something = {
count = 5
}
in 5+(something.count)
Note that `something` must be indented beyond the beginning of `let`, and the closing curly brace must be indented to the same level as `count`. These are both not a warning, but a parse error - you can confirm it with Ellie[2]. If that were due to a lack of resources, it would absolutely be understandable, but this also was an explicit choice[3] which developer time was spent implementing.
While there was nothing particularly wrong with bower for PureScript use case, it's always failed to attract people for that reason sadly. However, you can use Spago now to great success.
This is a really arrogant statement. In C, `if(a = b)` could cause incredibly subtle bugs. It was prominent enough that it got addressed in all the best practices books, like "Writing Solid Code", with a style that got later termed "yoda conditions" - a style that was prominent in spite of being acknowledged as less readable, because it forced a compiler error more often. It's hard to even think of many other types of bug with that kind of significance, and you just dismissed it out of hand with "I don't make those kinds of mistakes".
Well, that's pretty much equivalent to the the language preventing bugs, for the purpose of the conversation. You can imagine similar cases that would be harder for a linter to pick up. Things like type errors, or accessing the wrong side of a union - in C++ people used Hungarian Notation for a good while to try to make these kind of errors more detectable; now some languages have tagged unions/sum types to make them nearly impossible. The point where a linter is distinct from the language in catching syntactically evident errors is that, even if I use a linter for my own code, that isn't the same as having buy-in from the whole team to block any code that doesn't pass the linter from shipping to production; language syntax, on the other hand, is implicitly agreed upon.
Addressing this specific example, historically, running a linter all the time wasn't always practical, and `if(a = b)` was used intentionally a lot, e.g. to inline a check for a null pointer with an assignment.
To be fair, they only elected the conservative party, the LDP; the party elected the prime minister. Granted, they've elected the LDP almost continuously since 1955. Of course, they tried electing the other party in 2009, but their leadership kept resigning. Of course, given the LDP's stranglehold on politics, one has to wonder why they feel a need to pander to the nettouyo.
I stopped paying to attention to politics about 5 years ago and am very surprised to learn that the major opposition party (DPJ?) has essentially fractured into multiple, smaller parties, all using a variation of the same name.
At this point, I'm not even sure who to vote for anymore.
Haskell has a few libraries that do this[1]. Not trying to one-up the article or anything, just thought you might be interested to see that there are other places where this is available, and that it's not even something that needs full language support in some cases, just a library. Also similar - you can pretty transparently model nondeterminism[2] and probability[3] on a "promise"-like interface with just a library. Of course, whether or not there's good documentation is another story.
Philip Wadler wrote "Linear Types Can Change the World!" while he was working on Haskell back in 1990. I vaguely remember there were some mentions of possibly adding it a year or two before Rust was publicly announced, but it seemed like it was going to be far off at the time. I wouldn't be surprised if Rust contributed to a lot of the interest in it - Simon Peyton Jones did specifically say that he had "Rust Envy" for shipping something similar to linear types in one of his talks.
Linear Types can Change the World!: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5...