Haskell Problems for a New Decade
stephendiehl.com
stephendiehl.com
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.
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].
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.
For me, it's easy enough to follow.
Is that true? I thought those compiler courses typically implemented some toy language.
Maybe "in" is misplaced and the following was meant instead?
"Most undergraduates take a compiler course which they implement in C, Java or Scheme."
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.
Sorry but doesn't this statement fit better to the definition of "borderline" something?
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.
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.
I'm not that pro-haskell but I also see how all languages in the last decade shifted toward fp idioms clearly. I mean redux is a fold.
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.
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.
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)
By the way, I'm particularly interested because I am writing about Haskell myths. I have a very rough draft at http://h2.jaguarpaw.co.uk/posts/haskell-myths/
Edit: I forgot about consultancies like Well-Typed and Tweag
Another trend (that I don't particularly like) is all the blockchain startups using Haskell.
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
(Or really, just combine "cryptocurrency" or "cryptocurrencies" with any negative word and throw it into search and you'll see the point.)
All cryptocurrency has a serious reputation problem right now, and it's probably not going to go away for the considerable future.
It doesn't mean that the company has a product.
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.)
the act of trying to appear or sound more important or clever than you are
Some irony in your comment. I meant exactly what was said.
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.
[1]: https://docs.oracle.com/en/java/javase/13/security/permissio...
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.
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.
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.
[1]: https://dl.acm.org/doi/pdf/10.1145/3371078?download=true
- 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.
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).
In software verification,
a sound technique is ...
2. One example: make sure that HTTP routes that are GET will at most just read the DB, not write
3. I actually don’t like that the type system is where this is going into. I want to have some form of static analysis, and this is providing it.
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.
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.
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.
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.
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?
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.
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.
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.
Automated methods are.
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.
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.
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 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.
better scalability than
deductive
- 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.
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.
Model checkers check deep
DPLL is based
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.
can check most properties
expressible in TLA+
- 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.
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.
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.
I clarified further here: https://news.ycombinator.com/item?id=22146186
> 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
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
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,
* * *
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.
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.
[1] W. Hodges, Model Theory.
[2] D. Marker, Model Theory: An Introduction.
[3] C. C. Chang, H. J. Keisler Model theory.
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).
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.
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).
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.
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. :)
FP and OOP are both well tested design patterns. Mixing them up in an incoherent way just makes the whole software architecture somewhat unpredictable.
How programming paradigms can be lift over to the level of "algorithms + data structures", regardless of the language.
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?.
I'd say that OCaml blends imperative and functional programming cohesively and fairly equally, though.
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.
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.
[0] https://person.dibris.unige.it/moggi-eugenio/ftp/ic91.pdf
[1] https://groups.csail.mit.edu/pag/OLD/reading-group/wadler-mo...
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.
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.
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.
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.
> Sure, but why?
I already explained why.
Why do you even care about Haskell at all?
> 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.
That doesn't answer why because you reversed the logical implication. See here: https://news.ycombinator.com/item?id=22140610
> Why do you even care about Haskell at all?
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.
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.
Lean. It's implemented in a
dependently typed programming
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.
I meant that Lean, I think, could be implemented in Lean.
Do you also work with Lean?
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.
remove the barrier between
types and terms then ...
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
> 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.
You're not even putting any stakes on the table. That's such a safe bet. It's unlikely you'd even have a chance at losing the odds are so stacked.
There's a great talk on why functional programming is not the norm: https://www.youtube.com/watch?v=QyJZzq0v7Z4
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?
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.
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?
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.
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.
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?
[0] https://www.computer.org/education/bodies-of-knowledge/softw... [1] https://en.wikipedia.org/wiki/Church_of_Col%C3%B2nia_G%C3%BC... [2] https://github.com/github/semantic/blob/master/docs/why-hask...
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.
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%)
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.
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 :)
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.
99 bottles of beer with state monads gets at some of the challenge for the neophyte:
http://www.99-bottles-of-beer.net/language-haskell-1360.html
Look at the struggle going on to deal with a "simple" piece of state.
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.
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.
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.
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?
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.”
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.
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.
The vast majority of Python packages are in pure Python and require no C/++ skills at all.
- NumPy - Pandas - TensorFlow
etc.
In contrast the most popular scientific packages in Julia are almost all pure Julia.
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 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.
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.
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.
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.
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.
These are the details that matter.
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.
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.
https://travis-ci.org/JuliaDiffEq/OrdinaryDiffEq.jl
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!
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.
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.
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.
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 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.
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.
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).
It obviously might get replaced by new languages and ecosystems, but that’s a huge difference than it being a fad.
This is still very very poor, and one of the biggest problems faced by newcomers to the language (speaking as one myself...)
eg. Postgres Simple. This is the page you get to at first when you search for it:
https://www.stackage.org/lts-14.21/package/postgresql-simple...
It looks like there is no documentation, just a list of modules.
Clicking on the Database.PostgreSQL.Simple module gets you to the docs:
https://www.stackage.org/haddock/lts-14.21/postgresql-simple...
The package home page needs a README with links to wherever the good stuff lives.
Look at how GitHub does it.
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.
Look at https://www.stackage.org/package/rio
The only problem is that the readme is below the module list, and mostly hidden behind a Read More button.
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.
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 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 might be spat at or beaten up in the street for being Jewish - that happens in Brooklyn or LA anyway these days."
And I was wondering, how has it been for Jews in the US in the past few years up till now? When did things start to get noticeably worse?
I know about the rising Anti-Semitism and the particular incident in NY about a month ago.
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.
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.
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.
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.
So, if not on local variables, where are explicit types necessary (other than function parameters)?
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.
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.
Here is a reasonably good overview of safety (aka dynamic typing) vs types: https://papl.cs.brown.edu/2018/safety-soundness.html
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
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.
I can do exactly the same in Julia
struct SecretKey
value::Int
end
> 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.
stream.on('data', function(data) {
processStreamData(data, (results) => {
callback(results);
});
});
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.
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.
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 ;-)
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.
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.
Clojure certainly allows both, that is what protocols and multi-method dispatch are all about.
CLOS has Object in the name for a reason.
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.
If LLVM was what mattered every dynamic language would have slapped it in the back. I am sorry but it just isn't that simple.
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.
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.
https://medium.com/@Jernfrost/the-many-advantages-of-dynamic...
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.
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.
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.
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.
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).
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
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.
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.
Static languages are static because static provides opportunities for correctness, not on your list.
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.
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.
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.
It’s still under development but intended to be a high performance functional language.
The author has substantial experience in JITs and compilers.
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.
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.
I don't dispute this. My problem is that people will use this as a reason dismiss Haskell, and then use Python.
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.
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.)
Pragmatic, sloppy languages will always be more popular, because they are more forgiving.
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.
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.
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").
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.
You're mistaken about printf debug.
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 ;)
The "over-zealous axioms" you refer to can be boiled down to: if you do mutation in a function, don't give it a pure type.
https://hackage.haskell.org/package/monad-ste Is a fun imperative data structures with abort only exception lib I wrote a while ago that I’m still quite proud of