1. 49

    1. 19

      I’m always slightly surprised when I meet people who actually use Haskell. I consider it one of the languages like Smalltalk or Prolog that you should primarily learn because if makes you a better programmer in any language, not because you should actually use them (Erlang is almost in that category, but there are some places where it would definitely be my go-to choice).

      1. 25

        I’ve been using Haskell professionally for about a decade, I’m currently in my first job since uni where I’m not using it for production systems. There are few languages that all you to build as maintainable systems as Haskell. Yes there is a shallow learning curve (steep learning curves mean you learn a lot quickly), but the payoff is being able to produce systems which you can change drastically and have machine checked help with the compiler having your back constantly.

        I’ve used it for processing medium data on AWS with a fairly AWS specific pipeline of services, and during my time we rearchitected the fundamentals of the how the app ran twice, from a single monolithic containerised app, to splitting it into microservices, to using AWS Lambda, all in the same code base, without any bugs in business logic throughout. We knew that we could make the change we thought we needed to make, and then follow the errors until it compiled again (I couldn’t tell you how long it took, as there was obviously a lot of concurrent deployment changes, but the Haskell side was generally done is one, maybe two two-week sprints).

        We also did all this while much of the tooling we today didn’t exist, or was in its infancy; HLS is an amazing productivity booster that I wish I’d had over much of the past decade. There are warts, yes, but things have massively improved, and all of that without having the dedicated teams and financial backing other languages like Go and Rust have had behind them. Most of these tools have no more than a handful of people contributing to them, and are achieving great results.

        It makes for an amazing language where concurrency matters, its threading is as cheaper or cheaper than Erlang’s, and immutable by default with very explicit mutation where needed means your business logic can be clearly expressed without fear that you’ve forgotten some state - the data you have is all you need to produce the results. Performance is also excellent; it might not be C, C++ or Rust fast, but it’s in the ballpark, and the much nicer concurrency story than those three makes up for it for me, when you’re building production systems.

        Haskell’s type system is IMO its number one asset, and I disagree when people say you should only stick to the simplest types so it’s easier for others to learn. People can be taught, and we’re doing engineering, not playing with lego. Most other languages feel to me like building bridges by putting stones and logs on top of each other, Rust has figured out that you can bind them together with lime, where Haskell has moved onto using timber trusses. We haven’t as an industry figured out how to do engineering to the level of building trusses and cables from steel, and we’re a long way from finite element analysis to model out software-bridges, but Haskell gets us moving in the right direction. Engineering is all about building things which are predictable, model-able, and Haskell’s type system gives us a glimpse of that, by letting you make illegal states unrepresentable, and allowing us to precisely define what cannot be done, not just what can.

        It’s always struck me as bizarre that we expect professional programming to just be easy for everyone - anyone can buy an Arduino and make it do some stuff, but I want the people designing the power grid, my motherboard, and the avionics systems in planes to meet a significantly higher standard of rigour; why don’t we expect the same from professional software engineering?

        Haskell’s benefits can feel tedious in the small, but I have witnessed them absolutely pay off in the large. One aspect of the community is that we don’t tend to boast too much about it; why should we, we’re just getting the job done, we’re not trying to start a cult like some members of other language communities seem hell bent on. Facebook is processing millions of requests per second in Haskell to filter spam, and having non-programmers write that Haskell; banks around the world are internally building large systems in Haskell, and have been doing so many years at this point; NASA are using it for hard real-time monitoring of high assurance systems, and ESA are using a derivative (Clash) to design the hardware for terabit space communications laser systems. To name just a few.

        I could go on much longer, but as has been the case for the past 15 years, the rumours of Haskell’s death have been greatly exaggerated yet again. It is still worth learning, it is still worth building real systems in, and is only getting better at doing it as time goes on.

        1. 18

          It’s always struck me as bizarre that we expect professional programming to just be easy for everyone - anyone can buy an Arduino and make it do some stuff, but I want the people designing the power grid, my motherboard, and the avionics systems in planes to meet a significantly higher standard of rigour; why don’t we expect the same from professional software engineering?

          I couldn’t agree more. I’m flabbergasted by the obsession with simplicity, and unwillingness to learn in our industry. I can’t believe the success of Go. To me, it is a terrible language, working with it would be a nightmare, and yet people love it for “basically being ifs and loops”. Zig is coming up hot because it’s mostly C. How can you have this job be that unwilling to learn?

          Sorry for the rant comment, but that stuck with me since forever.

          1. 5

            I couldn’t disagree more :-) I love learning new languages but there are a lots of advantages to simplicity besides being easier for novices to pick up. In my job I have to go in unfamiliar codebases all the time and edit other people’s code, and that’s a lot easier when the language stops them from being too clever. Even in my own projects, fancier languages make me feel taxed trying to decide what’s the right way to do something instead of focusing on the problem at hand. In Rust, I see long discussions all the time where someone has code that already works, but they want to compact it down to an ideal form using just the right combinators. That rarely happens with Go because you “just write a loop” and move on, saving all that mental energy. I’m not necessarily saying I prefer Go over Rust all the time, but I do in this respect. You could just write boring loops in Rust too, but it matters what the language and community shepherd you to do.

            Also, I want to defend Zig! I’ve been learning it recently and really enjoying it. The fact that it’s “mostly C” is a killer feature that lets you integrate it with any existing C/C++ project or libraries. It has several innovations which fix many of C’s problems while avoiding C++ level complexity. It takes a fresh approach to memory allocation which is worth checking out for any systems programmer “willing to learn”.

            1. 6

              The thing is, I don’t actually have a problem with Go and Zig. I don’t want to use them, but that doesn’t mean I want to see them fail. What annoys me so much, is that they are successful, while other languages that I like are not. I really like Haskell, and I’m not really using it, mostly for the reasons detailed in OP’s post (although, for me, the ecosystem is the largest problem). But all those downsides are the consequence of a small community. I’m angry because these communities are so small, while Go is big, and Zig will probably become big.

              Having C-compatibility is certainly extremely useful, but you can link C-libraries in Rust too. There is a big margin between “just loops and ifs” and “too clever”. I think Haskell without most compiler extensions has a pretty reasonable level of complexity. Sure, GADT are over the top, but there is a hell of a lot of potential over Go before it becomes too clever. Give me ADT, generics and a great Macro system. Rust is close, but I think it’s still too verbose, has way too many iter() calls everywhere, no HKTs, and function signatures tend to be terrible with non-trivial generic code. Also, rust proc macros are too much effort, closures and async also have a lot of problems. I would love to have Rust with these things fixed. I don’t think that would be too complicated. But it won’t happen, because too many people already think Rust is too complicated. And THAT is what tilts me.

            2. 4

              Coming into someone else’s code is exactly when you want these features - you have absolutely no idea what the constraints and invariants on the system are, and in a language like Go, you probably never will. In Rust or Haskell, it is at least possible to teach the compiler what should be disallowed by new developers. People look at Python or JavaScript and think they’re simple, but they’re exponentially more complex than strongly typed languages because the state space of any piece of code is actually infinite. This makes it genuinely impossible to make changes and be certain you’ve made the correct changes.

              Prioritising writing your first code is a fundamentally flawed idea for a business that expects to be developing for a long time. Optimising for the ability to make changes without breaking things. “Move fast and break things” only needs to exist when you can’t avoid breaking things, and that is the case in a lot of the YOLOLangs we see today - but powerful type systems are finally taking their rightful place with languages like Rust, Typescript becoming popular and learning from the lessons Haskell has been teaching for decades.

          2. 1

            Industrial programming means that most of your fellow programmers will be non-seniors. What kind of language do you want to give them: Go or Rust?

            1. 3

              If I prioritize productivity, getting things done fast, I’d say Go. If I prioritize correctness, getting things done ‘right’ (contra Worse is Better), I’d say Rust, which I imagine would protect better from the mistakes that the programmers will make. Because I prioritize correctness and have very unimpressive productivity, I imagine I would be fired and never get to make that decision. :-)

              1. 2

                What’s that they said? “I can be very fast if I can be wrong some of the time.”

            2. 2

              If you ask like that: I want to give them Rust, Ocaml, and Haskell … and Raku, and I want them to learn it. I’m aware that that’s not gonna happen

              1. 1

                We’re talking about real humans here so no 100% that’s not going to happen. Though I think as a tech lead I could drag a small team through the onboarding curve with Rust. Just remember: .clone() is your friend.

      2. 13

        I’m the other way around; I think that Haskell memes are misleading at best and damaging at worst, but Haskell itself seems like a reasonable language. It’s one of the few popular languages to not be set-oriented, using DCPO instead of Set for its collection of types.

          1. 2

            Yeah. Haskell’s semantics are not necessarily categorical, but if they were, then they seem to fit well with CPOs of some sort. To me, this alone is quite enough to merit study.

      3. 16

        I can assure you Haskell has its place as a go-to language. I’ve used it professionally and for fun for 8 years now and it’s great for fleshing out (and keeping up to date) complex data domains, be it the core of a SaaS backend or a compiler. Not to mention its concurrency story (e.g. the stm library) which is pure magic.

      4. 5

        It was my default for a while, because at the time (2007 or so?) it was the best safe language to write Unix daemons in. It also had the best C FFI of any of the mature languages at the time.

        I still use Hakyll for my website, but I don’t write it much anymore besides that. I don’t write much code outside work at all these days.

      5. 4

        I’m always slightly surprised when I meet people who actually use Haskell.

        gwern uses Haskell to build his website.

        1. 3

          Hmm. That’s a cool and weird website! It really makes my PC chug tho, and it has some unpleasant reflow issues.

          1. 2

            It’s a static site, the chugging is not on Haskell. Apparently the pages are just huge infodumps.

          2. 1

            There’s a lot of JavaScript powering the tooltips.

      6. 3

        I read Learn You a Haskell and thought it was a pretty cool language. So I was excited to try it out, but once I took a good look at the ecosystem and tooling around the language I was so put off I just couldn’t bring myself to continue. I’m really glad I read the book though.

      7. 1

        We almost exclusively use Haskell at bitnomial. We’re a CFTC-regulated futures/options exchange. We’re able to build amazingly reliable distributed systems at scale with a pretty small team. It’s definitely not the best choice for everyone, but it’s worked phenomenally for us. Complex distributed systems with lots of concurrency and millions of dollars riding on us getting the logic right are made tractable with Haskell.

      8. 1

        I’m a noob on both of those languages, but when would you choose Erlang over Elixir?

        1. 4

          Not OP. But I know people that would use Erlang and, given the choice, not write Elixir at all.

          Personally I tend to write my libraries in Erlang and applications in Elixir. The main reason for this is that it is harder to use Elixir code from an Erlang application, but super simple to use Erlang code in an Elixir application. Obviously this does not work all the time. For example, if I was writing an Ecto adapter, I would write it in Elixir.

          1. 1

            I think rebar_mix makes it fairly easy to call into Elixir packages from Erlang.

            1. 1

              I do not know the current status of it, but I know there were issues with the process at one point. It is also less ideal actually calling Elixir code from Erlang. A normal Erlang function call would look like


              Whereas calling an Elixir function from Erlang is


              And then the opposite, calling an Elixir function from Elixir,


              And an Erlang function from Elixir,


              And that is only calling functions. There are other differences that you would need to be aware of as well which makes calling between languages less ergonomic than is ideal.

        2. 3

          I’ve never used Elixir. I am one of the three people in the world who like Prolog and so Elixir’s move away from Prolog-like syntax isn’t a selling point for me. Last time I looked at Elixir, they had made some things better and some worse in my highly subjective judgement.

    2. 15

      One point I think needs more emphasis is that Haskell gives you more tools to write cool, but inscrutable code than other languages - and it’s not just the bleeding-edge stuff like type families. Even simpler abstractions that Haskell ships with natively (which can be done in other languages too, they just don’t have them) can be used.

      OP used pairwiseMultiply as an example of Haskell’s strengths - to build off of this, here is an example of where I think Haskell’s tools permit the unrestrained programmer to confuse and astound. [1]

      adjacentSums = zipWith (+) <*> tail

      Don’t get me wrong, confusing code is not just a Haskell problem. You could get carried away with writing classes and factories in Java, you could import or define the same abstractions in JS, you could write APL.

      It’s just that many abstractions in Haskell are - dare I say - fun. It’s so tempting to write foldMap (First . tryAction) <=< makeThing or import from Control.Arrow. But then you come across code you wrote four years ago and have to scrutinize every line to figure out why this terse mess works - or worse, why it doesn’t.

      I think there is something to be said for code that knows how to be just verbose enough so that you can skim and understand why it works without wracking your brain or following a trail of types. The problem with most other languages is that they don’t have enough of Haskell’s abstractions - the problem with (some) Haskell is that it has too much.

      [1] OK so maybe I’m being glib by using the reader monad or making a strawman out of pointfree code. Try not to get caught up too much by this particular example.

    3. 12

      I came to Haskell having struggled mightily with Object Oriented code, in things like C++, Java, Ruby and the like.

      The thing I appreciated was that I could look at the code in front of me, and take it for what it was, without having to mentally calculate what was actually happening when a particular call happened, or whatnot.

      This meant I could draw a mental boundary around a given function, and when looking inside, I only needed what was inside to understand it.

      And as has been pointed out, the temptation to add more and more fancy type stuff takes us back to not being able to easily understand the code, because you have to mentally simulate the operation of the type checker to know what a given thing is. And to my mind this goes back to the horrors of inscrutable OO code.

      My 2c, probably off topic.

      1. 2

        To me “understanding in isolation” is an underrated goal, as its not strictly possible.

        What you can argue is “understanding semantics in isolation”, as in, i can glue together some api calls together without reading the docs much and hey itll run. But that doesn’t mean itll do exactly what you want it to do & no less.

        Its useful definitely, but it’s just half the picture (or less).

        The bigger point to me is exploitability of libraries, tell me how you implement it, not just what your api is. REPLs help a ton with this, LSP helps a ton especially if the type system is meaningfully descriptive. And probably most importantly how common will it be given the language/framework ecosystem can i go in their source and see easy to follow idiomatic code which i already know.

        Ime the best language for exploitability so far has been elm, second ime is ruby - i can tear things apart and see how it behaves with reasonable certainty

    4. 11

      This hits close to home for me, especially this part:

      And on various occasions, I’ve replaced complicatedly-typed abstractions with much simplified versions, only to see subsequent programmers notice the lack of fancy types5 and try to replace those simple abstractions with various kinds of cutting-edge type-level abstractions, only to see the code blow up in size, drop in performance, and lose much of its readability.

      It’s not the only language where this happens, but it’s especially prone to it. Killed all motivation for me a few times.

      1. 9

        To me it’s basically a “slippery slope” problem with static type systems. Similar issue here:


        Much of the OCaml I see in the wild is a mess of un-annotated, deeply-nested, functorized code that’s been PPX’d to death

        With dynamic types – programming and metaprogramming are done in the same language. Types are values.

        With static types, basic problems are convenient to express in the “basic language”. But then when you hit a more complex problem – or not even that, basic printing/serialization is enough to trigger it-[1] - there’s a temptation to ESCAPE into another language.

        That could be a macro language for syntactic abstraction, or more sophisticated type abstraction with something like GADTs. The base language seems like it’s “not enough” for some reason.

        Of course you don’t have to do that – you can use some runtime assertions in your statically typed program. But it seems to be a big temptation.

        [1] I didn’t read this whole Serde thread, but it sure smells a lot like a lot of protobuf problems I’ve seen. Static types and printing things is hard :) https://lobste.rs/s/80lw9s/serde_has_started_shipping_precompiled

    5. 8

      Thanks for the well written and informative article.

      Haskell has always occupied a weird niche in the constellation of programming languages. On one hand we have the siren’s song of programs that are correct by construction. Where if it compiles it works. People also make good arguments that with Haskell you can basically write the most elegant high level mathematical code and the sufficiently smart runtime will make it faster than c with things like loop fusion. I certainly believe that we do a poor job overall of utilizing typing to tell the compiler to automatically verify our code for us.

      At the same time my anecdotal experience with Haskell practitioners is best summed up by a story. Years ago I interviewed a very smart person. They chose to do their interview in Haskell. I don’t even remember the problem but we quickly started discussing some basic big O memory/runtime questions along with production concerns like “how much memory would this use?”. The answer: “I don’t know. Could be horrible. Could be awesome. I don’t know what’s going on with the thunks”. Followed shortly by: “The thing I love about Haskell is that no matter what I try to do, it’s like a research problem I could spend months on!”

      I guess it comes down to: Haskell gives us some tools to write better software, but the community is (from my pov) plagued by a lack of pragmatism. I have no doubt people can build great product & platforms on it. I’ve heard of a few. But with my current knowledge I don’t think I’d pick it for any tool. If I wanted to up my level of formalness I’d start with something like Rust. Also as of late I’d mix in tools like dafny (or the more well known TLA+) to write formally verified models/kernels. https://dafny.org/

      In fact most formal/provably correct industry software that I run into day to day is probably the various tools on AWS modeled in TLA+ or the work microsoft has done in that space.

    6. 5

      Absolutely tangential, but I think I’d write the Ruby example as

      flavors.product(containers, toppings).map do |flavor, container, topping|
        "a #{container} of #{flavor} ice cream with #{topping} on top"

      (But the Haskell example is still better, IMO)

      1. 1

        Some code golfing - actually made it read worse, but oh well!

        containers.product(flavors, toppings).map do
          "a %s of %s ice cream with %s on top" % _1
    7. 4

      I want everyone to learn haskell* because I run into way too many ad-hoc specs/documents for file formats, protocols, and data structures where a recursive sum-of-products type would succinctly tell the whole story.

      I think it took me 18 months to learn Haskell (while mostly doing project management and python) I couldn’t parse the whitespace when I first tried. Then I learned scala a few months later, and then a few months after that I could read haskell. Now I think in haskell** regardless of what I’m writing in.

      And I look back in horror at the docs and specs I wrote before I grokked Haskell.

      • or ocaml or scala. Maybe rust would do. Or ML I suppose, but I have no direct experience.

      ** and E

    8. 4

      I have a pile of issues with Haskell, many of which overlap the problems listed in this post, that said the post also doesn’t seem to end up with a point.

      But the post also starts off with a bunch of “benefits” of haskell that it grossly misrepresents. Yes haskell can be brief, but a lot of that is purely cosmetic: abbreviated names, gross misuse of operator overloading, etc (the wanton abuse of operators in haskell seems to be designed specifically for the purpose of minimizing code typed, rather than for actual value). The post then chooses a tremendously unreasonable example of how “concise” haskell is:

      pairwiseProduct = zipWith (*)

      This is a classic “look how concise haskell is” example which, alongside numerous others, uses an operator as a function. This is drastically overselling the conciseness advantage of haskell vs other languages. Yes there are code golf examples where you are using solely an operator as a function, but in the vast majority of cases you are using a named function, and then the win reduces to currying. Once you’re there the key press savings are reduced significantly. Even C supports passing named functions, C++ and all the modern static and dynamic languages support functions with attached context.

      But beyond some particularly gratuitous cases (Java’s massive boilerplate, etc) the majority of “verbosity” in other languages comes from stylistic choices: most code written in production environments is written to be readable, and that means variable and method names aren’t single characters. Similarly in real world code doing lots of unrelated things in a single line or expression is likely to be considered “bad code”, but in haskell it’s considered “good”. Cynically this is because Haskell puts so much undue weight on the cost of keypresses.

      Any code you ever write, is going to be eventually read more often than once, and so is being read more often than it is written. Programming languages should be optimized for readability, not keypresses, and if your language is still using optimization of keypresses as one of the first and most frequently repeated advantages, you need to stop.

      1. 2

        the wanton abuse of operators in haskell seems to be designed specifically for the purpose of minimizing code typed, rather than for actual value

        I would take a more charitable view and speculate that — like the cryptically short variable names — it comes from the influence of mathematics, in which it’s normal to use non-mnemonic¹ symbols for many operations/functions.

        ¹ by which I mean ones that don’t suggest their own meanings, unlike an alphanumeric identifier chosen to be “self-documenting”

    9. 3

      The worst part is that the three broad issues here interact multiplicatively, especially the combination of awkward tooling and breaking changes and breaking changes in the awkward tooling, and so on. I think a big problem is that a lot of the language’s biggest luminaries don’t fully understand or refuse to acknowledge their situation. They work in industry and not academia, and the assertion that Haskell is a practical language only requires an existence proof, and so their job existing is a witness to that proof. They downplay the impact of breaking changes in the standard library because they nominally use Haskell in a practical fashion and it wasn’t a big deal for them, not realizing that their job position is basically the equivalent of an auto manufacturer’s performance division: largely existing to bolster brand prestige and maybe, with luck, generating ideas or techniques that can be profitably applied in the consumer division. At least, that’s the only explanation I can think of that accounts for how much time they seem to be able to devote to bikeshedding on very subtle matters of code correctness in a way I’ve never seen be possible even in the most speculative of industry projects. It’s a bummer, because it’s fine if Haskell’s goal continues to be to avoid success at all costs (although if so there’s a real niche to be filled by the sort of language that Simple Haskell advocates are going for), but a lot of the most visible language advocates aren’t willing to admit that that’s still the situation because all the practical road bumps don’t actually affect them. Bummer.

    10. 3

      Oh I just wrote a comment about this [1]. It’s hard for me to reconcile these two parts:

      A good concrete example here is a compiler project I was involved in where our first implementation had AST nodes which used a type parameter to represent their expression types: in effect, this made it impossible to produce a syntax tree with a type error, because if we attempted this, our compiler itself wouldn’t compile. This approach did catch a few bugs as we were first writing the compiler! It also made many optimization passes into labyrinthine messes whenever they didn’t strictly adhere to the typing discipline that we wanted: masses of casts and lots of work attempting to appease the compiler for what should have been simple rewrites. In that project, we eventually removed the type parameter from the AST

      which seems to conflict with this:

      Using data structures indexed by compiler phase is a good example of a “fancy type-level feature” that I’ve found remarkably useful in the past.

      This links to “trees that grow” - https://www.microsoft.com/en-us/research/uploads/prod/2016/11/trees-that-grow.pdf

      Or maybe the author is just saying the parameterizing ASTs by type is useful in some cases but isn’t in other cases.

      Actually the toy codebase I hacked on was matklad’s TypeScript example with Expr<void> and Expr<Type>:


      (I did find TypeScript/Deno to be surprisingly pleasant. Among other things, the flexible union types can express “first class variants” like I do with Zephyr ASDL in https://www.oilshell.org/, which Rust can’t do, and OCaml seemingly needs GADTs [2] for - https://dev.realworldocaml.org/gadts.html )

      Anyway, I changed the representation to a Map<Expr, Type>, similar to how MyPy and Go do it internally, and it seems simpler and more flexible.

      It’s less type safe, but I think you have exactly the problem mentioned above – you don’t know until after you write the compiler if you need that type guarantee! (and I don’t think it’s a very strong guarantee – I think there are many crucial properties / invariants on IRs that you can’t really encode in the type system)

      It seems useful to be able to get the types of nodes even when the entire program didn’t type check.

      And it’s a pretty big change – it’s basically rewriting every line of the compiler if you want to change it later. So I kinda lean toward the simple solution, but I think opinions are mixed.

      On the other hand I do know I want the first class variants, e.g. because Bool | Int | ... can travel through at least 2 different IRs, for location info, etc.

      (and I’m still learning, which is why I bring it up)

      [1] https://news.ycombinator.com/item?id=37249247

      [2] This post references a tweet - The road to hell is paved with well-intentioned GADT usage, and even Real World OCaml says the power comes at a cost.

      1. 1

        FWIW someone answered my question here - https://news.ycombinator.com/item?id=37251385

        I was mixing up 2 different things – the issue of adding data across stages, and trying to express the target language type system in the host language type system.

        The latter idea seems weird to me, and it seems unsurprising that it falls down, since the 2 languages are in general unrelated. Though I did notice the duplication problem it’s trying to solve.

        1. 4

          I’ll post the reply I started to prepare anyway:

          I think the similarities between “Trees that Grow” and intrinsically typed ASTs is pretty shallow. As you say, they both parameterize types for ASTs, but I think it stops there. The role of the parameter is different:

          • For intrinsically typed AST, it restricts the underlying AST. You’re coupling the AST with type inference rules of the object language; you’re really starting to represent valid typing trees, not arbitrary syntax trees. You’ve committed to a type theory approach for understanding the language you’re compiling.
          • For “Trees that Grow”, it does not restrict the underlying AST. You’re restricting the AST to a certain compiler phase (ie. which metadata is carried along inside the AST). You have not committed to any kind of type theory or typing approach.

          When you the write a function transforming a “Tree that Grow”-AST, your “proof obligation” (what you need to convince the type-checker of) is that you are in a certain compiler-phase or between two phases. The phase (or phases) usually remain static (or simply parametric) throughout the function. This is usually so trivial that even thinking of is as “proving” is not very helpful.

          When you write a function transforming intrinsically typed ATS, your “proof obligation” is that the AST remains well-typed in the object language. Your code is essentially a provably correct construction of a valid typing tree, constructed by non-trivial structural induction proof over typing trees. The proving needs to happen in the language of your compiler. And you might, for the first time, wish to have paid more attention to that programming language theory class. But even more likely, you might wish, as the author, that you didn’t go for this approach ;)

          1. 1

            Oh yeah, they’re not similar at all! I just wasn’t familiar with the first part, and had problems reading it.

            But now I sorta get it, except same question as on my reply HN:

            Why not lower into a more strongly typed IR? That seems like the obvious solution.

            Again the first technique seems like a confusion of the target language and the host language, which in general aren’t the same. It would never occur to me to try that. I would be surprised if any production compiler does it. It’s also not surprising to me that it’s slow, because I have a lot of trouble imagining what a compiler can do with that sort of program.

            1. 1

              I’m familiar with this technique from proving properties about programing languages in proof assistants. So I assume people who use this for compilers want (some of) the same kinds of guarantees for their optimization pipeline.

              There is a certain elegance to it. You have an optimization step where you have written a recursive function on the structure of the AST, and then justify some correctness property with an inductive proof over the structure of the same AST. The proof follows the structure of the program. In a language like Agda, there is no difference in what you’re doing with your program and your proof, so you can remove duplication. And you don’t have to consider impossible cases either.

              It’s also not surprising to me that it’s slow, …

              It’s also collapsing the implementation of an optimization step and the proof of it’s correctness to one program. So you might have to use a slower algorithm than needed, because while the faster program might be correct, it is not simultaneously a proof of correctness from the perspective of the host language.

              I think there is a famous theorem related to this, but its name escape me.

              Why not lower into a more strongly typed IR?

              Personally, I consider ASTs to be IRs. And we are talking about a fairly “strongly typed” AST/IR here. I don’t think going to a lower-level IR gives you any new tools at your disposal for guaranteeing the kinds of properties people are after here.

              I would be surprised if any production compiler does it.

              Me too. I don’t think it’s used by CompCert either.

    11. 2

      Extensions? Never could really figure out what those were or how to use them.

      I tried doing some stuff in Haskell but with basic documentation it’s not really obvious how to do something non-trivial with it and I didn’t have the stomach or need to push much further into it. Then I switched to Clojure which was much much better (though also with its issues).

    12. 1

      Made me think of lenses and their types.