Simon Peyton Jones interview(haskell.foundation) |
Simon Peyton Jones interview(haskell.foundation) |
“So, one of the great things about Haskell actually, that is spoken about and I think it’s the sort of killer app for Haskell, is that it’s so refactorable, right? You can do a heart or lung transplant on GHC and make truly major changes and the type checker just guides you to do all the right things.”
Freely refactoring the code with worrying about unit tests, etc seems quite appealing.
To summarize the killer app for Haskell is that “it’s so refactorable”
I thought GHC was famously a nightmare to work in?
> GHC is not exemplary of good large scale system design in a pure function language. Rather ironically, it violates the properties that draw people to functional programming in the first place: immutability, modularity, and composability
> many new features have been force-fitted into the existing code without proper redesign
> While the current design isn’t glorious, it works
> On the bright side, GHC is written in Haskell, and this language is particularly well suited to performing massive refactorings with confidence that nothing breaks. Thus, it should be possible to refactor the GHC library towards a more robust and versatile design
and in fact Simon Peyton Jones continued by saying exactly that:
> You can do a heart or lung transplant on GHC and make truly major changes and the type checker just guides you to do all the right things. The difficult stuff is envisioning and being very clear about what you’re trying to do. Actually doing it is often not that hard.
So the two texts and the two opinions are completely in alignment. GHC is famously bad insofar as it has a poor design. But once a better design is designed, you can give it the heart transplant it needs without excess stress.
I have no idea how the heart transplant proposed by Sylvain Henry, John Ericson and Jeffrey M. Young is going. I suppose at some point there should be something checked in and a report about how painful or painless it was (and, potentially, if it's really completely wrong, perhaps a series of bug reports in the next seven releases of GHC).
That's not my experience. I did small changes in GHC when I had less then 6 months of Haskell experience. I felt the code was pretty straightforward.
This only tells that SPJ never had to work in hard realtime nor kernels. GHC code throws and doesn't help in violating latency bounds. Not at all. For such tasks we do have much better systems, without GC.
See, when you are defining a Haskell program, you are conceptually creating a tree of thunks that eventually get executed by the GHC runtime. Those thunks are typed, meaning they have typed inputs and outputs, and are either side-effect-free or are defined in a context that controls their side effects (e.g. the IO monad).
So you can change the definition of types willy-nilly and either get a working compiled program or some error output that tells you exactly what is broken or doesn't make sense to GHC's model of your proposed computation. Because computation itself is typed, you have a stronger guarantee that it will work as expected when executed by the GHC runtime. Because side effects are controlled, you are forced by the type checker to handle runtime errors (or crash).
At least that's how I understand it as someone who works with gifted Haskell engineers, but exists very much on the periphery of understanding.
If it compiled before and worked and your refactored version also compiles, chances are you didn't break anything.
all state is factored, so it can easily be refactored.
In my experience the ease of refactoring is more depending on the quality of the code you are refactoring than the language. That said, a strong type system helps avoiding stupid mistakes and Haskell have a very strong type system.
you can unplug, replug stuff at will
> SPJ: It’s a very different prospectus because in this case Verse is a pretty well-formed beast in Tim’s head. If we want to do something different we’re going to have to persuade him but I’m fine with that, right? But the dynamic is that he’s a sort of technical lead on the project – which is very unusual for the CEO of a multibillion dollar company and actually quite rewarding.
Quite unusual and very cool!
"So, for me, that’s as far as increasing our ability to give you statically guaranteed theorems about Haskell programs.
My money’s on Liquid Haskell at the moment and I hope that we the Haskell community"
My experience is that other refinement type systems are way less complex. See: https://github.com/hwayne/lets-prove-leftpad
In particular, compare https://github.com/hwayne/lets-prove-leftpad/blob/master/liq... to https://github.com/hwayne/lets-prove-leftpad/blob/master/daf...
For me this has been a bit of a disappointment.
[1] https://youtube.com/watch?v=wNa3MMbhwS4
[2] https://corecursive.com/015-dependant-types-in-haskell-with-...
The applications I’ve heard for Idris also have to do with finance (although not blockchain stuff).
(To be abundantly clear and uncontroversial, as it pertains to this comment, I'm not interested in discussing "is web3/metaverse {good,bad}", but rather in discussing the purely functional programming community-of-community's interests or anti-interests in it.)
Python/C++ come with their issues and when starting a project from scratch (e.g. a blockchain), there's more flexibility in the choice of language. In the blockchain field, throwing buzzwords has proven useful to gather money and make some projects stand out (functional programming, formal verification...). Also academics love these language, so starting a project in Haskell/OCaml can get you contributions from academia, possibly some big names joining your team. And of course, strongly typed languages with a clean semantics give you more safety which is important in some fields.
It means you can run your unit tests without having to change everything everywhere all at once.
The flag is -fdefer-type-errors
And I would say that if somebody never worked with Haskell (or some other language with a strong type system like Idris) they can bit fantom what is possible to encode in the type system.
He's one of my heroes, long may he lang
This is generally true in idiomatic Haskell code, but in fact even pure functions in Haskell can throw runtime exceptions, and you are not forced to handle these.
aside from that, you'd just need to worry about OOMs and faults in native code.
“error” is simply bottom. Bottom is an inhabitant of every Haskell type. There’s no straightforward way to just turn it off.
Work has been steady the master project plan is tracked in this ticket: https://gitlab.haskell.org/ghc/ghc/-/issues/17957
Almost all the recent work has been performed by Dominik Peteler (@mmhat) during Google summer of code, which John supervised. We've primarily been focused on landing !8341[0] which makes huge strides in Core w.r.t. modularity (see https://gitlab.haskell.org/ghc/ghc/-/issues/21872), but are on hold until schedules agree and some vacations end.
So the modularity project is far from dead. In fact Sylvain and I are planning on returning to it after we upstream the new Javascript backend (slated for 9.6, see MR!9133[1], tracking ticket[2]) hopefully this week.
PS: That patch is actually a good example of a gnarly lung transplant for GHC's Core IR (and done by a new contributor!).
[0]: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8341
[1]: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9133
This is possibly the single best example ever of how Computer Scientist and Software Engineer are different jobs with different skill sets.
That admittedly doesn't entail that Haskell ought to have special functions like 'error' that invite the programmer to explicitly introduce bottom values as a mechanism of signaling errors. However, in the real world, executing any function may raise an exceptional condition at any time (e.g. an out of memory error), regardless of programming language.
I don't understand: if the function you called doesn't terminate then you're blocked so I don't see why this should impact the types..