Most undergraduates take a compiler course in which they implement
C, Java or Scheme. I have yet to see a course at any university,
however, in which Haskell is used as the project language. [...] The
closest project I’ve seen to this is a minimal Haskell dialect
called duet.
Ben Lynn has been working on such a Haskell compiler[0], self-hosting and with IO too. It's a little unusual in its approach to compilation (targets combinatory logic and executes via graph reduction), but it's a great example nonetheless, from which one could build an undergraduate course.
Code generation is a difficult issue, compiling a lazy functional language to assembly could easily fill up two semesters of classes alone.
The VM in C is really small and the compiler can be built up incrementally[1].
I think you're essentially right, but the "toy language" is often a subset of some real language. in my compilers course it was a subset of pascal, which targeted a very friendly IR. there's no inherent reason why the same couldn't be done for a subset of C, Java, or Scheme. in particular, Scheme has a relatively simple syntax to parse. C is fairly difficult to parse, not sure to what degree the grammar can be simplified by removing features.
I have yet to see a course at any university, however, in which Haskell is used as the project language.
Given the language's inherent complexity (and tortured history) -- is the task of writing a Haskell compiler really suitable for the undergraduate curriculum?
That is, for "mere mortals". Not the kind who take tons and tons of graduate courses. In which case we'd be speaking of graduate-level courses.
I used this or similar (I forgot the name back then) when I was at UU decades ago; it was quite pleasant to work with as a teaching tool compared to ghc, esp at that time.
This post highlights my biggest problem with the language: it's about the how, not about the why. For example, dependent types. They add significant complexity to the language and are intended to help with correctness. But are they an effective way to achieve it compared to alternatives? The fact that even current formal verification research is mostly looking elsewhere seems to suggest that the answer is likely negative, so why focus on them now? Or algebraic effects, about which the article says, "These effect-system libraries may help to achieve a boilerplate-free nirvana of tracking algebraic effects at much more granular levels." But is that even a worthwhile goal? Why is it nirvana to more easily do something that might not be worth doing at all?
Researchers who study some technique X ask themselves how best to use X to do Y, and publish a series of papers on the subject, but practitioners don't care about the answer to that question because they don't care about that question at all. They want to know how best to do Y, period. One could say that every language, once designed, is committed to some techniques that it tries to employ in full effect. But any product made for practical use should at least strive to begin with the why rather than the how, both in its original design and throughout its evolution. I work with designers of a popular programming language, and I see them spending literally years first trying to answer the why or the what before getting to the how. So either Haskell is a language intended as a research tool for those studying some particular techniques -- which is a very worthy goal but not one that helps me achieve mine -- or it's intended to provide entertainment for practitioners who are particularly drawn to its style. Either way, it's not a language that's designed to solve a problem for practitioners (and if it is, it doesn't seem that testing whether it actually does so successfully is a priority).
I think it's important to have languages for language research, but if that's what they are, don't try to present them as something else. And BTW, at ~0.06% of US market share -- less than Clojure, Elixir, Rust and Fortran, about the same as Erlang and Delphi, and slightly more than Lisp, F# and Elm -- and little or no growth (https://www.hiringlab.org/2019/11/19/todays-top-tech-skills/), I wouldn't call Haskell a "popular language," as this post does, just yet.
Another Haskell post, another pron comment about how its community is misguided and wasting their time.
I've solved production problems with Haskell (including w/advanced type system features & dependent types). I will continue to do so. And I will probably write other commercial, money-making software for enterprises and for myself for years to come.
I have plenty of experience programming in other languages. Clojure, Go, Java, Python. Haskell was the hardest to pick up. But now that I know it, writing other languages requires so much more energy in comparison. I barely have to try to deliver equal results compared to solving the same problems with other tools (so it's not a result of me just increasing my skill - the tool itself is a force multiplier for myself 100%)
What I said was that Haskell's design and evolution have been primarily guided by research questions rather than business needs, not that it's unsuitable for production use. I didn't say it's unsuitable for production use, nor do I think it. That doesn't change the pretty obvious fact that its features are mostly guided by research questions.
> barely have to try to deliver equal results compared to solving the same problems with other tools (so it's not a result of me just increasing my skill - the tool itself is a force multiplier for myself 100%)
If that effect were scalable and largely universal, then there would be no need for this discussion, anyway. But if it works well for you and the other thousands of developers who make up ~0.06% of the market, then it's great that it's available. Research languages also serve a very valuable goal in figuring out what works and what doesn't. If no one used them, we wouldn't know.
Which Haskell design decision flies in the face of production use or what kind of feature would you like you to see in Haskell that isn't picked up due to it being an academic language?
I’ve not used Haskell (so I have no idea of the validity) but the criticism I always hear leveled in discussions is that lazy evaluation makes runtime hard to reason about.
On the other hand this blog post http://www.haskellforall.com/2013/05/program-imperatively-us... demonstrates how one of the bits of Haskell that some people find complex (lenses) can be used together with the state monad to provide an "imperative-like" experience that's even nicer than most imperative languages.
Is it just me, or is the linked example messed up in all sorts of ways, even ignoring the use of monads and transformers? Looks like a novice trying to code in fancy ways.
For instance, it defines a Beer datatype, yet stores a plain Int in the state, then casts it to Beer only to use a custom pretty printer, instead of creating a verse :: Int -> String, or verse :: Beer -> String function.
Yeah the the very first and by now a worn out dismissal you always see is it's an academic research language, not for writing REAL software.
Out of interest, what kind of software do you build with Haskell? I'm doing web stuff and haven't quite been able to decide whether to stick to Haskell or Elixir for my own projects.
Hm I'd describe it mostly as generic "backend engineering." Web services, databases, data processing, etc. I've used GHCJS as well but I mostly made small changes (I don't have frontend skills.)
In my free time I'm making games in Haskell, but that's slow-going partially due to the ecosystem not being mature but mostly due to lack of free time :)
This has been a growing concern of mine about the whole functional-as-defined-by-John-Backus (viz, not including lisp) lineage of programming languages. On my grumpy days, I'm inclined to say that the current culture can be best described as, "Got excited and ran off to do some coding before making it all the way to the end of The Evolution of a Haskell Programmer." (https://www.willamette.edu/~fruehr/haskell/evolution.html)
That doesn't particularly bother me in Haskell, which was born as, and continues to primarily serve as, a platform for language research. (Secondary purpose, at least for me: A platform for daydreaming about a non-post-C++ existence. I suspect that professional use remains a small minority.) It gets more worrisome to me in an ostensibly industry-oriented language like Scala. There I start to fear that my colleagues choose ways of solving problems for about the same reasons that I prefer mechanical watches over quartz ones: Not because they're more practical or more economical - no in both cases - but because they're cooler.
I think it'll probably get better naturally, though, the same way that lisp programming culture eventually stopped being quite so enamored of macros, and Java programming culture eventually stopped being quite so enamored of elaborate XML configuration files.
> They add significant complexity to the language and are intended to help with correctness. But are they an effective way to achieve it compared to alternatives?
Python programmers say the same about all static type systems.
What alternatives do you have in mind? Are they as generally applicable as dependant types?
Dependant types are a simple and unifying way to solve a variety of shortcomings with conventional statically typed systems. For example, dependant types can express first-class modules as simple records, or allow sophisticated record operations like merge to be well-typed.
> [tracking algebraic effects] But is that even a worthwhile goal? Why is it nirvana to more easily do something that might not be worth doing at all?
Given the various hugely expensive bugs I have been involved in (e.g. Java toString on a date reading the system locale). I would say yes. In my industry, reproducable numbers are of vital importance, so much so that the quants use Haskell in preference to something more mainstream and supported.
> Python programmers say the same about all static type systems.
So what? Even if you think having X is good, that doesn't mean having 100X is necessarily better.
> Dependant types are a simple and unifying way to solve a variety of shortcomings with conventional statically typed systems.
But solving problems with type systems is not a business goal. Increasing correctness is.
> What alternatives do you have in mind?
The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods. Dependent types are a powerful, general and complex mechanism that only scales well for very simple problems.
> Given the various hugely expensive bugs I have been involved in (e.g. Java toString on a date reading the system locale). I would say yes.
There are easier ways, like Java's permission system, that I mentioned elsewhere.
> The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods
Model checking is great, and many tools developed by the model checking community are marvellous (especially the TLA+ model checker).
But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. They scale well enough to show that that said kernel has no in-kernel storage channels that can be exploited in a side channel attack.
Deductive methods scale well enough to verify (completely automaticallly, without human intervention) that the compiled binaries faithfully implement a given C program, so the compiler and linker need not be trusted.
These are deep properties. You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length (not algorithm sketches or high-level system descriptions, actual code that compiles and runs).
That's for deductive approaches in general. But sone of your specific claims about type theory are dubious as well. Elsewhere you claim that
> The fact that even current formal verification research is mostly looking elsewhere seems to suggest that the answer is likely negative
Your claim that formal methods research is mostly looking elsewhere is really stretching it. More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year. The number of submissions to ICFP's TyDe track had over 30% growth last year. TYPES already dwarfs the biggest conferences devoted to model checking or any other specific formal method. No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere". No other subfields are ezperiencing comparable growth.
> But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. ... Deductive methods scale well enough to verify (completely automaticallly, without human intervention) that the compiled binaries faithfully implement a given C program, so the compiler and linker need not be trusted.
Unfortunately, they do not. The two projects you mentioned are positively tiny -- they correspond to about 10KLOC of C, or less than 1/5th the size of jQuery -- and they each took world experts years of effort. Both, BTW, required serious limitations in the algorithms used to keep them simple. That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator.
> You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length
Concolic tests are unsound, which is why they scale so well. Model checking routinely verifies much larger codebases, so much so that people don't bothering writing papers about it. When deductive methods are used to verify a 10KLOC program that's news. You can buy off-the-shelf model checkers that do more in industry pretty much all the time.
> More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year.
Perhaps, but when you look at FM conferences, deductive methods in general and type systems in particular are significantly more represented.
> No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere"
There's no need to abandon something that has yet to break through in the first place. Most FM research is just done elsewhere.
> No other subfields are ezperiencing comparable growth.
> You can buy off-the-shelf model checkers that do more in industry pretty much all the time.
When you establish actual deep properties, that's news. You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker.
Again, if non-deductive formal methods are routinely used to establish comparably deep properties of programs of comparable size (as you claim), you should have no trouble naming at least one example. You don't need research papers to justify that claim, just a few statements of the form "Global Property P of 10k line C Program Q was established by model checker R".
> That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator.
No, not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels. While that is a significant expense, there is no order of magnitude difference, much less something in the "billion dollar particle accelerator" territory. Especially since it delivered global correctness properties that are out of reach for any other method.
> you should have no trouble naming at least one example.
Model checkers don't usually beat deductive proofs in both size and depth, but they often easily beat them on any one of these.
In terms of code size, model checkers have verified reachability on C programs of over 50KLOC in less than an hour for at least 15 years now (BLAST). Some bugs found in the past few years Linux kernel with a model checker are here: http://linuxtesting.org/results/ldv-cpachecker
In terms of depth -- there are too many to choose from. Both SCADE and Simulink are routinely used in industry to verify LTL. TLC, a model checker for TLA+ was used to develop and verify deep properties of the OpenComRTOS kernel https://en.wikipedia.org/wiki/OpenComRTOS
> You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker.
There is no real method like this of any kind. A heroic effort by teams of PhD candidate proof monkeys working for some years isn't a technique.
> not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels.
I don't know what the cost of producing commercial L4 microkernels, but that 10KLOC program took 12 person years, plus another 12 for tooling. 2 years per KLOC, and even half of that, is well beyond the reach of 99% of software, plus no one has ever managed to use deductive verification for programs that are significantly larger than that in any amount of time. That's about three (!) orders of magnitude behind ordinary business software. This gap has remained pretty much constant over the last forty years.
I think it is possible that deductive proofs may become viable in industry in some high-assurance, high-cost domains, provided that the programs are very small. But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software.
TLC checks models, not implementations, so the compariaon is not really appropriate at all. Using TLA+ on actual code is yet to be a success story:
Deductive methods the assembly refinement proof of seL4 (binary verification) is completely automated, and takes less than two hours on a modern PC.
OpenComRTOS is much much smaller and simpler than seL4 (comparable to eChronos). It's important work, and a neat example at how formal modeling allows one to _design better products_ even in well-explored domains, but it's a really poor example for illustrating the supposed scalability of model checking compared to deductive methods. Especially ehen the book on the system emphasizes how they kept experiencing state explosions which broke the checker during development.
In any case, TLC checks specifications, not implementations; it's not appropriate to compare them to deductive methods that work on actual source code (cf. the properties of the _specification_ account for less than 5% of total proof obligations, and establish global properties that are stronger and deeper than model checking could provide). Attempts to use TLA+ on implementations such as C2TLA+ are far less successful, it's not been demonstrated to scale well (no case studies above 1 kloc at all). Writing and checking specifications is useful, and leads to more reliable software, and you're free to argue that there is far more low-hanging fruit to be found in this area than in dependent type systems. But it's not the same as checking 50kloc _programs_, and you should not conflate these activiities.
Not to say that many deductive tools are completely automated and have been shown to work at scale too: SydTV verifies the correspondence between thr seL4 binary and the corresponding sourcr in under two hours on a modern PC.
And what you're competing against (dependent types) has the potential to scale far better: even the 3.5kloc Agda program I'm working on can be checked in under a minute, and Agda is very far from optimal with respect to type checking.
> But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software.
You're entitled to that opinion. Just don't conflate that with general trends and sentiments in the formal methods community. Contrary to your earlier claims, there is no agreement in the field that one should "look elsewhere".
The same goes for your claim that non-deductive techniques scale better and establish deeper properties than deductive ones: if you believe this will be shown decisively true in the future, that's a perfectly alright opinion to have, and you'll find plenty of peiple who share it. But don't act as if it's an empirical fact when the evidence shows no such scalability advantage at this point in time, and most deep properties that deductive, proof-producing methods can establish are still out of reach for non-deductive methods.
(ps. Writing these posts took me a lot of time, so I'll have to limit myself to one more comment in this thread.)
> TLC checks models, not implementations, so the compariaon is not really appropriate at all. Using TLA+ on actual code is yet to be a success story
TLC checks specifications of arbitrary detail. I don't see why it matters when it comes to deep properties. There does not exist any method -- automated or manual -- that can verify deep properties of code of size even within an order of magnitude of ordinary applications. Inasmuch as model checkers and deductive proofs work at all, model checkers are clearly more scalable.
> But it's not the same as checking 50kloc _programs_, and you should not conflate these activities.
I explicitly said that model checkers don't beat deductive proofs on size and depth at the same time, but they do beat them easily separately. Still, there are a few cases where model checkers fail, and the only option available is formal proof. Usually, that is too expensive, but we have seen that in extreme circumstances when a great amount of work is applied to a very small amount of code, this could "work" in the sense that specialized, highly-trained teams working for a long time could do it. AFAIK, this has so far only been tried in research projects, and never by "ordinary" engineers.
> And what you're competing against (dependent types) has the potential to scale far better: even the 3.5kloc Agda program I'm working on can be checked in under a minute, and Agda is very far from optimal with respect to type checking.
If checking a proof were comparable to finding one, then the P vs NP problem would have been resolved a long time ago. You should compare the time it takes to write and model-check a 3500-line TLA+ spec vs the time it takes to write a 3500 line Agda program and check the proofs.
> Contrary to your earlier claims, there is no agreement in the field that one should "look elsewhere".
I didn't say there was consensus; I said that the majority of researchers are looking elsewhere, and that's where most research is focused.
> But don't act as if it's an empirical fact when the evidence shows no such scalability advantage at this point in time, and most deep properties that deductive, proof-producing methods can establish are still out of reach for non-deductive methods.
Deductive methods have been studied for at least forty years now, and AFAIK, they have never been used in any meaningful scale by non-researchers in industry. On the other hand, while automated methods obviously have not reached the point that they could automatically verify arbitrary properties of arbitrarily sized code -- and they never will, and neither will deductive methods -- they are being used in industry on a regular basis, with capabilities ranging on depth, scale, and soundness, and their use is growing; just in the safety-critical space where SCADE and Simulink are used, but at Microsoft, Amazon, Oracle and Facebook as well as smaller companies. As an applicable formal method in the real world, deductive proofs don't even exist yet, heroic efforts by researchers notwithstanding.
Which is why it's unsurprising that more researchers are looking into methods that have had some measure of success outside research. I find all aspects of formal methods very interesting, and I wish all researchers luck and success (and I sometimes amuse myself with small machine-checked proofs, usually in the TLA+ proof assistant or sometimes in Lean), but it is misleading to present deductive and automated methods as being on equal footings in terms of real-world success.
I also think there is a fundamental mismatch between deductive proofs and software verification, something I call the "soundness problem." Unlike mathematics, while an algorithm can be proven correct, a software system never can, any more than a chair could -- it's a physical system. This means that soundness is never, ever, ever a requirement in software verification. On the other hand, achieving soundness (for deep properties) is very costly, as both theory and experience tell us. This is why many experiments these days -- both in academia and industry -- try to turn down the soundness knob to achieve other actual requirements in software verification (see O'Hearn's recent "incorrectness logic"). A method that is inflexible on soundness -- which is both not required and very costly, is one that seems to be clashing with the very needs of software verification.
This is also why you find that research projects using deductive proofs are almost invariably done by people with little or no industry experience. They treat the problem of software verification as an academic exercise without understanding what real software is and how it's used. On the other hand, you see many more researchers with industry experience looking into automated methods. It's funny, to see the transformation. You look at someone like Peter O'Hearn that's moved from academia to industry. What does he do then? Turn down soundness. You also see it with Leslie Lamport and David Harel, and I could probably find more examples. Once researchers are faced with how software is actually developed, the first thing they realize you need to do is to reduce soundness (for deep properties). Soundness is not a requirement, and it is the enemy of scale and speed, which are (I've written a short post on one aspect where researchers don't understand how software is written: https://pron.github.io/posts/people-dont-write-programs). There are cases in software where soundness is needed -- automatic refactoring and compiler optimization -- which is why I think type systems are interesting for those, but correctness -- not so much.
On the other hands approaches to correctness based on dependent types are favored by people who may be very good researchers, but are not professional programmers, not familiar with industry, and have not conducted field studies (people like Bob Harper, Adam Chlipala, Edwin Brady, and Leonardo de Moura). Now, their research is very good, but it is theoretical, and so far unsuitable for any field use, which is unsurprising, given that they're unfamiliar with how software is made. Which brings me back to my original point: bringing dependent types to Haskell is an interesting first field experiment, but it is just that -- a research experiment designed to answer a research question (someone who worked on seL4 told me that they believe they could bring the cost down enough to be similar to that of high-assurance software, but that's not where Haskell is or, I think, wants to be). It is very different from the kind of work that people like O'Hearn and Lamport are doing, which is scaling up approaches that have already shown their worth in the field.
This is misleading. There are two notions of scalability:
- Scalable to large code bases.
- Scalable to deep properties.
Deductive methods are currently the only ones that scale to deep properties. Model checking et al are currently the much better at scaling to large code bases. Note however two things: First, Facebook's infer tool which scales quite well to large code bases, is partly based on deductive methods. Secondly, and most importantly, under the hood in most current approaches, SAT/SMT solvers do much of the heavy lifting. Existing SAT/SMT solvers are invariably based on DPLL, i.e. resolution, i.e. a deductive method.
> Deductive methods are currently the only ones that scale to deep properties.
Model checkers check deep properties with overall significantly less effort. It is true that they don't always succeed, but neither do deductive proofs. In industry, deductive methods are used as a last resort, when they're used at all, to tie together results from automated techniques.
> Note however two things: ...
That's not what I meant by "deductive methods;" I meant verification by semi-automated deductive proofs. Also, SMT solvers aren't used in isolation to verify significant pieces of software, they're used as components of model checkers, concolic testing and proof assistants (or to verify local properties of code units), so they're used in both semi-automated deductive methods as well as in automated methods. I also believe that DPLL is based on assignment and backtracking, not resolution.
DPLL is based on a form of resolution, in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model.
TLC is a model checker can check most properties expressible in TLA+, which are more expressive than any base lambda-calculus theory (e.g. it includes temporal refinement properties). See my overview on TLA+'s theory: https://pron.github.io/tlaplus
> in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model
So not deductive. You know that because DPLL does not directly yield a proof of UNSAT.
Lamport's TLA contains ZF set theory. That makes TLA super expressive. Unless a major breakthrough has happened in logic that I have not been informed about, model checkers cannot verify complex TLA properties for large code bases fully autom atically. Let's be quantitative in our two dimensions of scalability:
- Assume we 'measure' the complexity of a property by the number of quantifier alternations in the logical formula.
- Assume we 'measure' the complexity of a program by lines of code.
(Yes, both measures are simplistic.) What is the most complex property that has been established in TLA fully automatically with no hand tweaking etc for more than 50,000 LoCs? And how does that complexity compare to for example the complexity of the formula that has been used in the verification of SeL4?
So not deductive.
So first-order logic is not deductive, because it doesn't yield a direct proof of FALSE?
There is an interesting question here: what is the precise meaning of "deductive"? Informally it means: building proof trees by instantiating axiom and rule scheme. But that is vague. What does that mean exactly? Are modern SAT/SMT solvers doing this? The field of proof complexity thinks of (propositional) proof systems simply as poly-time functions onto propositional tautologies.
> What is the most complex property that has been established in TLA fully automatically with no hand tweaking etc for more than 50,000 LoCs? And how does that complexity compare to for example the complexity of the formula that has been used in the verification of SeL4?
TLC, a model checker for TLA+, is commonly used to verify arbitrary properties -- at least as "deep" as those used in seL4, and often deeper -- of TLA+ specifications of a few thousand lines. Those properties can informally correspond to codebases with hundreds of thousands of lines, but there is currently no method for formally verifying arbitrary properties of 50KLOC, be it automatic or manual. Automated methods, however, are used either for deep properties (quantifier alterations) of few k-lines of spec/code or shallower (though still non-local and non-compositional) properties of 50-100KLOC. Manual deductive methods are virtually used for nothing outside of research projects/teams, except for local, compositional properties, of the kind expressible by simple type systems.
> So first-order logic is not deductive, because it doesn't yield a direct proof of FALSE?
In any logic you can work deductively in the proof theory, or in the model theory. DPLL SAT solvers work in the model theory of first-order logic. Also, SAT solvers work on propositional logic, not first-order logic. Because of completeness, we know that every model-theoretic proof corresponds to a proof-theoretic proof, but that's not how most SAT algorithms work (except for resolution solvers).
> There is an interesting question here: what is the precise meaning of "deductive"?
It means using the syntactic inference rules of a proof theory, rather than the semantic rules of a model theory (possibly relying on completeness meta-theorems, as in the case of propositional logic, although that's not relevant for most interesting first-order theories). SMT solvers employ SAT, and can work on some first-order theories. I am not familiar with all the techniques SMT solvers use, but I believe they employ both proof-theoretic and model-theoretic techniques. In any event, as I mentioned before, SMT solvers are rarely used alone, because they're very limited. They are used as automated helpers for specific steps in proof assistants (TLAPS, the TLA+ proof assistant makes heavy use of SMT solvers for proof steps), for local properties of code (e.g. OpenJML for Java, in Dafny and in SPARK) or as components in CEGAR model checkers and in concolic test systems.
TLC ... is commonly used to ...
at least as "deep" as those
used in seL4, and often deeper
What you are in essence implying here is that the SeL4 verification can be handled fully automatically by TLC. I do not believe that without a demonstration ... and please don't forget to collect your Turing Award!
One problem with model-checking is that you handle loops by replacing loops with approximations (unrolling the loop a few times) and in effect only verifying properties that are not affected by such approximations. In other words extremely shallow properties. (You may use different words, like "timeout" or "unsound technique" but from a logical POV, it's all the same ...)
the model theory ...
rather than the semantic
rules of a model theory
All mathematics is deductive.
ZFC is a deductive theory, HOL is a deductive theory, HoTT is a deductive theory. MLTT is a deductive theory,
Quine's NF is a deductive theory.
With that, what mathematicians call a model is but another deductive theory, e.g. the model theory of Peano Arithmetic happens in ZFC, another deductive theory.
The deductive/non-deductive distinction is really a discussion of different kinds of algorithms. Deduction somehow involves building up proof trees from axioms and rules, using unification. It could be fair to say that concrete DPLL implementations (as opposed to textbook presentations) that are based on model enumeration, non-chronological backtracking, random restarts, clause learning, watched literals etc don't quite fit this algorithmic pattern.
I am not sure exactly how to delineate deductive from non-deductive algorithms, that's why I think it's an interesting question.
SMT solvers are rarely used alone,
I agree, but model checkers, type checkers for dependent types , modern testing technques, and (interactive) provers all tend to off-load at least parts of their work to SAT/SMT solvers which makes the opposition between deductive and non-deductive methods unclear.
* * *
BTW I am not arguing against fuzzing, concolic, model checking testing etc. All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code.
> What you are in essence implying here is that the SeL4 verification can be handled fully automatically by TLC.
No, I am not. Read what I wrote again :)
> and please don't forget to collect your Turing Award!
Some people have already beat me to it. The 2007 Turing Award was awarded for the invention of model checkers that precisely and soundly check deep properties.
> One problem with model-checking is that you handle loops by replacing loops with approximations
No, that's what sound static analysis with abstract interpretation does. Model checkers are both sound and precise, i.e. they have neither false positives nor false negatives. To the extent they use sound abstraction (i.e. over-approximation), as in CEGAR algorithms, they do so to increase performance and to sometimes be able to handle infinite state spaces. A model checker, however, is always sound and precise, or else it's not a model checker.
> In other words extremely shallow properties.
Model checkers commonly check arbitrarily deep properties. Engineers in industry use them for this purpose every day.
> All mathematics is deductive.
Yes, and all (or much, depending on your favorite philosophy of mathematics) of it has models. If you have two apples in one hand and one apple in the other and you count how many you have, you have not done so using deduction in any logical theory. That had you used such a process you would have also reached the same result is because of soundness and completeness meta-theorems. That mathematics has both proof and model theories, and that they're compatible, is the most important result in formal logic.
> All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code.
All verification methods are limited by both size of code and depth of properties. For non-trivial property, the least scalable method, on average, is deductive proof. Which is not to say it is not useful when automated methods have failed.
Sorry, I got confused about loops in model checking, I was wrong about that. I don't know what happened, since I even have co-authored a model-checking paper where we do check loops.
Be that as it may, seL4 cannot currently be automatically verified, and it's not due to code size (8700 lines of C and 600 lines
of assembler). It's hard to see what the obstacle to mechanisation could be but logical complexity.
Model theory is not some magical deduction-free paradise. The reason we care about model theory in logic is because we want to have evidence that the deductive system at hand is consistent. Building models of Peano arithmetic in ZFC for example, but also relating constructive and classical logic through double negation or embedding type theory in set theory, are all about relative consistency. It's easy to make a FOM (= foundation of mathematics) unsound, and logical luminaries including Frege, Church and Martin-Lof managed to do so. Those soundness proofs in essence transform a proof of falsity in one system to the other, and relative consistency is the best we can get in order to increase our confidence in a formal system. It is true that traditional model theory, as for example done in [1, 2, 3]. doesn't really foreground the deductive nature of ZFC, it's taken for granted, and reasoning proceeds at a more informal level. If you want to mechanise those proofs, you will have to go back to deduction.
> It's hard to see what the obstacle to mechanisation could be but logical complexity.
There is no impenetrable obstacle if humans could do it (for some definition of "could"), but the difficulty is handling infinite state spaces. Model checkers can do it in some situations, but the could do it in more. Neither model checkers nor humans can handle infinite state spaces -- or even very large ones -- in all situations (halting problem and its generalizations).
> Model theory is not some magical deduction-free paradise.
I just pointed out that some of the most successful automated methods, like model checkers (hence their name, BTW) and SAT solvers (which are really special kinds of model checkers), work in the model, not the proof theory.
> The reason we care about model theory in logic is because we want to have evidence that the deductive system at hand is consistent.
The reason we care about models is that we want to know that the "symbols game" of formal logic corresponds to mathematical objects; i.e. that it is sound -- a stronger property than consistency. The model existed first. Proof theory in deductive systems -- and formal logic in general as we know it -- is a 20th-century invention (well, late 19th but only accepted by mathematicians in the 20th).
> But solving problems with type systems is not a business goal. Increasing correctness is.
I gave an example of increasing correctness in the context of record data types, something almost every business app does.
> The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods.
And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query?
> There are easier ways, like Java's permission system, that I mentioned elsewhere.
Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM?
> I gave an example of increasing correctness in the context of record data types, something almost every business app does.
A tank is a way of getting people to work faster than walking, a concern that almost all people have, but that doesn't mean we should propose tanks for that purpose. That dependent types could increase correctness doesn't mean they should be added to a language -- unless its goal is research. This is a common problem I see. Say A is some business concern. The question we need to answer to decide whether to use solution B is not B => A but A => B.
What you're saying is that if I choose to use technique X and I want to achieve Y, then this is a way to do it. This is not the same as saying this is a good technique of achieving Y. The logical implication is reversed from what we'd like to find out. At best you're saying if you use dependent types, you increase correctness. I want to know what you should do to increase correctness, and using dependent types might be the worst possible option. The question is not whether dependent types imply increased correctness, but whether wanting increased correctness implies we should use dependent types. In fact, the post cites a case study about dependent Haskell that isn't exactly a glowing review of the feature.
> And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query?
"Type-checking a SQL query" is not a business goal, and if I try to convert it to some goal you may have been referring to, for example, what is a good way to check if there are mistakes of some simple class in a SQL query, then I'm not sure simple testing isn't more than sufficient. Having said that, I like simple type systems, and I think they are also sufficient for that (e.g. there are typesafe SQL libraries for Java).
> Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM?
I don't know what the requirements are so I don't know.
Dependent types are not just useful for proving correctness properties, and in fact I think dependent types in Haskell are not really intended to prove really complex properties, like the full functional correctness of a compiler. Hence, I think the use of Coq or Agda proofs as an example of impracticality is a strawman argument. You might need a research team and several years to show the correctness of an operating system in Coq. You do not need that to have type-safe database access or statically checked matrix sizes. Not all non-research uses of dependent types are impractical.
You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever? Should Java not have added lambdas because it already had anonymous inner classes? You can clearly get by just fine in a lot of business applications without some of these features.
I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness. It’s not so clear that dependent types are too complex a solution there, especially if you look at a library like Servant, which already uses some advanced type system features, and which is actually a really practical library that is probably used in production applications as well. A library like Servant might be able to expressed more clearly with dependent types than with a hodgepodge of type system extensions. I think that wanting type-safe REST API access is already an order of magnitude more practical than model checking kernel code.
> Not all non-research uses of dependent types are impractical.
That's like saying that a tank could get you to work, so some of its uses are practical for civilians. Does the weight of dependent types justify such disproportionate applicability?
> You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever?
And those arguments would be just true, except that industry languages adopted those features many years after they've been tried in research languages and shown their worth, while industry languages didn't adopt other features (or perhaps haven't yet), because they didn't prove to be the right solutions to big problems. It's perfectly fine to adopt many ideas that are open research questions, but if you do so you can't deny that your goal is research.
> I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness.
No, because that's the inverted implication, or "tank" problem again. Just because a tank can get you to work doesn't mean that it should. If you want to achieve goal A, and feature B achieves it, i.e. B => A, you cannot conclude from that that you should adopt B. You're assuming A and B => A and concluding B. That just doesn't follow.
The question we're asking is whether A => B. We're not asking whether dependent types can be put to some practical use -- that's what researchers ask. We engineers ask what solution to our problem we should adopt (usually the least costly one).
> but practitioners don't care about the answer to that question because they don't care about that question at all. They want to know how best to do Y, period.
OK, I'll bite. If the entirety of your goal is to do Y, you will never write a single test. Why would you write a test? It doesn't "do Y", for whichever Y is producing profit or some other benefit for you.
Real, True Scotsmen understand that how to do Y is important, because it makes sure that they'll be able to do Z tomorrow. Tests are not essential for functional systems, they are essential for maintainable systems.
Types are just tests enforced by the compiler. Every type-level tool that Haskell gives you is just another tool that makes it easier to write tests that actually help prove that your code is still working.
Half the problem with our industry is that no other industry would accept unmaintainable product. Too many practicioners are practically proud of all their rewrites and green-field projects.
Though I don’t use it professionally, I believe purescript has proven that algebraic effects systems are very useful for granular effect handling.
Things like “this writes to the database”, “this makes an unbounded query”, “this requires a random number generator “, rather than a nebulous “oh this has I/O” is very powerful and useful for maintaining a system
> Things like “this writes to the database”, “this makes an unbounded query”, “this requires a random number generator “, rather than a nebulous “oh this has I/O” is very powerful and useful for maintaining a system
1. How do you know that?
2. Why?
3. Why is tracking the effects in the type system useful? Even if and where this is important, it could be easily achieved using something like Java's 20+-year-old security manager and with finer granularity (i.e. you can allow code to read or write certain files, connect to certain domains etc.) [1]. Just because you can do something in the type system, doesn't mean you should, as it may not be the best way.
Because it is a way to force you think about how you structure your code. You necessarily pull out the pure parts and are explicit in handling all the impure parts. This also makes it very easy to test your code.
Why is it done in the type system? Well, because the goal is to have guarantees at compile-time, and this happens to be something that can be expressed in a sufficiently powerful type system.
> Well, because the goal is to have guarantees at compile-time
No, that's no one's goal. The goal is to increase correctness as much as possible prior to shipping. BTW, reducing soundness guarantees is all the rage in FM research these days [1] precisely because soundness has a high cost, and it is rarely needed for non-simple, technical properties.
This comment is deeply misleading. O'Hearn's incorrectness logic that you cite in your [1] is perfectly sound. It just changes the meaning of Hoare triples from over-approximation to under-approximation. In brief:
- Hoare logic soundly over-approximates
- Incorrectness logic soundly under-approximates
Sound under-approximation is extremely useful when you want to prove that a certain problem must arise in code, rather than may arise. The problem with logic based program verification has often been that your prover could not prove that a program was correct, but, due to over-approximation of traditional Hoare logic, the best you could learn from this failure was (simplifying a great deal) that something may go wrong. That is not particularly useful in practise, since often this is a false alert.
I am well aware. In software verification, a "sound" verification method usually means no missed bugs. Obviously, the logic is sound in the sense that it cannot be used to prove false statements; in that same sense, tests are also sound, and yet in software verification, tests are considered an unsound verification technique (which, these days, is becoming good).
Tests are not sound in the sense of conventional program logic (overapproximation). O'Hearn's [1] even proves a soundness theorem. So when you say say [1] is not sound then this is confusing for the reader.
> Tests are not sound in the sense of conventional program logic (overapproximation).
Of course they are, in the logic sense of "sound", and in the same sense that incorrectness logic is sound. A test is a proof of a proposition about a single program behavior (provided that the execution is deterministic). But neither testing nor incorrectness logic are sound in the sense that term is used in software verification, namely as proofs of some explicit or implied universal proposition. In software verification, a sound technique is one that guarantees conformance to a specification over all behaviors (or conversely, the absence of spec violations in any behavior).
This strikes me as a pretty bizarre statement. The more checks I can put into the compiler, the less tests I have to write. Tests are also code and come with development and maintenance costs. Since a software project's costs correlate directly with lines of code, the less you can write to get the job done the better.
Type checks done by the compiler and tests that you manually have to write are not the only two available techniques. Again, the goal is not to have the compiler do anything, but to produce software that's as correct as needed for the lowest cost.
As for 3. Haskell already does it now with the IO monad.
I can see how having something more specific for effects than the most generic IO type is the next step on an evolutionary path for languages with an advanced type system. The concern whether or not it is worthwhile then extends to the whole type system.
If you look in the Haskell 2010 report the Goals section states that Haskell was designed for teaching and research and applications (in that order) and that the design committee intended that Haskell would serve as a basis for future research in language design.
Usable for applications here means that it should be stable (_e.g._ so you can write your research tools in it and as a common language for sharing code examples in the academic programming language research community).
Market share in the greater software development area (outside academia) was not one of its goals.
What would satisfy you? And don't you think you are holding Haskell to an unfair standard that you're not holding to other languages?
Do you have research to show a GC is better than manual memory management? That object oriented programming is any better than procedural? Or any of the other thousands of questions you could ask about extant languages today. But for some reason you need rock-solid evidence dependent typing does X before it's worthwhile to be used in an language?
They add significant complexity to the language and are intended to help with correctness.
Not exactly -- they're intended to help with reasoning about the structure of programs and hopefully reject the obviously wrong ones. Correctness would still require a more formal system of validation. Whether this is more easily achieved in a language like Haskell is still an open question. The LiquidHaskell team and Synquid project are both very interesting.
In a Haskell program the compiler trivially rejects programs that fail to provide a branch for a missing case.
I can reason about the scope of what a function can do (and what it cannot) based on it's type information.
I can reason about an equation in familiar terms of substitution and composition.
Types don't automatically ensure my program is correct, for some vague notion of correctness.
Either way, it's not a language that's designed to solve a problem for practitioners
If I am right to assume that practitioners are programmers then I have to disagree with the premise here.
I am not a researcher. I write software for factories to help real people I've met face to face solve real problems.
I have solved pragmatic, real-world problems by writing programs with Haskell and it was a productive, novel experience. The feature I recently shipped to production has migrated nearly a million schema-less JSON documents to a well-defined schema, continuously back-fills the new table from an AWS Lambda function when we receive data in the old format, and was largely only possible to do in such a short amount of time because of the features of Haskell's type system. I haven't had a single bug report or failure in 5 months to boot.
To compare: every single Javascript service we've shipped to production in the last three years, despite all of the testing, validation, and effort we put in to getting it right has at least one production error within three months. Tolerance for these failures has to be built into everything we do.
Haskell is not only suited for research. It is used in Facebook and Github. It has plenty of industrial uses and is definitely designed for and with the aid of practitioners. It's development is largely supported by volunteers: practitioners and researchers alike.
It may not be popular but all it takes is one startup to choose it as their basis to change the conversation. The Viaweb team chose Lisp, arguably as obscure as Haskell at the time, and did great work.
As for dependent types the why is simple: we can express richer specifications in the type system. It would enable Haskell to use a uniform language for terms and types. For programmers the simplest, minimal example are sized vectors as types. You can pass around a vector in Haskell that is sized so that out-of-bounds access is not possible. However the size of the vector is opaque at the type level. With a dependently-typed vector you could specify the bounds of the vector your algorithm supports which further reduces cases where a programmer mistakenly uses your function for unbounded inputs. This is only the minimal example but dependently typed languages scale up from there: there are research languages that have implemented full-on interactive theorem provers and libraries that can encode the whole of mathematical research and knowledge in them: Lean and mathlib. I firmly believe this is where programming is going to go. Dependently typed languages are the next step.
I started writing a guide for interested hackers to get started writing real, working programs in a research-heavy dependently-typed programming language called Lean which you can find here: https://agentultra.github.io/lean-for-hackers/
I suggest giving it a shot before condemning Haskell so easily. There's a lot of promise here.
And in my experience, selling Haskell is a lot easier than selling formal verification, fwiw. Hardly anyone uses TLA+ compared to Haskell. And I spend a fair amount of time and energy trying to sell both.
> working programs in a research-heavy dependently-typed programming language called Lean which you can find here
I have used Lean. It's nice and intersting, but not really a useful tool for software correctness intended for use by engineers. You can do some very interesting math with it, though.
> As for dependent types the why is simple: we can express richer specifications in the type system.
Sure, but why? Expressing richer specifications in the type systems also has a significant cost. A language whose goal is not research would likely spend years considering whether this is a good idea or not.
> I suggest giving it a shot before condemning Haskell so easily. There's a lot of promise here.
I have, and I don't think it's bad, I just don't particularly like it, for the same reasons some people don't particularly like Python or Java. I certainly don't think you can't use it for practical applications, but its evolution is, without a doubt, guided by research goals. And when it comes to promise, I don't know how many decades one can reasonably believe that. Haskell doesn't even spread in companies that are already using it, unlike languages that have contributed a significant bottom-line advantage, and it shows virtually no growth after 25 years, in many of them it was highly hyped. I have absolutely no problem with people who like it. Programming language preference is a matter of personal taste; I like Java, Clojure, Eve, ML and Zig, not crazy about Haskell, and dislike Scala, and others like Haskell and dislike the languages I like; it's perfectly reasonable and expected, like taste in music. But you cannot claim it's a language designed for practitioners and yet have its features guided by research questions.
> Expressing richer specifications in the type systems also has a significant cost.
And everything that has a cost should have a benefit or we would abandon the whole enterprise.
The simply typed lambda calculus will be 80 years old this year, in June. What was Church going after when he published it to the Journal of Symbolic logic? If you go back and read it he was trying to make sense of the lambda calculus. That calculus gave us one branch of computing as we know it but it was not sufficiently expressive enough to make logical statements about different classes of functions: not all functions that have the same shape have the same meaning.
In a similar fashion not all programs are created equal. Given a set of functional requirements by a person we can probably independently write programs that satisfy them. Type theory is simply a means for us to reason about these programs. Whether you write your program that enables you to verify the internal correctness of your programs with respect to the type system used to check it or not doesn't matter one bit to the user of the system. To the programmer however, it can matter a great deal.
Of the programs we could write in languages that don't allow us to verify the correctness of our programs with respect to a particular type theory all we can say is: when I evaluated the program with these inputs at this time, it worked. We can be reasonably certain it will continue to work and it will likely work on more inputs.
Of the programs we write in a language that does allow us to verify the program is logically consistent and sound with respect to a particular type theory is that it is consistent. We would still be obligated to prove that the program meets the specified requirements. But we don't have to worry about whether we forgot to handle a branch, access data that isn't there, over write data we didn't intend to... and a whole slew of things that do plague us in languages without such tools. We can instead focus our effort on proving that we meet the requirements which is a much smaller and more tractable problem.
As an engineer I don't see the reason why theory and research must be separate. I see my work as sitting between both worlds: theory informs application which in turn gives me more problems to inform the direction to go.
> I just don't particularly like it, for the same reasons some people don't particularly like Python or Java.
That's fair, I don't particularly like Java either.
But I don't go into threads about Java and ask Java developers why they bother with it.
Some of the challenges posted by Stephan are legitimately interesting challenges for Haskell programmers. A dependently typed Haskell would, ironically, make Haskell a more simple language and allow us to continue pushing type-driven programming further for many of the benefits I've described. Many of the benefits to these issues have been described in the article.
> it shows virtually no growth after 25 years
I beg to differ. Even after 10 years it has shown a lot of growth. TFA opens with celebrating the advances made in the last decade.
The reason why Haskell isn't as popular as many mainstream languages, if it's so great, is network effects. Javascript is as popular as it is because it was the only language available for a long, long time on a platform many people wanted to write software for. Ruby would not even be on the radar if it wasn't for it's killer app: Rails. I dabbled in Ruby before Rails came along -- it was super obscure -- but no matter how good it was without Rails it would have languished in obscurity, I think. Some languages became popular by sheer force: Java was a solution in search of a problem and Oracle had a war chest to make sure people thought about it. I recall a time with Python was incredibly rare and obscure and had similar network effects to over-come. Haskell doesn't have a company or group of companies pumping millions of dollars into its development, is not a platform exclusive, and so far hasn't had a killer application where it excelled over other incumbents (except perhaps in compilers).
It also doesn't help that many programmers continue to persist FUD about Haskell for reasons I don't understand. Similar to how people feel justified for being contemptuous of Javascript or PHP I suppose.
However if Haskell was the platform-exclusive language of the web for several decades I think this conversation would be completely different.
Haskell is a fine language and the reasons for working on effect systems are good ones and I'm excited to see the results. If you don't get why then try harder to understand the work or find something constructive to say about it. The people working on it are brilliant and have good, practical reasons for it.
I don't know anything about, say Ruby, so I have nothing to say about it. But Haskell is an interesting and elegant language that I know, and I like to follow its progress. I just think it suffers from a split brain in the community. The language evolves to answer research questions that I'm interested in, yet some go out of their way to present it differently.
> And everything that has a cost should have a benefit or we would abandon the whole enterprise.
Yes, but that brings me to the point in the linked comments. We are interested in the question correctness => dependent types not dependent types => correctness. The answer to why Haskell should add dependent types is that it's an interesting research question, and that Haskell is designed to answer research questions.
> As an engineer I don't see the reason why theory and research must be separate.
They are separate because the concerns of engineers and researchers are vastly different. A researcher studies X and wants to know what X can do. An engineer wants to know the best way of doing Y. Not to mention that out of every 100 things in research, maybe one will ultimately, after years of engineering, will result in a solution engineers need. How do I know which one is it? I love both engineering and research, but the two are very far apart.
> But I don't go into threads about Java and ask Java developers why they bother with it.
If you were interested in Java then perhaps you should. BTW, I didn't ask why people who use Haskell bother with it. They do it for the same reason people use any non-popular language: they like it. I ask what they think the language is and why it is clearly one thing and yet they insist on presenting it as another. Haskell also suffers from a terrible evangelism disease, where its evangelists don't say things like "I really like Haskell, here's why, and perhaps you should to" but also make incorrect empirical claims about things I know a little about, like software correctness.
BTW, HN isn't a forum for Haskell fans, and anyone can say anything, as long as it's reasonable. I don't go to Haskell forums and discuss my problems with its community because I'm not in the target audience of those forums, but I think I am in HN's. This particular post is at the top of /r/Haskell right now, where it's being discussed by an exclusive group of Haskell fans.
But don't take what I write on social media too seriously. I don't. I think Haskell is a perfectly fine programming language, and it rightly has some fans.
> The answer to why Haskell should add dependent types is that it's an interesting research question, and that Haskell is designed to answer research questions.
Interesting, yes, but I believe it will also have practical benefits for engineers using the language as well.
I hope Haskell will migrate to dependent types because it will unify the language. Some of the more frustrating features of Haskell are due to it having a separate language for types and terms. When people see a huge list of language pragmas and the singleton libraries being pulled out this is what I hear people frequently complain about when they say Haskell is too complicated. If you can remove the barrier between types and terms then most of that added complexity goes away.
A good example of this is Lean. It's implemented in a dependently typed programming language because it unifies types and terms which makes writing the compiler and programs more simple. I think this could also be extended to Haskell.
It will be difficult, and presented as a "grand challenge," because unlike Lean, Haskell has many more libraries and applications that depend on it and we all know how breaking compatibility goes.
> They are separate because the concerns of engineers and researchers are vastly different.
In the twenty some years that I've been fortunate enough to write software for a living I don't believe this is true. I find that in software engineering that research and application inform one another and have a tight feedback loop. I read papers and often I implement them to help solve problems. Often in implementing that research I find feedback to give the authors or I find new problems that require some research in order to solve.
Pure mathematicians have it a bit harder. I lament that John Conway may never live to see the solution to some of the problems he's posed.
But I think we have it pretty good. The logicians have done most of the work for us. And we can implement new theories quite fast.
BTW I'm not saying you can't comment on or criticize Haskell, this is an interesting discussion. I am a little sensitive to people being contemptuous of the hard work others put into Haskell and was probably either misreading your comments or responding to that. For the people that do work on Haskell I think these are the great challenges for us to solve this decade. Algebraic effects have been used in production at Github and elsewhere and there's still work to do to make them shine but it's generally good stuff and moving in a positive direction. Same with dependent types.
Regardless, thank you for being patient. I appreciate your work and your writing here and elsewhere. All the best.
> A good example of this is Lean. It's implemented in a dependently typed programming language because it unifies types and terms which makes writing the compiler and programs more simple. I think this could also be extended to Haskell.
If in the next fifty years more than, say, 3% of programmers will be programming in a language like Lean, I will eat my hat. Take a Haskeller's favorite, simplest "function", id, and look at its Lean definition (as you know the universe polymorphism is required for consistency):
universe u
def id {α : Sort u} (a : α) : α := a
Now, try to explain to a programmer what kind of object id is (not why the definition must be this way, but what is it that it defines). And it's not as if there is some hidden universal mathematical truth about programming here; this is an unecessary complication due to Lean's chosen foundation, which was chosen not with the best interests of programmers in mind (which I know because I discussed this with Jeremy Avigad). In fact, few if any of Lean's author have any significant experience in software development in industry, or in software verification, and they made an error in their introductory paper that anyone with any experience with software correctness would immediately spot. Lean is fun in its special way, but I think it's a horrible, if entertaining, way to write programs.
> I find that in software engineering that research and application inform one another and have a tight feedback loop. I read papers and often I implement them to help solve problems.
That's not what I meant, though. Of course research and practice enrich one another. But their goals and concerns are drastically different. It is rarely the case that an interesting research question is a recommended practice for practitioners. In fact, the more interesting something is to a researcher, the less likely it is to be a good idea for a general recommendation for practitioners.
The short of it is: network effects. Haskell, OCaml, SML... they've never had the benefit of being the exclusive language to a popular platform like the web, macOS, or UNIX. They've not yet had a killer app like Rails or Numpy/SciPy/PyTorch. They've certainly not been foisted on the market with a war chest of marketing dollars like Java and C#. And they're not an incremental improvement on the status quo with an obvious, easy benefit.
> Now, try to explain to a programmer what kind of object id is
That's a rhetorical exercise. You can take a random snippet of APL or Fortran and the outcome would be the same. Every language requires training and effort to learn.
I teach people Haskell and TLA+. If you think teaching people the value of a language like Haskell is hard you should see the blank stares I get on the first day teaching experienced developers TLA+. Interested folks will come around eventually and have their moment but it takes training and dedication to get there.
> was chosen not with the best interests of programmers in mind
I'm well aware. I converse regularly with the maintainers of mathlib and the community. I know the focus there is on building a good tool for mathematicians.
I still think they built an interesting programming language even if that wasn't their intended purpose. That's why I started writing the hackers' guide. The documentation on the programming side is missing and needs to be filled in. They still need programmers to build the tools, the VM, the libraries, etc.
It's niche. And I'm not even the least bit surprised you find it horrible. I don't expect Lean to take off with programmers. I think the ideas in it are good and there is definitely some good things we could take from it in designing the dependently typed programming language that does penetrate the market and over-come the network effects.
Either way I think the people proposing the challenges for Haskell programmers to solve have a good reason to do so otherwise we would have a hard time finding the motivation for it. We want to see where algebraic effects go because new users often complain that monad transformers are hard to learn and users of mtl cite many problems that a well-done algebraic effect system would alleviate. Dependent types would remove the complexity of writing programs that work with types and enable us to write more programs with more expressive types. If you don't see why that's useful then what do you think the community should be focusing on?
> There's a great talk on why functional programming is not the norm
It's a great talk in the sense that it satisfies people who want excuses. The real reason is similar to the one in the talk, but more disappointing: over decades, functional programming was not found to be either significantly better or significantly worse than other paradigms in productivity or other similar metrics, but for many years imperative paradigms enjoyed a significant benefit in runtime performance, and so there's really no reason to switch. I honestly couldn't care -- I like, and hate, OOP and FP equally -- but paradigms exist to serve practitioners, not the other way around.
One thing is clear: you cannot at once say you're interested in serving the research of typed lambda calculus -- a worthy research goal -- and also in advancing the state-of-the-art in the software industry, which is another worthy goal, but a very different one. If you're interested in the latter you must conduct some sort of study on the problem at hand; if you're interested in the former, then you have zero information to make a claim about the latter. In other words, you can either want to advance programming or advance typed FP; you cannot do both at once, because doing they both require very different kinds of study. If you're for typed FP, then that position is no less valid than being for OOP, or any other paradigm some people like, but it's not more valid, either.
> And they're not an incremental improvement on the status quo with an obvious, easy benefit.
... or at all.
> That's a rhetorical exercise. You can take a random snippet of APL or Fortran and the outcome would be the same.
I totally disagree here. Simplifying ideas makes you understand what is essential and what isn't, and is absolutely required before some idea can get out of the lab and become a useful technology in the field. If the most basic subroutine represents some object in a meta-universe, that even 99% of mathematicians have no clue about -- you're off to a bad start with engineers. The use of constructive type theory as a foundation is interesting to logicians who want to study the properties of constructive type theories and of proof assistants based on them. It is nothing but an unnecessary complication for software developers. As you point out, there are often some necessary complications, so there's really no need to add unnecessary ones.
BTW, you mentioned TLA+. TLA+ also requires some effort, although significantly less than Lean (or Isabelle, or Coq), but TLA+ has made a historical breakthrough in formal logic. From its inception in the late 19th century, and even from its first beginnings in the 17th, formal logic aspired to be a useful tool for practitioners. But time and again it's fallen far short of that goal, something that logicians like John von Neumann and Alan Turing bemoaned. AFAIK, TLA+ is the first powerful (i.e. with arbitrary quantification) formal logic in the history of formal logic that has gained some use among ordinary practitioners -- to paraphrase Alan Turing, among "the programmers in the street" (Turing said that formal logic failed to find use for "the mathematician in the street," and tried, unsuccessfully, to rectify that). It was no miracle: Lamport spent years trying to simplify the logic and adapt it to the actual needs of engineers, including through "field research" (others, like David Harel, have done the same). That is something that the logicians behind other proof assistants seem to be uninterested in doing, and so their failure in achieving that particular goal is unsurprising.
> Every language requires training and effort to learn.
... Interested folks will come around eventually and have their moment but it takes training and dedication to get there.
But why get there at all? I'm interested, I learned some Haskell and some Lean, I think Haskell is OK -- not much better or much worse than most languages, but not my cup of tea -- and Lean is very interesting for those interested in formal logic, but offers little to engineers; I enjoy it because I'm interested in some theoretical aspects. But why would I subject other developers who aren't particularly interested in a certain paradigm to suffer until they "get there" just for the sake of that paradigm? Again, paradigms exist to serve practitioners, not the other way around.
> If you don't see why that's useful then what do you think the community should be focusing on?
I think the community should be honest about what Haskell is: a testing ground for ideas in the research of typed functional programming. Then, it should consider measuring some results before disappearing down its own rabbit hole, where it's of little use to anyone. Algebraic effects could be an interesting experiment at this point. I don't really care about the pains of all 300 Haskell developers with monad transformers, but if Haskell tries another approach to IO, then it might eventually find a generally useful ones; same goes for using linear types instead of monads. But dependent types? They're currently at the stage when even their biggest fans find it hard to say more good things about them than bad. If Haskell wants to serve software by testing out new ideas in typed functional programming, I think it should at least focus on ones that might still be in the lab but are at least out of the tube.
> BTW, you mentioned TLA+. TLA+ also requires some effort, although significantly less than Lean (or Isabelle, or Coq), but TLA+ has made a historical breakthrough in formal logic. From its inception in the late 19th century, and even from its first beginnings in the 17th, formal logic aspired to be a useful tool for practitioners. But time and again it's fallen far short of that goal, something that logicians like John von Neumann and Alan Turing bemoaned. AFAIK, TLA+ is the first powerful (i.e. with arbitrary quantification) formal logic in the history of formal logic that has gained some use among ordinary practitioners -- to paraphrase Alan Turing, among "the programmers in the street" (Turing said that formal logic failed to find use for "the mathematician in the street," and tried, unsuccessfully, to rectify that).
I will bet you 100 USD that TLA+ had less than 10% of the users of Z before the AWS paper.
> It was no miracle: Lamport spent years trying to simplify the logic and adapt it to the actual needs of engineers, including through "field research" (others, like David Harel, have done the same). That is something that the logicians behind other proof assistants seem to be uninterested in doing, and so their failure in achieving that particular goal is unsurprising.
I will bet you another 100$ that the success of TLA+ has nothing to do with making it "accessible" and everything to do with AWS vouching for it. If reaching the actual needs of the engineers was so important, why is the CLI tooling in such a bad state?
So what? TLA+ still achieved something that no other formal logic had before it (AFAIK). If you mean to say that Lean could do the same, I think spending a month with it will dissuade you of that notion, despite the fact that it is more similar to programming and despite it more programming-like tooling that programmers of certain backgrounds might appreciate.
Amazon may not have used TLA+ if not for TLC, but very good model checkers have existed for decades, have been used successfully in industry, and still have not made any inroads into mainstream software.
> If reaching the actual needs of the engineers was so important, why is the CLI tooling in such a bad state?
For one, resources are limited. For another, you assume that the best place to invest effort in order to help developers is in CLI tooling. I, for one, disagree. I think building a model-checker that works well is a higher priority; I also think that designing what is possibly the first "utilized" logic in the history of formal logic is also more important. Even with those two, there are other things that I think deserve more attention, because I think TLA+ has much bigger problems than how you launch some program.
I also think that some of the complaints about the tooling might be about something else altogether, but I'm not entirely sure what it is. Simply doing what beginners think they want is rarely a good strategy for product design. You get the feedback, but then you have to understand what the true issue is. Having said that, there can certainly be some reasonable disagreement over priorities.
> So what? TLA+ still achieved something that no other formal logic had before it (AFAIK).
What I'm saying is that either TLA+ wasn't the first (Z was earlier), _or_ TLA+'s success has much less to do with anything especially accessible about it and more because a high profile company wrote about it.
> because I think TLA+ has much bigger problems than how you launch some program. [...] I also think that some of the complaints about the tooling might be about something else altogether, but I'm not entirely sure what it is. Simply doing what beginners think they want is rarely a good strategy for product design. You get the feedback, but then you have to understand what the true issue is
When I asked "what would make TLA+ easier to use", tons of people mentioned better CLI tooling. You told them all that they don't actually need that and they are thinking about TLA+ wrong. Maybe you aren't actually listening to the feedback.
I've also heard it from tons of experienced TLA+ users that they'd like better CLI tooling.
Was Z ever used outside high-assurance software (or the classroom)? BTW, while Z certainly employs a formal logic, I don't think it is a formal logic itself -- unlike TLA+ -- at least not in the common usage of the term.
> TLA+'s success has much less to do with anything especially accessible about it and more because a high profile company wrote about it.
But for a high-profile company to write about it, it first had to be used at that high-profile company for some mainstream software. My point is that being an accessible logic may not be a sufficient condition for adoption, but it is certainly a necessary one, and an extraordinary accomplishment. Both Isabelle and Coq have had some significant exposure, and yet they are still virtually unused by non-researchers or former researchers.
> When I asked "what would make TLA+ easier to use", tons of people mentioned better CLI tooling.You told them all that they don't actually need that and they are thinking about TLA+ wrong. Maybe you aren't actually listening to the feedback.
Maybe, but "listening to feedback" is not the same as accepting it at face value. The vast majority of those people were either relative beginners or not even that. To understand the feedback I need to first make sure they understand what TLA+ is and how it's supposed to be used, or else their very expectations could be misplaced. I've written my thoughts on why I thought the answer to that question is negative here: https://old.reddit.com/r/tlaplus/comments/edqf6j/an_interest... I don't make any decisions whatsoever on TLA+'s development, so I'm not the one who needs convincing, but as far as forming my personal opinion on the feedback, what I wrote there is my response to it. It's certainly possible that either my premise or my conclusion is wrong, or both. It's also possible that both are right, and still better CLI support should be a top priority. That is why I would very much like to understand the feedback in more depth. If you like, we could continue it on /r/tlaplus (or the mailing list), where it will be more easily discoverable.
> I've also heard it from tons of experienced TLA+ users that they'd like better CLI tooling.
Sure, but the question is, is that the most important thing to focus efforts on? Anyway, I'm sure that any contribution that makes any part of the TLA+ toolset more friendly, even if for a subset of users, would be welcomed and appreciated by the maintainers, as long as it doesn't interfere with what they consider more important goals.
> and also in advancing the state-of-the-art in the software industry, which is another worthy goal, but a very different one.
The state of the art doesn't advance until practitioners share the results of adopting new techniques and tools. How else would the SWEBOK guide [0] have a section on unit testing if, in study, we don't have results that correlate the practice of TDD with a reduction in software errors, productivity, or some form of correctness? Is it irrational of us to practice TDD anyway?
How do we know formal methods are effective if there hasn't been a large scale study?
An interesting example of this balance between research and practice came to me from learning about the construction of cathedrals, particularly the funicular system of Guadi [1]. Instead of conventional drawings he used hanging models of the structures. It was not widely practiced or a proven method but it enabled him to reduce his models to 1:10th the scale and accurately model the forces in complex curves. As he shared his work and others studied it the state of the art advanced.
> .. or at all.
> I think Haskell is OK -- not much better or much worse than most languages, but not my cup of tea -- and Lean is very interesting for those interested in formal logic, but offers little to engineers
I think we're at, or approaching, the point where we're talking past each other.
I heard the talk from the Semantic team at Github on their experience report with algebraic effects sounded positive [2]. They are probably the largest production deployment of a code base exploiting algebraic effects. Their primary area of focus is in semantic analysis of ASTs. And yet they would like to continue pushing the state of the art with algebraic effects because, in their words, In Haskell, control flow is not dictated by the language, but by the data structures used. Algebraic effect interpreters enable them to interpret and analyze unsafe code without having to maintain buggy, difficult to reason about exception-based work flows. They say this singular feature alone is essential for rapid development.
Yes, they're doing research. However their research isn't in answering hypothesis about effect interpreters. It's directly contributing to an interesting feature in one of the largest code-sharing platforms in the world. They were able to exploit algebraic effects so they could focus on their research, their real-world problem, without having to fuss around with the limitations of conventional mainstream languages.
I do wish more companies using Haskell would share their experiences with it. It would go a long way to dispelling the pervasive view that Haskell is only good for research. It's not: it's a practical, production ready language, run time, and ecosystem that can help anyone interested in using it to tackle hard problems.
In a similar fashion I think dependent types would make working with types in Haskell easier. Instead of having to learn the different mix of language extensions you need to enable in order to work with inductive type families, it could be more like Lean, where it's a normal data declaration. Haskell introduces a lot of extra concepts at the type level because it has two different languages. I can simplify a lot of code in libraries I've written if Haskell had dependent types (and I'm working on libraries in Lean that may eventually prove it).
It may take a while but I think Haskell will eventually get there. The community has been discussing and researching it for years. It's going at the pace it is because the Haskell community is not focused on pure research: there are a lot of production applications and libraries out there and they don't want to break compatibility for the sake of answering interesting research questions. Despite your opinions on type theory there's a real, practical reason I might exploit Rank-2 types or Generalized Algebraic Data Types and it's not simply to answer a pressing hypothetical question: I've used these in anger.
I hope some of this answers your questions as to why get there at all?
What I'm trying to say is simple: personal aesthetic preference, empirical results and research questions are all very important, and every one of them is a reasonable motivation for making decisions, but they are very different from another, and should not be conflated.
As to Haskell, it is definitely production-ready, and usable in a variety of circumstances. Also, its design and evolution are just as definitely primarily guided by research goals. These two simple, obvious, facts are not in opposition to one another. I have read numerous articles on why some people like Haskell, or many other languages. They are very important: some people like the tracking of "side effects"; some enjoy the succinctness. None of those articles, however, have any bearing on other questions. Which are not necessarily more important, but they are very different.
Lean. It's implemented in a
dependently typed programming
Lean is implemented in C++ [1, 2]. There's a message in there somewhere. The message is probably something along the lines of: if you want performance, use a low-level language.
I'm aware, I have a branch implementing C FFI for Lean 3; my point was that it's logic, mathlib could be implemented in system F instead. I'm pretty sure Lean could be implemented in Lean eventually.
What do you mean by "it's logic, mathlib could be implemented in system F"? System F is not dependently typed!
Anyway, nobody doubts that Lean's logic is a dependently typed formalism: "Lean is based on a version of
dependent type theory known as the Calculus of Inductive Constructions" [1]. I thought the discussion here was about using dependent types in programming languages. Note that logics and programming languages are not the same things.
[1] J. Avigad, L. de Moura, S. Kong, Theorem Proving in Lean.
That's an interesting question: can Lean be implemented in Lean's dependent type theory.
I'm not currently working with Lean, but I will start a large verification project in a few months. We have not yet decided which prover to go for. We may write our own.
Exactly. I find it revealing that having some moderately visible successful software does not feature on this list. Even ocaml does, IMO, better here (bits of mirageOs for non-linux docker; Xen; unison, coq, at least one successful ocaml only company) vs what, pandoc and shellCheck?
Haskellers are in a rough spot, then, aren't they?
All of the pretension that comes with knowing one of the functional languages that has a community that pretends to know math, and they end up working retail. Ow.
Joking diss aside, though, I definitely feel for people who love languages with limited reach.
(Also, I think GitHub hired a few people explicitly for Haskell, which is worth mentioning because Microsoft is vaguely more reputable than most of the companies listed in this thread.)
You must know how bad of a reputation cryptocurrencies have at this point, right? They aren't exactly loved, especially around these parts. Cardano (which I'm assuming is what IOHK works on) may be different, it might not be, but either way it has an uphill climb to be recognized as anything better than, well...
I can't answer his "so what", I was just trying to clarify what was left implicit in this conversation (if not for you, then maybe for readers who don't know).
Apologies if my comment felt offending. I've just seen a few stories about companies using non mainstream tools for important matter without making a product out of it. Caring only about known programs made in <lang> is shallow IMO
Well, to my mind the fact that Haskell has a large amount of mind share in academia and smart programmers, has been around for decades and there is very little to show for it[*] that I'm aware off makes me think it almost certainly has negative average utility for developing useful software. Why would you think otherwise? I'm not saying it will necessarily have negative utility for your particular problem, or that the negative utility it has might not be a cost worth swallowing in order to hire some really smart programmers who happen to like it.
I don't understand your argument, in that I really can't see how one can equally argue the opposite. I fully acknowledge that Haskell has been successful as a test bed for PL research, and I also think Haskell is an interesting language worth studying. It is also true that FP ideas have increasingly bled into mainstream languages over the past two decades. But that does in no way imply that Haskell is in any way a good general choice for writing useful software.
And although a lot of practically useful stuff has come out of Haskell-land (property based testing, for example), it's not even obvious to me that Haskell has been a huge part of the shift to more FP-y idioms (compared, to say, scheme or SML). Your own example, fold, has been around decades before Haskell.
What can I say, I didn't read why es6, php or cpp lifted closures into the language. I consider this is pure FP influence which haskell is the most known instance. And yeah scheme and sml were prior art, but sml is not even on the map of PL choices (I saw it mentionned in rust history, but I think it's mostly the eager semantics, otherwise you could replace it with any pure FP language)
What do you mean with es6 lifted closures into the language? As far as I remember, closures have been in JS right from the start (and given that Brendan Eich joined mozilla to "do scheme in the browser", we can be pretty sure where they came from). ES6 just added a more lightweight syntax.
I agree that SML isn't even on the map, in terms of practical programming language choices (one of the most hilariously titled CS books of all time must _ML for the working programmer_ where the final "real project" chapters consist of writing such working programer perennials as a lambda calculus interpreter and a theorem prover). And I believe that even scheme is less suited to write almost any type of practical software than Haskell. But that's precisely my point: a language having a positive influence on the state of applied programming does not mean that it is actually a good choice for solving practical problems with. And vice versa.
You're right, I just meant the lexical closure syntax (..) => (giving a clear fp feel to the language by promoting closure syntactically). and this is part of a wide move from all dyn langs to lift fp features like destructuring. es6 was just one tiny point that I had in mind when commenting above.
btw I love sml. I'm just being realist about it's mainstream existence.
Lastly, it's as if you consider haskell as proof of concept and nothing more. I don't see any real hurdles why haskell is less practical than typescript (except the fact that TS relies on the years of js project they can compile and interop with)
How about: a typical typescript project does not start off with a dozen compiler pragmas non-trivially changing language semantics? Or: no matter their background, it will take at least 10x more time to spin up new developers with Haskell than typescript?
Haskell language extensions do not change the language semantics. They extend the semantics with additional functionality. Existing code does not change its meaning when you enable an extension.
Ah, great counterexample! StrictData is another. Do you
know any others that change language semantics
non-trivially? I would roughly define "non-trivially" to
mean "correct programs become incorrect".
There’s also QuasiQuoter which can make valid code with list comprehensions not compile, but it doesn’t just compile it, it gets stuck looking for the end tag.
Not sure if that qualifies :P
If a language is used at a company and its use is not spreading rapidly within that company (as has happened with Fortran and C and Java/Python) you do ask yourself, is the language actually serving a business purpose, or is the business serving a "language purpose" by giving some fans their entertainment? I can't think of a worse signal for a language's value, or perhaps the size of its useful domain, than it being used for years at a company without spreading.
Mild point, there's no way a single language would suddenly progress through all layers no matter what its qualities.
I understand your question though, it's highly possible that the devs picked haskell for their own interest. But so far it's been a few years and the haskell "module" is dealing with the core of their business.
> there's no way a single language would suddenly progress through all layers no matter what its qualities.
Except that's exactly what languages that provide a business value do (like the ones I mentioned). Maybe not always in all layers, but they tend to fill a big, wide niche at a company very quickly.
Read up on logical fallacies.
You claim Haskell is how language and then point out how stupid it is.
But we only have your word that Haskell indeed is how language.
Show your proof ;)
Which is why although I see these kind of languages quite relevant to advance the state of the art, the industry belongs to impure multi-paradigm languages.
Like Brian Goetz puts it, it is not FP vs OOP, rather combining FP and OOP, using the best of each to solve different kinds of problems with the same tool.
I'm not so sure a multi-paradigm language is truly the ideal alternative. Languages that brag being multi-paradigm, such as Python or Javascript, in the end offer very few facilities for actual functional programming. It just doesn't feel idiomatic with them.
FP and OOP are both well tested design patterns. Mixing them up in an incoherent way just makes the whole software architecture somewhat unpredictable.
One could perhaps draw a distinction between languages that were designed from the ground up as multiparadigm, such as OCaml, and languages that originally targeted one paradigm and then became multiparadigm by katamari-ing up a bunch of extra features, as Python did.
FWIW, I also don't know that Python officially conceives of itself as multiparadigm so much as as a procedural language with classes. Kids these days forget that higher-order programming has a long history in procedural programming, too. ALGOL was doing it in the 1960s, after lisp but a good decade before Backus published Can Programming Be Liberated from the von Neumann Style?.
For what it's worth, despite the O in OCaml, in practice the object layer isn't used that often. However, that's because the ML module system serves many of the same use cases that objects and classes do in other languages. People do use objects in OCaml occasionally if they need the dynamic dispatch.
I'd say that OCaml blends imperative and functional programming cohesively and fairly equally, though.
The python leadership commitee has always been explicitly anti "functional programming". They only allow a few functional things that serve Python's overall goal of making basic problems simple to solve.
Combining FP and OOP is not a practical goal in and of itself, either (although it is a research goal for other languages led by researchers, such as Scala). At best, it's a means to some end, and Brian Goetz treats it as such. He cares more about the why than the how.
Some problems get better solved as a set of classes, others as functions operating across data alongside pattern matching, and yet others are happy to take lambdas as callbacks.
Many of the anti-OOP crowd doesn't realize how much OOP is already available on Common Lisp, that Smalltalk-80 already allowed for a good LINQ like mix with its blocks and collection methods, or how SML modules can be combined to make what isn't much different from interface based polymorphism.
It is a matter of having a nice toolbox instead of just a hammer. :)
I'm not arguing for languages like Go. I'm saying that Go code will be forever difficult to reason about, no matter what future features they decide to add to it.
Using Haskell as another example, it has grown immensely, but never compromised on purity.
Why? Monads [from category theory] were [applied in comp sci] as a way to give imperative programs formal semantics. Making use of them to retain referential transparency in the presence of effects is probably Haskell's greatest success. [Edited for clarity].
Monads are just one of many ways of formalizing notions of state. All of them have their tradeoffs. For example, in temporal logic it's much more obvious that "state does not compose" due to the frame problem.
Please don't say "referntial transparency" because it doesn't mean what some Haskellers think it does. It means the following: an expression e is referentially transparent if any sub-term in it can be replaced with any other having the same reference (aka denotation) without changing e's reference. This is true for Java, and most programming languages, really, but, incidentally, not true for Template Haskell (or any language with macros). Referential opacity or opaqueness increases the expressiveness of the language, which is why Lisp, which is not transparent because of macros, is more expressive than the lambda calculus (which is), and why modal logic is so expressive. It's an interesting property, but it's not what pure-FP fans think it means. What they mean is that the language is referentially transparent (like most language) and a term's reference (denotation) is an object value in the language -- this is not true in imperative language where terms refer to something called "predicate transformers". This quality is also called "value semantics" which is pretty much a synonym for "pure functional." In other words, some FP fans have redefined referential transparency to mean pure functional, and then use "referential transparency" incorrectly as some more general thing, when they actually just mean "pure functional."
And yes, monads are a way to express some non-deterministic computations in lambda-calculus-based languages, as are linear types.
> Haskell's greatest success
Success in what sense? In expressing what amounts to side-effects in a language based on a lambda calculus as monads? Sure.
Monads are from category theory, so at most they were adopted, not developed.
They are a workaround, because by definition purity implies that nothing changes in the world.
I can run the same Haskell program multiple times, and it might eventually produce different values as output given the same input values, e.g. an URL or file handle.
Are you referring to how an online document or a file might change so that Haskell program might have a different output given the same URL as an input?
As @willtim explains, monads were applied to PL theory to model effects. The IO monad models the effect of state, i.e. imperative programs. The type `IO a` is essentially a "wrapper" or "alias" for the type `RealWorld -> (RealWorld, a)`. You should think of the entire world as being the input to a Haskell program.
Haskell does have impure backdoors into IO such as unsafePerformIO, but the IO monad itself is perfectly pure.
P.S. For more information, check out the work of Eugenio Moggi [0], who started using monads to give semantics to programming languages, and Philip Wadler [1], who applied the idea on a programmer-facing level.
Haskell is and has always been primarily a research language. It just has some popularity outside the academia. This is something everybody investing into Haskell knows (or should know).
That's not what the author of the article seems to think, though. He admits that "Haskell is never really going to be a mainstream programming language," but even non-mainstream languages, like, say, Erlang or Clojure are very much concerned with the why, and aren't aimed at research. A research language and a non-mainstream language are two very different things.
> “ Many of the large tech companies are investing in alternative languages such as Swift and Julia in order to build the next iterations of these libraries because of the hard limitations of CPython.”
I would be interested in evidence of this. I work at a big tech company in ML and scientific computing, and have close peers and friends in similar leadership roles of this tech in other big companies, FAANG, finance, biotech, large cloud providers, etc.
I am only hearing about the adoption of CPython skyrocketing and continued investment in tools like numba, llvm-lite and Cython. At none of these companies have I heard any interest in Julia, Swift or Rust development for these use cases, and have heard many, many arguments for why Python wins the trade-offs discussion against those options.
In fact, two places I used to work for (one a heavy Haskell shop and one a heavy Scala shop) are moving away from those languages and to Python, for all kinds of reasons related to fundamental limitations of static typing and enforced (rather than provisioned) safety.
I mean, Haskell & Scala are great languages and so are Julia & Swift. But even though in some esoteric corners people have started to disprefer Python, it’s super unrealistic to suggest there’s large movement away from it. Rather there’s a large move to it.
It reminds me of the Alex Martelli quote from Python Interviews,
> “Eventually we bought that little start-up and we found out how 20 developers ran circles around our hundreds of great developers. The solution was very simple! Those 20 guys were using Python. We were using C++. So that was YouTube and still is.”
I work in HFT and now use Julia for all my research, and a couple of my colleagues now do too. Personally I'd rather retire and farm goats than go back to having to write Python professionally: there's just soo much that can go wrong that doesn't happen in a typed language, so much unnecessary stuff you have to keep in your head when coding. It also seems incredibly counterproductive to use a language that's 100x slower than necessary just because it's the only language some people know; the difference in research speed between having to wait one second for a result and ten minutes is massive.
Of course, HFT is a somewhat different usecase than pure ML, as we work with data in a format that's rarely seen elsewhere (high-frequency orderbook tick data). Python's probably less painful for working with data for which somebody else has already written a C/C++ library with a nice API, as then you don't need to write your own C/C++ library and interface with it. My choice is either: write Python, and the research will take 100x longer, write Python and C++, and the development will take 2-4 times longer, or write Julia, and get similar performance to C++ with even faster development time than Python.
Is it just performance that puts you off Python? If so, did you try writing a native extension to accelerate it?
Where i work, we also have analysis work which involves sequentially reading gigabytes of binary data. We came up with a workflow where a tool written in Java runs a daily job to parse the raw data and write a simplified, fixed-width binary version of it, then we have a small Python C extension which can read that format. We can push a bit of filtering down into the C as well.
This has worked out pretty well! We get to write all the tricky parsing in a fast, typesafe language, we get to write the ever-changing analytics scripts in Python, and we only had to write a small amount of C, which is mostly I/O and VM API glue.
The Java and C parts were both written by an intern in a month or two. He's a sharp guy, admittedly, but if an intern can do it, i bet an HFT developer could too.
>Is it just performance that puts you off Python? If so, did you try writing a native extension to accelerate it?
This is what I did originally, but it was way slower to have to write and maintain C++ and a Python interface for it than to just write Julia. Particularly because the some of the business/trading logic basically has to be in the native layer (can't backtest a HFT algo without running it on HFT data, and that volume of high frequency tick data is too slow to process in pure Python).
One of the close colleagues I was alluding to also works in HFT and they do in fact use Cython libraries built in house for extremely low latency applications, order book processing, etc.
Their main alternatives are coding in C++ directly or wholesale switch to Rust, but they prefer Cython. I know they evaluated Julia and found it entirely intractable to use for their production systems.
I'm curious why they found Julia intractable. In my experience it's much quicker to write than Rust, C++ or Cython. It's also much more expressive than Cython.
Is it because they tried embedding it in C++? That can be painful, because it needs its own thread, and can only have one per process, but it's certainly doable.
I’m not sure what you mean by saying Julia is more expressive than Cython, given that Cython is as expressive as C.
In this shop’s particular situation, it’s mostly the switching costs to Julia that cause it to lose the debate. The firm has lots of systems software, data fetchers, offline analytics jobs, research code, etc. With Python & Cython, they easily write all of it in one ecosystem, build shared libraries that span all these use cases, rely on shared testing frameworks, integration pipelines, packaging, virtual envs, etc.
If Julia offered some kind of crazy game changer advantage that required a huge amount of effort to get in Python/Cython, they might consider breaking off some subsystem that has to have new environment management, new tooling, etc., and is not sharable across as many use cases.
But there is no such case. They might get some sort of “5% more generic” or “5% benefit from seamless typing instead of a little rough around the edges typing in Cython”, and these differences would never justify the huge costs of switching or the missing third party packages that are heavily relied on.
I always like to remind people that in any professional setting, ~95% of the software you write is for reporting and testing, and 5% at best is for the actual application. Out of that 5%, another 95% never has serious resource bottlenecks and taking care to write super careful optimized code for the 5% of the 5% can be done in nearly any language. Choose your ecosystem based on what best solves your problems in that other 99.75% of cases.
This is especially true in HFT and quant finance, which is why so many of those firms use Python for everything except the 0.25% of the code where performance is insanely critical, they just use anything that super easily plugs into Python, usually C++ or Cython.
>I’m not sure what you mean by saying Julia is more expressive than Cython, given that Cython is as expressive as C.
I mean expressive in the sense of how much you can get done per unit code/time. Perhaps a better way of phrasing it: for most problems X that I encounter in my work, I can write code in Julia to solve X faster than I could write C/C++ to solve x, and also faster than I could write Cython to solve x. Excellent type inference is a big part of this, along with macros, multiple dispatch, and libraries designed with performance in mind (e.g. https://juliacollections.github.io/DataStructures.jl/latest/...).
>In this shop’s particular situation, it’s mostly the switching costs to Julia that cause it to lose the debate. The firm has lots of systems software, data fetchers, offline analytics jobs, research code, etc. With Python & Cython, they easily write all of it in one ecosystem, build shared libraries that span all these use cases, rely on shared testing frameworks, integration pipelines, packaging, virtual envs, etc.
>I always like to remind people that in any professional setting, ~95% of the software you write is for reporting and testing, and 5% at best is for the actual application. Out of that 5%, another 95% never has serious resource bottlenecks and taking care to write super careful optimized code for the 5% of the 5% can be done in nearly any language. Choose your ecosystem based on what best solves your problems in that other 99.75% of cases.
That makes sense then. In my firm at least (and in my team at least) the case is different: we're mostly full stack, so each member will be responsible for the whole pipeline from research->model_development->backtesting->production_algo_development->algo_testing/initial_trading. In this case 95% of my time is spent writing research code, running research, and writing production code, so if I can double the speed at which my research code runs or double the speed at which I can write it, that translates into a massive increase in my productivity/output.
Did you find something better than tensorflow+python by any chance? I'm desperately looking for something that is mature, stays in loop and does not require me to touch python.
Depends what you're trying to do, but Flux.jl is pretty nice: https://github.com/FluxML/Flux.jl . Failing that, the Julia Python FFI is very good, so it's possible to use PyTorch almost seamlessly in Julia (I previously used Tensorflow 1.x, and it was such a painful experience I'm not brave enough to touch 2.0).
Complexity matters. Python originally had success because it was easy to use. It was one of the first languages I learned after C++ to just get stuff done.
People are not leaving Python for Haskell, Rust, Swift and Scala because those languages are too complex to deal with.
However what we see time and again is that languages that are easy to use and which offer real advantages gain adoption. Look at the rising popularity of Go as a good example.
This is why I belive Julia has a real chance against Python. It hits all the right checkboxes: It is easy to learn, simple tools, while also being highly productive and giving great performance.
Sure Python is not suddenly going to get knocked off the crown. But the fact is that Julia has far more growth potential. Packages are built faster as there is no need for C/C++. Packages are combined way easier due to multiple dispatch and lack of C/C++ dependency. This is a hard one to explain in a short text but Julia has a unique ability in how packages can easily combine. Hence with a couple of Julia packages you get squeeze out the same functionality as a dozen Python packages.
I am a researcher at an algo trading shop. We are moving our core libraries from rust+python to Julia.
It really is amazingly powerful and has great interop with python (eg seamless zero copy array sharing).
In the past one had to muck about with cython/c/numpy api to speed things up, now one can just write the functionality in Julia and make it available in both ecosystems.
Python will likely remain the premier language to do research in, but more and more work can move to Julia which is much better at anything not immediately vectorizable.
Great news for me! I actually do Julia training. My colleagues do Python training. But we don't seem to be quit at the critical mass yet to gain a lot of training requests for Julia. But I am an optimist. There seems to be a shift going on. 2020 could be a breakout year for Julia.
A lot of my job the way I see it at the moment is to try to learn about people's experience switching to Julia to help explain to people why it would benefit them.
How did you guy actually end up switching to Julia? Was it a careful analysis ordered from the top, or was there more like some Julia evangelists who bugged people until they tried it an realized it was actually quite useful?
I used to work in the oil industry, and tried to convince people to try Julia. It would have been a huge advantage over our Python interface in terms of performance but it was a very hard sell. People are conservative. They are very reluctant to try new things. So I am always curious how other people pull off making a change happen.
Julia was brought in largely organically. We often need performant non-vectorizable code. Numba is actually a real pain to work with if the code is not explicitly numeric only. It works well for optimizing a hot loop here and there, but anything more complex becomes an exercise in frustration.
So we started experimenting with Julia and it was literally like the best of both worlds. Compile times can still be a struggle sometimes, but we are happy to eat a few secs startup cost when doing research, as most of the time we'd just have an ipython/julia repl going and keep the session open for hours/days.
Most people (me included) weren't prepared to pay the mental tax of writing Rust on potentially throwaway experimental code, so as we worked we realized that the core Rust libs can be easily replaced with much simpler Julia code without any loss in performance.
While the PyO3 library is awesome, it was actually quite difficult to reconcile the safety of Rust with the dynamism of Python and the friction can be really felt in any code dealing with the interop. This is mainly on the Rust side, as it ended up being littered with casting and type checks when communicating with Python. Rust being compiled AOT, a lot of the generics power goes out the window in the interop purely because it is impossible to know at compile time the type of objects coming from python. This has negative implications for performance, because the rust code can't be neatly specialized either, but has to resort to dynamic dispatch and trait objects. Julia wins here due to the JIT compiler that auto-specializes code at run time when the types are known.
I really appreciate folks like the parent here who take the time to highlight specific details like these that arose from their experience with different languages and paradigms.
> This is why I belive Julia has a real chance against Python. It hits all the right checkboxes: It is easy to learn, simple tools, while also being highly productive and giving great performance.
The only thing that makes me anxious about Julia is Dan Luu's complaint that testing is not a big part of the culture. Generally, for code folks are going to rely on to be correct, I want some mechanism for assuring correctness. Types, tests, proofs, whatever, but I want to see them.
Admittedly this is true of a lot of scientific computing, so I may be misplacing my nervousness.
In 2016 yes. But this has been very much addressed. At this point, not only is Julia well-tested, but it's so well-tested that it has to carry around its own patched LLVM and its own math library in order for its full tests to pass, because for example it requires things like sin to be correct to 1ulp which isn't actually true in a lot of implementations! Then when you go to packages, there's a huge culture of testing. Compare OrdinaryDiffEq's (just the ODE part of DifferentialEquations.jl) test suite:
which does convergence tests on every algorithm, along with regression tests on every interpolation and analytical value unit tests on each feature, etc. Meanwhile, scipy integrate has some of its own algorithms, but only a few regression tests, and most tests just check that things run: https://github.com/scipy/scipy/tree/master/scipy/integrate/t... . Same with other libraries like torchdiffeq: https://github.com/rtqichen/torchdiffeq/tree/master/tests . So Julia's testing culture is now strict enough that things that are commonly accepted in other programming languages would be a rejected PR due to lack of testing! And for good reason: these tests catch what would be "performance regressions" (i.e. regressions so the algorithm doesn't hit its theoretical properties) all the time!
My counterpoint to this would be that everything you need for proper testing exists already in Julia.
Also I would argue that Julia is a much easier language to write correct code in than Python. Python suffers the general OOP problem where it becomes hard to isolate problems due to all the mutations (imperative coding).
While Julia is not a purely functional language, you program in a far more functional style in Julia because it supports it much better.
My own experience when working with both languages suggest that I am able to write more pure functions in Julia than Python. I am able to crank out small isolated functions which I quickly test in my REPL environment as I go.
It is a different way of working. My Python friends write more formalized tests than me as they code. Julia is perhaps more in the LISP tradition. You are continuously writing and testing as you go in the REPL. Some of those test make their way into my test suite but not all.
Because we are generally not writing Server code in Julia testing is less important. If the program crashes so what? What is important is correctness of numerical output. Yes you need tests for that.
But I would speculate that tests needed to verify correctness of numerical calculations are less than tests needed to secure uptime for some server service.
Python is a fad right now, i dont think this will last. And i appreciate python dont mistake my comment. It just happened to have a simple 'ui' and some people made nice libs in it. The language is too fragile to reach more imo. i'd bet on Julia because it has stronger roots even though few care about it.
"nice libs" are worth a lot; consider Fortran. Although quite possibly nice libs that are often just bindings to stuff in other languages have less staying power.
Julia is getting a lot of adoption outside of the tradition CS crowd, so data scientists who would otherwise might be using R or Matlab, or Mathematica. I’m not really sure who is adopting Swift yet, beyond iOS devs.
yep, it is the current state of things. However, it would be better to have all this huge ecosystem written in a single performant language. People trade perceivable simplicity for things that are more beneficial long term.
>However, it would be better to have all this huge ecosystem written in a single performant language.
It's not the language, it's the linkage model. Python glues C components together and that's why experienced professionals don't blink when going all in on Python: the performance can be easily cranked up to C level.
Within the scope of a linked C library, this is true. But when your Python code is shuttling chunks of data between libraries it's less so. Pure Julia has the advantage that it can perform global optimisations that Python-wrapping-C can't.
I disagree. In practice the things I can do between Cython, llvmlite and numba are very low effort, wide reach optimizations. Practically, I have never found a case when a feature of Julia would have made this much easier for me. As a result, the tradeoff of Julia continues to be 100% focused on the switching costs, infrastructure maturity, drop in equivalents of well worn Python libraries, etc.
Doesn't that "just drop down to C" get complicated when you need to pass callback functions though? Users will want to write them in the original language for convenience and to use closures safely and easily. Wouldn't that kill your performance if the callback function is just Python again but called many times (e.g. an integrand for a numeric integration function, which integrand depends on captured runtime params). This is no problem in Julia, what are people doing cases like this in Python land?
I would argue that because it could have been Lua in the first place. Fastest C ffi. Faster, simpler scripting language with natural 1 - indexed arrays like in fortran, matlab. It got some traction, yes, from ML community thanks to Torch but Python had better batteries already at that time.
The problem is that you need C/C++ expertise to build packages, which creates a barriers between users of packages and makers of packages.
This is a big selling point for Julia. One is seeing much faster package development on Julia than on Python because you use the same language on both ends. Package users are often able to contribute to the packages they use.
Also the Python-Linkage has major limitations. If you create anything that requires the user to pass a function defined in Python to the C/C++ layer you take a performance hit. Think about solvers e.g.
For machine learning that is a big deal. In Julia you can write your own scientific models and do automatic differentiation and training on them. If you do the same in Python you get a huge performance penalty. C/C++ cannot really help you.
Yes, but these large packages represent a very small portion of Python packages. Also, they still include very large amounts of Python code.
So a typical user who knows only Python can still contribute even to these packages, and certainly to the other 99.9% of pure Python packages.
The barriers only exist if you want to contribute to the C++ core of NumPy or TensorFlow, and these parts are so complex and performance critical that even in Julia I'm sure only experts would be touching them.
I am not convinced. It does not reflect the frustrations I have heard from Python developers who ended up switching to Julia.
I don't have personal experience interfacing C/C++ code with Python but I spent a lot of time with Lua and C/C++ and Lua is considered far easier to integrate than Python.
Yet looking back and those experiences, while I thought it was super easy and cool back then, it was fraught with all sorts of problems with impedance mismatch.
Especially shuffling large chunks of data back and forth between the interfaces of two languages is hard. You cannot take an arbitrary Python data structure and push it into say NumPy.
I've seen in practice how much problems that can cause at one of my previous companies. We made a C++ application with a Python interface. We got major performance issues because we shuffled data back and forth as NumPy arrays.
It also limited what we could do with the data. Rather than being rich objects with associated functionality, you are stuck with blobs of NumPy data, which is really just dumb data with generic operations associated with them.
With Julia I can create e.g. an RBG buffer, where ever element is an RGB value and register functions working specifically for this type of data. In Python you would be stuck with pretending your NumPy array of floats or ints represents an RBG buffer.
But don't take it from me. Talk to people who have switched from Python to Julia and let them describe the benefits. I meet a lot of these people and they talk about how much simpler code they can write and performance gains they get.
Sure if your Python packages fit your niche great at the moment, no need to switch. But too many people twist themselves sideways to continue with the technology they have determined is all they ever need. Python developers should know that too. Lots of Java, C++, Perl etc guy at some point resisted going over to Python with lots of lame excuses.
Which library in the top 100 that you used had documentation (or lack thereof) that wasn't sufficient to understand how to accomplish the task at hand?
Some of the libraries need you to click into the docs for specific modules to get the full documentation for them. This confused me when I first set out.
eg. Postgres Simple. This is the page you get to at first when you search for it:
Part of the problem is that stackage.org does not have a nice design for reading docs, even when the author has written some like this.
I'd love to see more Haskell packages using readthedocs or similar. But I imagine that stackage providing ugly docs for free as a side-effect of publishing the package discourages most from making the extra effort to have nice docs.
I appreciate that the content is ultimately all there, and this particular package has made effort with docs.
But "the only problem" in this design is... quite a bad design. I don't really understand the choice to hide the actual docs and make a tree listing of sub-modules the primary content on the page.
This is pretty standard practice. The landing page for a package is never where examples live (except for the README). Haddocks are used for examples & tutorials, and the top-level module or a documentation-only module ending in ".Tutorial" are often provided.
Sure. It just took a bit of getting used to, but could be the reason why a lot of casual developers looking at the language have the impression that the documentation is poor.
I was just repeating the statistic from the article
I've no idea if the packages I have used or looked at are in the top 100 but most of them have not really had what I would call 'documentation', just sort of minimal probably auto-generated api docs
I'm going to give the same Haskell hot-take I gave on Twitter while at NeurIPS in December: the problem with Haskell is that you can port the awesome parts of pure, compositional abstractions over to Python, far more quickly than you can port really good domain-specific libraries and applications over to Haskell. My experience was that porting some nice ADT-based machinery to Python, using an available ADT library, took roughly one weekend, whereas porting the major domain-specific package I needed from Python to Haskell would take months to years.
I love Haskell. I prefer to use Haskell when I can. Haskell is a language in which I can Achieve Enlightenment. But apparently, God help me if I need to do some heavy graph processing or CUDA numerics in Haskell.
I have a strange relationship with Haskell. I love Haskell repl driven development of pure code for playing with algorithms and ideas. I use Haskell in this use case much like I use Common Lisp and Scheme languages. However, I am not very good at writing impure code and the interfaces between pure and impure code. To put it more plainly, I enjoy the language and I am productive, but I suffer sometimes figuring out other people’s Haskell code.
Despite the positive tone, what really struck me in this article was that they struggle with getting people to work on the compiler because it is too complex.
It just confirms my main criticism against advance statically typed languages: They are simply too complex.
It is why I have more faith in languages like Julia, because you can achieve a tremendous amounts of power, expressiveness and performance in a relatively simple language.
Dynamic typing gives you simplicity in the type system which is impossible to achieve with static type checking.
Long term this has profound implications. People can keep hacking on and expanding Julia because they can wrap their head around the language. You don't need to be Einstein to grok it.
I think you may also see Clojure overtake Scala for the same reason. The simplicity of Clojure may in the long run overtake Scala although Scala benefits a lot from similarity to Java at a superficial level.
I don't think the issue here is due to static typing, but due to the age and complexity of the language implementation. It's not trivial to figure out how all of those extensions interact with each other and your changes.
Compilers are wonderful to implement in a statically typed language with algebraic types and pattern matching, every pass can be a function transforming this intermediate language to that intermediate language until you emit the target code. The only thing that comes close in dynamically typed languages is the Nanopass framework used in Chez Scheme.
GHC development has a far lower bus factor now than when it just consisted of a handful of Simons. Compare to Clojure that has everything needing to go through one guy.
Julia is irrelevant, it is implemented in C++. All the real work is done in LLVM, which is a tremendously complex heap of C++, far more intimidating than GHC.
How did you arrive at that number? Quite a lot of ways one could count that.
Anyway I have never claimed statically typed languages are irrelevant or not useful. My criticism is of advance statically typed languages.
I am quite okay with stuff like Go, C and maybe Ada and Swift. I am highly critical of C++. Far too complex language.
With Haskell my criticism is different. It seems like an elegant language you can learn a lot from. However I criticize the prevalent belief that Haskell is some sort of programming Nirvana. That somehow it is the ultimate language. I think Haskell is grossly overrated. It is too complex at a theoretical level for the average programmer.
When we also learn the implementation is complex.... well then I am not sure there is much hope for that language. Sure keep it in academia. People learn lots of useful stuff from it. But don't kid yourself into thinking world dominance is right around the corner.
Most compilers are very complex because generating performant code on modern hardware is hard. I don't think the complexity of the type system make much of a difference. Of course many new languages (like Julia) outsource a large part of the complexity to LLVM.
I completely disagree. The experience with Julia points in a different direction.
Julia performance has has little to do with LLVM. If performance was that easy, you could just slap LLVM in the back of any dynamic language and poff by magic you have super performance.
Most dynamic languages that have reached decent performance have done so using trace-JIT compilers. These are complex and require a lot of man hours to make.
PyPy is a similar approach. It is hard problem to solve.
Yet Julia spending considerably less man hours than either project and with smaller and simpler code base has managed to run circles around these two projects in terms of performance.
Why? Because of smart language design. The pervasive multiple-dispatch design tailored towards JIT code generation has been key.
It allowed Julia to get great performance with a very simple method-JIT compiler. These are much easier to make than trace-JIT compilers.
But Julia is not alone. Go is another example of a language which kicks above its weight. It is a relatively simple implementation, yet has good performance and is enjoyable for most people to work with. Except those who really hate Go of course ;-)
My bottom line is: LANGUAGE DESIGN MATTERS!!! You you design a smart and simple language you can get away with simple implementations and still get good performance.
Sure LLVM is an important piece of the puzzle, but it serves no more important role than C does as the backend for Haskell IMHO.
Julia is built around multiple dispatch - when making a call, the method to execute is chosen based on the run-time types of all of the arguments.
Once this choice has been made, Julia compiles the method, specialised for the exact types of the arguments.
So, the dispatch process and the JIT compiler are linked - both are reliant on type information every time a function is called.
This specialisation is the only way the Julia JIT uses runtime type information. Unlike JavaScript JITs, Julia does not track things like the types of local variables during execution (although it may do some static inference). Therefore type annotations for local variables can improve performance.
Mostly spot on, although it's very rare for local variables to require type annotation—type inference can easily figure it out for locals. Unless, of course, they are assigned from an untyped external source the compiler couldn't possibly know. You could, for example read something from a JSON source knowing that it should be an number, annotate it with `json["field"]::Float64` and then the compiler will emit code to check the type and throw an error unless the type is actually a Float64.
You actually don't need explicit types in function parameters unless you're trying to control dispatching. Otherwise the compiler will auto-specialize on call. This blog post might be a better explanation on when it's necessary: https://www.stochasticlifestyle.com/type-dispatch-design-pos...
pansa had a great answer so I will just add to that. Multiple dispatch is rare among programming languages and the few which do it only has it as an add-on.
I believe Julia is the only programming language where multiple dispatch is the way all function calls work. There are no exceptions. It is also the only language where it was used to aid a JIT compiler.
Once you dig into multiple dispatch and see how it affects everything from performance to Julia package design and how packages integrate with each other, you will just be blown away.
It is hard to convey how ingenious this solution is. Even the creators themselves have admitted they did not realize how clever this would end up being. They only realized after people started actively using Julia what a gold mine they had hit.
> It just confirms my main criticism against advance statically typed languages: They are simply too complex.
But this is about the complexity of the compiler itself, not of general software written in Haskell. For any given language, most people use the language and don't hack the compiler. The compiler of any given language can be complex for plenty of reasons, many historical and unrelated to the programming language itself.
I don't think that the type systems are too complex. I think the issue is that approximately zero effort (perhaps even negative effort) has been put into the UX of the type system. We have tools for debugging run-time errors, such as debuggers and tracing. When you shift errors from run-time to compile-time, as type systems do, you need similar tools to debug and inspect type checking. Very little work has been done here.
Yes, this is missing from the article. There is some recent work (inspired by Elm raising the bar) with better UX for type errors. The technology tools exists but the labor is waiting to be done for every type in every program.
Like documentation in general, it's the kind of work that requires a long slog across the code base, not inventing a new abstraction, so most Haskellers and most people don't bother to do it.
That is why dynamic languages shine. Because types are objects like any other object you can use the same tools to deal with types as other code. It is one of the reasons why meta programming tends to be much harder to achieve in statically typed languages.
(What you call types are not what those who work in programming language theory call types. I disagree but this is an old and well worn argument and I'm not really interested in revisiting it.)
There is your problem right there. These static type gurus live in an alternative universe in ivory towers far removed from where the rest of us simpleton programmers live.
Frankly I think it is an intellectual cargo cult. For all its sophistication these languages have not delivered that much. Look at language like Go, which these guys would laugh their butt off. Yet Go has produced usable software for a lot more people and made a lot more developers happy than Haskell ever could.
Coming years after Haskell Julia seems to be doing a lot more for science than Haskell has ever managed to achieve.
Put another way, the standard programming language theory is that types are constraints that are uncovered (via type inference) and checked at compile-time. If type information is found at run-time these are known as tags. In Haskell, for example, you can declare a type like
newtype SecretKey = Int
This creates a new type (SecretKey) that has a run-time representation that is just an Int. I.e. it has no additional information associated with it at run-time that you could use to distinguish it from an Int. At compile-time it is distinguished, however. You cannot use a SecretKey where an Int is expected and vice-versa. This could prevent you leaking secrets to other parts of your program, for example. This is one way you can reclaim performance in a statically typed language, vs dynamic types, without degenerating to passing around uninformative primitive types like Int (which introduces the possibility for errors).
In my opinion you are actually reading this the wrong way. When I explain concepts such as boxing to people I will refer to type tags. But in that context I use the phrase to refer to how something is implemented.
How a type system is implemented is different from how it conceptually / semantically.
For instance in Julia types are conceptually objects you can pass around. However they will not always correspond to a type tag. Conceptually all objects in Julia have a type. However at runtime they may not. The JIT compiler could have gotten entirely rid of them.
When values are placed in a Julia array, individual elements will typically not have any type tags. However conceptually they still have a type.
To me type tags are just an implementation detail which both dynamic and static languages may use. However when you speak at a conceptual level you don't use that word. You don't say, "lets put this type tag into that object," you say "lets put that type into that object, bind to that variable or whatever."
The way I like to talk about static and dynamic languages is to say: In dynamic languages values have types, but not expressions / variables. In static languages expressions have types, not values.
That is of course a simplification, but IMHO simple and sensible way of making the distinction.
> This creates a new type (SecretKey) that has a run-time representation that is just an Int. I.e. it has no additional information associated with it at run-time that you could use to distinguish it from an Int. At compile-time it is distinguished, however.
I can do exactly the same in Julia
struct SecretKey
value::Int
end
After the JIT compiler is done, there is no difference between this and an `Int`. The type associated with the value only exists conceptually at runtime. A `SecretKey` value in Julia will in most methods look no different from an `Int`
> without degenerating to passing around uninformative primitive types like Int (which introduces the possibility for errors).
That would be the same in a strongly typed dynamic language. Except the error will of course be caught at runtime. But it is not like you can use the types in an illegal way.
Ok, I get `data` from the stream, I guess it's some kind of array, but what can I do with it? What exactly is it's type? I need to extract Int32's from the stream and operate on those, how do I do that?
So, as you say, I was forced to trigger the code at runtime, by inserting some debugging code that logged the type to console.
So for a simpleminded guy like me, static typing helps me a lot because it makes it easier to reason about the code I'm reading.
> I think you may also see Clojure overtake Scala for the same reason. The simplicity of Clojure may in the long run overtake Scala although Scala benefits a lot from similarity to Java at a superficial level.
Correct me if I'm wrong, but didn't Scala overtake Clojure some years ago as the second most popular language on the JVM (second to Java ofc). From my point of view it rarely happens that these trends reverse.
Scala has the advantage that it allows OOP or Functional Programming, which Clojure does not.
But I do get your point about simplicity. I tried 3 times to learn functional programming by learning Haskell and it never clicked. Then I learned Clojure and who would have thought, functional programming is actually not as hard as Haskell makes it out to be.
I work in a JVM shop and I don't see Clojure making much head way. Unlike say, Apache Spark, there's no killer app (datomic notwithstanding) that requires Clojure over Scala.
Scala also offer the advantage of static type checking, and a less alien syntax. Yeah, I know Clojure is just s-expressions, but all the brackets don't help its uptake.
Oh, and Clojure stack traces make Scala stack traces look positively brief and informative.
Scala's syntax for (generic) type declarations is super alien, and you can't avoid it because it's a big part of why you'd use Scala in the first place.
I don't keep up with Scala and Clojure that much since I am not a JVM guy but I was always under the impression that Scala being older has ALWAYS had a lead on Clojure.
However the Scala hype seems to have died down years ago while you see more enthusiasm around Clojure.
> I tried 3 times to learn functional programming by learning Haskell and it never clicked.
LISP (Racket) and Julia helped me most with functional programming. For Haskell type of functional programming I think Swift actually helped me most.
But I find many of the same problems with Swift as with Haskell. Understanding type mistakes can be really hard. You struggle much longer with figuring out type problems than you would in a dynamic language.
I think advocates of these super statically typed languages completely overestimate the complexity the average human mind is capable of dealing with. Perhaps because the creators are super smart themselves ;-)
> I think advocates of these super statically typed languages completely overestimate the complexity the average human mind is capable of dealing with. Perhaps because the creators are super smart themselves ;-)
That is a really good point. From my personal pov languages that take to long to understand and take you >1 week to get productive are rarely useful since you won't be able to afford or train "normal" people to use it.
In my company we recently switched from Python + Numba to Python and Clojure. Since even though people never heard of functional programming or Clojure, they can get started on simple things within the first week.
Haskell's compiler is already big and fat, having a very wide range of features. I don't think Haskell's extensibility is a problem in terms of adoption at this point, the problems lie elsewhere.
Therefore, simplifying GHC development likely wouldn't attract any larger user base for the language.
> Dynamic typing gives you simplicity in the type system
Can you elaborate on this? Dynamically typed languages essentially have no type system (but yes even they do have types).
> Therefore, simplifying GHC development likely wouldn't attract any larger user base for the language.
I can agree with that. What I meant was more that I see it as a sort of symptom of its complexity. A kind of complexity which causes problems elsewhere.
> Can you elaborate on this? Dynamically typed languages essentially have no type system (but yes even they do have types).
Of course they have a type system. You define types and the types of values determine what you can do with them. That is not different from static typing. It is just that the enforcement happens at runtime.
One example of complexity in static typing is what you get when you try to do any kind of meta programming such as templates or generics.
Perhaps the easiest way to illustrate the problem is to look at the terra language. http://terralang.org
In terra you see Lua serving the same job as the templating language in C++. Yet a typical templating language is very limiting compared to a full blown dynamic language.
With static typing you just very easily end up in a catch-22 situation: What are the types of the types of the types?
For instance in Julia I can write:
A = Int
B = Char
c = 10
bar(name::String) = println("Hello ", name)
foo(x::(c < 10 ? A : B)) = 2+x - 10
Which is kind of complete nonsense code, but it illustrates a few different things which I can trivially do in a dynamic language like Julia but which would be hard in a static language. Here I am storing types in the variables A and B. Then I define a function `foo` which has a specific implementation depending on the type of its single input argument `x`.
In `bar` I specify the type of `name` as String. However in `foo` the type of `x` is evaluated at runtime. When the function definition of `foo` get evaluated, only then do we decide what the type of `x` is.
Here an if statement is used to determine the type of `x`. However I have the availability of the full Julia language to make that decision. I can make multiple functions to do that.
Try something like that in a statically typed language and the type system will tie itself in knots. If you could even support this in a static language, the complexity of describing what I just did in a static language would make most software developers dizzy.
> That is not different from static typing. It is just that the enforcement happens at runtime.
Isn't the inherent problem with dynamically typed languages exactly that they do not enforce types at compile time nor runtime? Like you try to call a method of an object that does not exist, and it crashes the runtime.
Moreover, I'm not sure I get your example. Wouldn't that be just a matter of a union type + parametric pattern matching in a statically typed functional language? You would just get exhaustiveness checks and type safety on top of that for free.
You can get literally the same "simplicity" as a "dynamically typed" language through structural row-polymorphic types with type inference, i.e. static duck typing. Not to mention that the concepts of static and dynamic typing are orthogonal and there are languages that have both or neither.
You have no clue what you're talking about.
Before calling somebody clueless you have to understand the point they are actually making. I don't have the space to go into details in this comment. But you can read a more detailed explanation of what sort of simplicity I am talking about here:
It is not just about the simplicity of implementation but also about the simplicity you can create in your whole development environment and process.
> You can get literally the same "simplicity" as a "dynamically typed" language through structural row-polymorphic types with type inference
If you believe that, then I am sure you can point me to a language that does exactly this and let me try learning it myself and make up my own mind whether it is simple or not.
> The same problem as before repeats itself. Complexity grows to a point that we yet again need a real language to do the job. A script language which allows us to write some code that explains how e.g. our C++ values should show up in the debugger. Not to mention that debuggers for statically typed languages themselves tend to grow into complex behemoths with a dizzying array of functionality to deal with the complexities of statically typed languages.
This is just blatant nonsense and the author of the article clearly has no idea what a powerful static type system is capable of.
If you want to get a feel for what structural typing can give you, you don't need to look further than TypeScript. If you want proper row polymorphism, you can try PureScript.
> This is just blatant nonsense and the author of the article clearly has no idea what a powerful static type system is capable of.
A complete non-sequitur. It does not refute the fact that most tools such as debuggers are customized with dynamic languages. The few times statically typed languages are used, it tends to be some kind of managed language where a lot of type info is retained at runtime.
> no idea what a powerful static type system is capable of.
If statically typed languages where so amazing and powerful then they would have been frequently used as extension mechanisms. They are not. Meta-programming also tends to be poorly developed in most statically typed language. The paradigm is just very limiting.
> If you want to get a feel for what structural typing can give you, you don't need to look further than TypeScript
I know structural typing from Go. If you think structural typing is a proper substitute for dynamic typing then you simply have not used a powerful dynamic language before. Or you have not learned how to use it properly.
With dynamic typing you can easily manipulate types as objects. Structural typing does not give you that. You latch on to a completely superficial similarity and think it is somehow similar in capability and scope.
The attitude you display is what makes a lot of the static typing fans kind of off putting. The smug superiority complex. I prefer dynamic languages but I recognize areas where static typing is preferable.
> With dynamic typing you can easily manipulate types as objects
There are statically typed languages like Agda in which types themselves are "first-class objects" whose types are "kinds" whose types are "sorts" and so on. They form a hierarchy of Russel universes where functions can be defined at every level of the hierarchy. Typical ambiguity even allows to define implicitly universe-polymorphic functions that work on terms of every universe, i.e. you can write a function that can be applied to values _or_ types _or_ kinds just the same.
Scala is still growing, and it has been doing so (albeit slowly) from the very beginning. Clojure was very trendy for a while and grew really quickly, but it peaked around 2015 and is mostly dead now. The idea that clojure will supercede scala in the future is completely lost to reality.
Scala and Haskell are complex because it's creators wanted that way, not because they are typed FP. Take a look at Elm, it's very simple and clean syntax.
Big issue with Haskell adoption is the number of hoops you have to jump through to write efficient code in it. Haskell abstracts away the idea of a procedural VM implementing the code underneath, but you often need that exposed to finagle your code into a form that’s efficient.
Haskell programming ethos is opposed to that, the language wants people to focus on the semantics of computation not the method. Yet we must be able to specify computation method if we want our programs to operate efficiently.
The truth is that the Haskell compiler will never be able to automatically translate idiomatic Haskell code into something that’s competitive with C in the common case. once you start finagling your haskell code to compete with C you’ve negated the point of using Haskell to begin with.
> The truth is that the Haskell compiler will never be able to automatically translate idiomatic Haskell code into something that’s competitive with C in the common case.
Is this something you have experience with, or are you just theorizing? I know there are pitfalls to Haskell development, but to assert that "the common case" has uncompetitive performance seems wrong to me.
My problem with this kind of assertions is that often -- not saying it's your case, that's why I'm asking -- they come from people who imagine how it must be (or read it in a blog), often coming from a place of never really having tried to solve something with the language, and this sadly percolates into popular wisdom ("Haskell is not good for this or that"). Something similar happened to Java's allegedly "poor" performance, way past the point Java software sometimes outperformed C in many areas.
I think it's a common problem with almost all, if not all, languages that come to us out of the 1990s that they are fundamentally built on the presumption that "someday" compilers may save us. Well, "someday" is pretty much here, and they've all failed, as far as I'm concerned. (If you're happy with 10x-slower-than-C and substantial memory eaten to get even that fast, YMMV, but it's not what was hoped for. No sarcasm on that, BTW; sometimes that's suitable, just like sometimes 50x-slower-than-C is suitable. But it's not what was hoped for.)
Haskell can do some pretty tricks with specific code if you tickle it right, but if you just write general, normal code, it's faster than Python (a low bar, Python qua Python is nearly the slowest language in anything like common use) but not a generally "fast" language. "Someday" is here; if it's not "generally C-fast" today, I see no particular reason to believe it will be in the future either, especially since GHC seems to have spent a great deal of its design budget.
It would be interesting to see someone's take on Haskell, but where they write the language from the very beginning to be a high-performance language. There's probably multiple points in this design space that would be possible. Arguably Rust is nearly one of them, and getting even closer in the next few years.
Yes I have many many hours of experience with Haskell and familiarity with functional programming. I’m speaking from experience.
Optimizing Haskell code is a huge downer. The experience of having to throw away beautiful code and rewrite it in C++ or non-idiomatic Haskell purely for performance reasons is extremely disheartening. I don’t recommend it.
Haskell actually does a great job when you do need to drop to C (or lower-level Haskell) for performance. It has a great FFI, a bunch of modules around low-level programming (raw ptrs w/arithmetic even), and things like the ST trick and (soon) LinearTypes to help you build interfaces that guarantee your impurity doesn't leak when called by pure code.
Haskell code tends to be pretty fast as-is, and tbh I don't see the problem with having to think about performance when you're writing performance sensitive code. When you do need to hand-optimize, Haskell does not get in your way or make it impossible.
Also, many extremely complex Haskell abstractions can be optimized away completely by GHC! Generics, lenses, and the state monad come to mind.
The thing is, like 20% of your program ends up being non-idiomatic, ghc-specific Haskell. I suppose for certain applications it could end up being the whole thing, but in general I'm thinking optimized Haskell is in that ballpark tops.
And idiomatic Haskell's performance is plenty acceptable for a variety of common use-cases (so not "nearly always is")
I've deployed plenty of web services & data processing jobs in Haskell and the RTS has never been a bottleneck or issue. So I'm guessing you weren't doing an IO-bound activity (where Haskell is quite good.)
You're right in that you don't spend time on Haskell thinking about how the code actually executes.
But I honestly don't think performance is the reason majority of the developers shy away from Haskell. Most often you achieve relatively good performance without giving it any thought. At least compared to its peers, I mean other high level languages you'd use to solve the same problem.
Haskell's main problem is that it is over-zealous, and built on axioms that make it a poor fit for real people writing real code. Everything else flows from that core issue. Functional purity and lazy evaluation are interesting, but when you can't toss a printf debug or log statement into a function without changing function signatures all the way up, it's not going to be popular.
Pragmatic, sloppy languages will always be more popular, because they are more forgiving.
To be fair, you can printf debug anywhere (Debug.Trace module). I'm the "print to debug" kind of guy, and I can debug in Haskell just like in Python using this.
I think the issue you have stems from the fact that people can't transfer the knowledge from C/C++/Python/wtv directly. One of the standard way to build programs in Haskell (mtl-style) allows you to perform IO actions almost anywhere, provided you're willing to play with monads. But this is so different from anything most people have ever seen that I understand why it can be frustrating.
Any idea when this was added? I am relatively certain that it was not possible in Haskell 98, and admittedly most of my Haskell experience is a decade old.
I have picked up three well-regarded Haskell books over the past decade trying to get back into the language, and don't recall any mention of this capability.
That's another issue, the dearth of anything like tutorials or books on how to do something practical with Haskell, rather than the whirlwind tour of language features. I keep being told that serious software is being built in Haskell, but the knowledge of how to get from university-grade code to production-grade code is an unmarked wilderness that everyone must apparently navigate on their own.
Looking back on historical GHC releases, the earliest one available on the web page is version 0.29, released in July 1995, and it already has the trace function. I would guess has been there for a long time.
The license on the Debug.Trace module says 2001... That's all I know.
I'm a big fan of the "Haskell Programming from First Principles" book. I read it on-and-off over the course of 2 years, and I think I'm an intermediate Haskell user at this point.
The most production-grade Haskell software I've ever played with would be Pandoc (document conversion) and the Yesod family of webdev libraries. Playing with Yesod is a bit scarier because it uses some Template Haskell magic. On the flip side, there's a great user guide (the "Yesod book").
> when you can't toss a printf debug or log statement into a function without changing function signatures all the way up
But you absolutely _can_ do this in Haskell.
Sure, it's considered very unsafe and shouldn't be used in production, but for printf debugging it's fine.
Admittedly, production-ready logging requires type signature modification, but if you subscribe to Haskell's idea that side-effects should be reflected in type signatures, then I don't see that as excessive.
Do you have any actual experience trying to solve something using Haskell, or are you just theorizing about how you imagine it would be "for real people writing real code"?
I've tried a few times, and bounced off quite hard. I'd rather go with something more pragmatic like Ocaml or Scala or F#. Particularly since all of those interop rather seamlessly with the vast array of existing code that is written for either the JVM or .NET, yet still give you considerably better type systems than the default C# or Java.
I tend to use Scala and Java for my day job. I completely understand you. Though I feel that a lot of what's good in Scala is better and simpler in Haskell, or was influenced by Haskell, so even if I don't use it for my day job, I feel it has made my job easier and better. Knowing Haskell has made me a better Scala programmer.
As an example, whenever I had trouble visualizing what some functions would do in Scala -- because they used to have horrible signatures, though it's getting better -- I would simply test the equivalent functions in GHCi to get a feel of what they would do, because Haskell functions tend to be simpler than Scala's ;)
Indeed! It’s an excellent low level imperative language. And amusingly enough bits low level libraries like vector and primitive that actually motivate a lot of the really fantastic type system innovations in ghc over time.
Code generation is a difficult issue, compiling a lazy functional language to assembly could easily fill up two semesters of classes alone.
The VM in C is really small and the compiler can be built up incrementally[1].
[0] https://github.com/blynn/compiler
[1] https://crypto.stanford.edu/~blynn/compiler/quest.html