Typing Is Hard
typing-is-hard.ch
typing-is-hard.ch
This is not necessarily the end of the world. If you go out of your way to write an actual compile-time program by abusing your type system, and that program contains an endless loop, you probably shouldn't be surprised that your compiler hangs.
Unsound type systems cause more headaches in practice. For example, TypeScript types are only trustworthy if your program is careful about boundaries with the outside world. In larger, older systems, I occasionally do get bit by this.
It depends on what you mean by "something like" because Idris' dependent types are arguably equally as useful in practice but type checking remains decidable due to totality. This goes for Agda, Coq and Epigram (if it still exists?) as well for different technical reasons each, not that they are as convenient to program with.
My point was just that the situation with C++ is worse than it has to be.
Decidability of type checking is instead related to how explicit surface syntax is. In intensional type theory, the usage of equality proofs is marked explicitly, which is sufficient to retain decidable type checking. In contrast, in extensional type theory, the usage of equality proofs is left implicit, which causes type checking to be undecidable.
ZFC and MLTT do not differ in that decidability of proof validity is not related to logical expressiveness.
It's not even true that for type theories, decidability of proof validity implies normalization. Normalization is not logically equivalent to decidable type checking.
For example, we can have a term language for extensional type theory which is annotated with reduction traces. This is the kind of syntax that we get when we embed ETT inside ITT. It has decidable type checking, as the type checker does not have to perform reduction, it only has to follow traces. This kind of tracing is actually used in the GHC Haskell compiler to some extent. So we have decidable type checking for a surface syntax of a type theory, for a type theory which is a) consistent b) not strongly normalizing.
Let’s come at this from the other direction. Suppose I find a non-normalizing term X of type false (like that produced by Girard’s paradox if we leave off stratification). What happens when I try to type check this?
id(X): ==(X, rec_0(0, X))
Where id is the constructor of the propositional equality type and rec_0 is the recursor for False.
id(X): ==(X, rec_0(0, X))
Sorry, what's this supposed mean, is it a definition? The propositional equality type has two or three arguments, I only see one (X) here, if as you say "id" is propositional equality.
In any case, nothing peculiar happens when we check a trace-annotated proof of bottom. We are free to use any particular finite-step unfolding of the non-normalizing proof.
We also don't need any paradox or inconsistency for a non-normalizing term, it is enough to work in ETT in a typing context which implies bottom, or which contains an undecidable equational theory, e.g. the rules of the SK-calculus.
> The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem
Decidability of type checking is always relative to a particular surface/raw syntax. A trace-annotated raw syntax does not need a normalization assumption for type checking.
The overall expression is shorthand for any term whose typechecking involves that type assertion. For example, type checking passing the term to the left of the colon to an identity lambda with argument type of the term to the right of the colon (λ(x: ==(0, X, rec_0(0, X))).x)(id(X)) will pass iff the left term’s type is right term.
I’m not talking about extensional type theories here (as Idris/MLTT is not extensional), so I don’t think I understand the relevance of the trace annotated proof. Idris will let you write the term I have above without any trace annotations so its typechecker must do something with it.
You’re right that a trace-annotated raw syntax doesn’t need normalization assumptions, but Idris is not trace annotated; the type checking algorithm is required to perform any normalization required without further direction from the user.
The Idris type system does allow you to specify and formalize TMs internally, but that has no bearing on decidability of type checking, as I explained before.
the alternative would be writing bash or python or ... scripts to generate the code, and for those :
- you likely don't have any error message at all (ugh)
- they won't have knowledge of the type system of the language you're operating.
Seriously, everyone complains about pages and pages of template errors, but if you use any decent IDE it's a two-click process to go to the part of your code where things fail. Errors will be split, then (at least with GCC & clang) you just start at the bottom of the error which is the place in your code where things go wrong 99% of the time - and if not, rarely if ever more than a couple steps above that. see e.g. : https://streamable.com/0k6lvl
also, decidable likely implies total - and my experience with total languages is that more often than not you need to add another turing-complete "scripting" layer on top of it (for instance, a TC language to generate expressions in the total language) as it's so cumbersome to write otherwise when you have actually business rules and not simple math examples
The challenge beyond the math is then making the error messages useful, and also being able to make progress beyond the first error in a useful way.
Ask yourself why dynamic type languages keep appearing, despite a fanatical resolve to purge them from the face of the earth? It’s almost as if some people prefer them.
But I guess the knowledge of salvation by compile time binding must be brought to the late binding heathens, to use a poor analogy.
On the other hand, I’m willing to admit that strict Compile time type checking is what many or most people prefer.
Generalizing to transportation one might ask: What is the better transportation device, a boat or a horse?
... of which one can somewhat reasonably conclude, that whether the question itself is the right question, is the real question.
Few oppose types if they don't have to do anything at all and if it doesn't take any of their time either in runtime, compile time, or otherwise. Realities being what they are, there is always at least some parts of the aforementioned that is false for any type system that is actually useful.
Because of this, and for a few other similar characteristics of types and computation, it boils down to nothing but a question of which kind of tradeoffs people find palatable.
Given that premise, there should be no surprise that the answers are subjective no matter the responder. The question of better is here nothing but an entirely subjective question veiled as an ostensibly objective one.
E.g., My coworker grabbed a word from somewhere, slapped a cast on it and proceeded to write into it. Hilarity ensues.
All the burden of explicit compile time checking, but no guarantees that anything is what you said it is by the time your coworker uses it. Of course, no computer Run-time is wasted on silly things like type, bounds or null checking, either.
Is this correct? I dug out Milner's paper [1] where he states that Algorithm J is more efficient (which was what I had been led to believe), but that Algorithm W is more suited to functional (as opposed to imperative) implementations.
Edit: Actually I think I'm parsing this sentence incorrectly, "best known" means literally that as opposed to "most efficient known".
[1] https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/...
kevincox's comment sums up my misunderstanding.
With the amount of high-quality keyboard manufacturers these days, though, and the support for variance in preferred type parameters—do you need backlighting? Mac keys?—I do not blame people for asserting the problem of picking one is undecidable.
Edit: Nevermind, I think I just missed the joke maybe
Then I realized it was Haskell zealotry :-(
I'm not arguing for or against undecidability in type systems, the page aims to be present the information neutrally.
Can anyone comment on Ada's type system?
Julia also has Common Lisp-like multimethods, which are pretty nice, especially for linear algebra sorts of stuff, where you might be multiplying a scalar by a tensor, or a tensor by a tensor, and don't want to have to specify different syntax for the two operations.
What would you describe as dynamic typechecking then? Would Scheme be a language that would fall under your definition, since it has much less dynamic dispatch?
> isn’t inserting any meaningful check until the last possible moment when there is nothing left to do but blow up anyway
I mean, inserting it earlier would require static knowledge of types, no?
> Not sure about Julia behavior, but I would guess that it also isn’t going to be sprinkling dynamic checks all over given its aspirations toward performance.
Haven't used it since I took a linalg class in undergrad, but my understanding was that Julia does similar dynamic dispatch, but it's using a JIT, and does type propagation. As a result, once operand types are known, the compiler is free to monomorphize and inline.
A coworker wrote a thing to do this for Common Lisp, too (for some numerical code); if you're willing to give up a bit of dynamism, you can get quite a bit of performance out of this.
I’m not sure about Scheme because I’m not very familiar, but one possibility is simply that “dynamic type checking” is meaningless. In other words, one could argue that anything that blows up at runtime is “runtime type checked” but that doesn’t seem meaningful. The only meaningful definition of “runtime type checking” that I can think of is explicit comparisons between a type annotation and a value’s runtime type information, for example, given this Python:
def foo(a: str) -> bool:
return a.startswith(“foo”)
if not isinstance(a, str):
raise TypeError(“‘a’ is not a str”)
But these are different IMO than just blowing up at the last possible moment because there is no reasonable way to continue the program.
> I mean, inserting it earlier would require static knowledge of types, no?
First of all, even if it did require knowledge of static types, it could still be checked at runtime and thus runtime type checked. Secondly, many types aren’t known statically—consider types that are programmatically generated, such as are common when using SQLAlchemy, boto, etc. The interpreter could still type check these at runtime via either the JIT type-checking method described above or the flat-footed insertion of an isinstance() check at the start of the function (but I would argue that the later the type checking happens the less useful and meaningful it becomes).
> Haven't used it since I took a linalg class in undergrad, but my understanding was that Julia does similar dynamic dispatch, but it's using a JIT, and does type propagation. As a result, once operand types are known, the compiler is free to monomorphize and inline.
This sounds like the JIT type checking method that I described above, which is a concrete example of a meaningful runtime type checking example (as opposed to the notion that Python/JS does type checking at runtime which is either meaningless or incorrect IMO).
> one possibility is simply that “dynamic type checking” is meaningless.
If I take your quotation out of context, this was the assumption of some people who separated languages into simply "strongly" vs "weakly" typed, by which they meant "checked by compiler" vs "not checked". It's incorrect though, and is the reason for separate "static" vs "dynamic" distinction.
C is a famous example of static (checked at compile time) but weak (≈ unsound) typing — compiler will happily accept programs that corrupt memory in all kinds of ways. mutating "const" variable, freeing used memory, crashing, remote code execution, and more... I don't think there are any invariants that a C compiler can enforce.
Scheme, Python, Lua, Javascript etc. OTOH, have no static (= compile-time) type checking, yet they maintain some invariants! An object that has pointers to it will not be freed; An object's type is known, and will not change (well, some class transmutation is allowed but some not, an int will not turn into an array); Some types are immutable; You can never divide a string / string! etc...
Moreover, by maintaining run-time metadata about object's types, they can tell you specifically that an operation raised a TypeError. Thus these languages are strongly typed at run time.
IOW, I'm arguing that anything that blows up at run time is checked IFF it tells you it was a type error. This is meaningful compared to C segfaults that tell you nothing :-)
---
The Java paper https://dl.acm.org/doi/pdf/10.1145/2983990.2984004 shows an interesting subtlety. "Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM" — yet they present unsound programs that "type-checks according to the Java Language Specification and is compiled by javac, version 1.8.0_25".
What gives? If a bad program compiles, how come JVM is still sound? See, Java has two type systems!
- JVM is the runtime, intended to be capable of loading even untrusted bytecode yet still maintain some type invariants. It manages memory and type metadata, and for this bad program will correctly identify type violation at run-time: "When executed, a ClassCastExceptionis thrown inside the main method with the message “java.lang.Integer cannot be cast to java.lang.String”"
- The compilers uses a distinct more complex static type system. The question of soundness is: can any program that passed the compiler cause JVM run-time type errors?
+ Java language allows you to write type casts. These are deliberate "trust me" holes in the *static* type system, whose specified semantics is: JVM will check type at run time and raise exception if not as programmer promised.
As https://typing-is-hard.ch/#what-about-unsafe-casts says, since these are deliberate, and fall back to meaningful run-time type checking(!), let's ignore them — redefine "soundness" as: can a program with no exclicit casts cause a run-time type error?
+ Generics only exist in static type system!
They are invisible to JVM (aka "type erasure"), they compile into dynamically checked casts.
Their soundness goal was that the compiler can prove these implicit casts will never fail — e.g. you can only put candies into ArrayList<Candy>, so arr.get(0).eat() is guaranteed to give you a candy you can eat.
That paper demonstrates a simple 17-line program with no explicit casts that compiles yet causes run time type error.
If you think what type soundness means, ALL statically typed languages have 2 type systems! There are execution semantics — what it means to, say, compute number + number. And there is a static language of talking about types that aims to predict / prove the types that will be involved at run time. Static checking fails if they don't match. Dynamic checking largely fails when you don't do it :-) But also when you erased info you needed to do it.
A type system is a means to prove the absence of certain errors in a program.
Think of a type system as a park pilot that sounds an alarm before you hit an obstacle. What python does is the crashing sound when you hit the obstacle. Forth is finding the dent days later and wondering where the eff that came from. Python is more conclusive then Forth, but you still have a dent.
I do wonder how far you can go without letting go of unsound-ness in practice though. Convenience is nice, guarantees are very very nice
I personally think the whole typing movement of the last decade has been mostly a red herring. What I mean with that is that it appears to try solve the "wrong" problem. While strong typing certainly can solve a whole class of bugs, my impression is that where this has been required most, ended up always situations where horrible overall design and code quality were the actual main problems (not typing).
Coming from a (embedded) assembly and C direction myself, I have nothing against strong typing. But what has consistently rubbed me the wrong way about this modern strong typing "movement", both intuitively and rationally, is how it appears to fix something that is essentially broken on a whole different level. No amount of strong typing is going to fix that.
I know, nothing much actionable or concrete here. Just my opinion. Regardless, this old geezer certainly agrees with the overall impression that "unsound" is pretty much the state of this art, these days.
I have a little over 30 years of programming experience, the majority of it in statically typed languages (and quite a few). I have absolutely nothing against them (on the contrary).
I still remember the rise in popularity of dynamically types languages, and how/why they were promoted. Faster development and code simplification, by only doing data validation where it was really needed (at run time), among them. Whether that was a good development, depends on where you stand. Do you care about correct software? Are you a business making software for profit, minimizing development costs? Are you part of a constantly growing market, where programmers who properly understand CS fundamentals are increasingly harder to find (or just more expensive)?
Either way, to me it's no surprise that dynamically typed languages became as popular as they did, nor would I say that it is totally without merit (depending on your perspective). Sadly, it's also a heck of a lot easier to make utter garbage with dynamically typed languages. Not in the least because a programmer would no longer be confronted with their intellectual excrement at compile time. Unless all edge cases are properly tested during dev time, those usually become "user problems" during run time.
People like me have frequently warned consultancy clients about the dangers of technologies and languages based on dynamically typed data, but more often than not other factors that were deemed more important. Fair enough, at least from a business perspective. Maybe not so much from an ethic and/or legal liability standpoint, but somehow the software industry has managed to create itself a rather unique immunity from legal consequence as the result of horrendous software quality (so good luck selling a need for better software).
Sure, the contemporary static typing movement (as I like to call it) does appear to have genuine intentions to assist programmer (some of which should probably not even be allowed to code) to write substantially less buggy code. But I certainly do not agree with this idea that static typing will extend both mediocre and great programmers. In fact, if any of contemporary statically typed languages (or worse: ad-hoc extensions to dynamically typed languages) make somebody write substantially better software, then I firmly believe that this person either has fundamental CS related problems, or is being rushed/pressured too much to ever produce anything of considerable quality. I sincerely doubt that a statically typed language (or language add-on) will ever fix either of those.
Such programmers will nonetheless still be good enough for a lot of regular programming gigs though. But, for the love of the gods, please keep those people miles away from anything embedded or kernel-level code.
Again, I think you mean nothing but good. You may even know far more on the subject than I can expect, just based on your response. Either way, I certainly don't mean to offend you. Still, whenever I read a response like your's, I can't escape the feeling that it sounds more like a repeated mantra than that in comes from a deep understanding of the actual problem, including its long/complicated history.
This is a trap many programmers fall into. You should be parsing, not validating[0]. If you are ingesting JSON data, for instance, what you need is not a generic JSON parser but a parser that only accepts JSON representations that map to a particular, static data type and throws parse errors where in a dynamic language you might find "validation errors", for example, an unknown data field or a field value of the wrong type.
Getting the types right early doesn't substantially slow you down overall, and yields a result that's much, much easier to get correct. Any such slowdown is a greater "capex" in the form of initial development, that's more than offset by much, much lower "opex" in the form of maintenance.
> In fact, if any of contemporary statically typed languages (or worse: ad-hoc extensions to dynamically typed languages) make somebody write substantially better software, then I firmly believe that this person either has fundamental CS related problems, or is being rushed/pressured too much to ever produce anything of considerable quality. I sincerely doubt that a statically typed language (or language add-on) will ever fix either of those.
This is wrong, and it's wrong for "theory vs. reality" reasons. Take one of the languages in your background: C. What you see may be true of a hypothetical programmer who knows all the arcane rules to C and can avoid tripping one of C's many, many UB landmines the first time, every time. But most programmers in the real world are human beings who may not have had their coffee. And they are going to make mistakes and unwittingly trip UB landmines. And this is as true of great C programmers as it is of beginners. You could build some strong rules around C, such as "allocate memory as little as humanly possible" and "avoid threading unless you can justify needing the performance gains" that will help programmers stay well clear of the traps inherent to C programming. Or you can switch to Rust, and fearlessly write code that allocates memory and even threaded code, because Rust's type system guarantees memory safety and a lack of data races.
[0] https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
Maybe it was an unfortunate choice of words on my part. Additionally, and I only meant to indicated how it was promoted/advertised, rather than make any statement about weather it was a sound argument. Either way, at the end of the day, a parser is a validator all the same.
Sure, more (domain) specific parsers indeed make better code (duh). That's true for both compile time and run time parsing. But how often, in real life business situation, is there enough time to create a solid architecture and fully fleshed out (domain) specific (run time, or compile time) parsers?
Again, I'm not disputing that statically typed languages may have a potential for creating more structurally healthy code. However, from my experience it still takes a hell of a lot of time and effort (for which there often is no room in real life business situations). Dynamically typed languages often create seriously flawed software, no doubt about that. But I'm convinced that this is more because many programmers just don't do what they actually should be doing in any case (in any language).
Statically types language can alleviate that problem a little, by forcing programmers to think more about what they should already be thinking about in the first place. But it is not a magic bullet. I'm not even going to discuss the downsides from overly specified/specific software code.
> This is wrong, and it's wrong for "theory vs. reality" reasons.
In case you missed it: my main gripe with all of this is that I just can not find any of all these great improvements, that evangelists keep pushing, in actual real world examples (at least not within my personal experience). Yet here you try to convince me that my point it too much theory and telling me a story about how real world programming actually works. Seriously? I mentioned C to indicate from which direction in the industry I come from, nothing more. Well, maybe also to indicate that I've been doing this for some time now.
No need to tell me how programmers work (plenty of experience with that), or making excuses for how it's just human nature for them to fuck up if they aren't held by their hand. I might have bought that kind of bullshit 25 years go. There have been plenty of attempts, purporting to to give programmers better tools and assist them writing better software. Most of them with only good intentions. Nothing new about that, about as old as commercial software itself. However, I've seen a rather depressing trend how all of those hardly ever held up in reality, over time. Whether that is because the knowledge level of programmers constantly degrades, or if it is because such solutions promote laziness, that might be more of a philosophical discussion and hard to establish as fact.
I find it at least a bit ironic though, how I apparently am being schooled on how I "just don't get it right", by what to me sounds and smells a hell of a lot like theoretical evangelical drivel itself. In fact, at this point I can't help but recall an iconic argument about how plants crave Brawndo, because of the electrolytes.
Keep on programming the way you do. If you are a good programmer, it shouldn't matter which language or tools you use. I wish you nothing but the best and good luck. Time will tell if Rust will survive the hype and actually deliver what it has been promising for a while. Maybe it indeed will. I'm not holding my breath though. Especially not since (nontransparent) corporate influence/control on languages and tools in becoming an ever growing factor (with all kind of problems associated with it).
Many older languages with ad-hoc type systems are unsound, but there are also some older relatively used languages with powerful and sound type systems like Haskell.
Long version:
Being Turing Complete means that a system can compute everything that a Turing Machine can compute.
For a long time, it was an open question whether there was a way to determine whether, for a given statement, one could determine whether it was universally valid.
Alan Turing's creation of the Turing Machine was originally in order to try to answer this question. The idea was that to determine if a statement was universally valid, one would need to be able to mechanically derive the statement from the axioms of logic - i.e., there would be an algorithm (which Turing formalized as a "Turing Machine") that would be able to take the input and decide whether it was universally valid.
Turing then proved - likely his greatest claim to fame - that such an algorithm could not exist - as one can always build an input for which it will be forced to give the wrong answer.
Hence, Turing showed that for any Turing Machine - or any system equivalent to a Turing Machine - which answers "yes" or "no" to some input, it is impossible to decide whether it accepts its input in finite time.
Intuitively you should probably think of this as a slight extension of the halting problem, you can't always tell whether or not something (your type checking) halts. It's not that much of a leap to say that you can't tell whether it will halt after an even number or odd number of steps if it does halt (this doesn't immediately follow from the halting problem, but it is true). Imagine if you had a type that said "if it takes an even number of steps for some given computation to halt, I'm 'type A', if it takes an odd number I'm 'type B'". That's something a turing complete type system can do, and since you can't tell whether it will take an even or odd number of steps you can't tell whether or not the variable is 'type A' or 'type B'.
If it's undecidable it's not necessarily turing complete, but it's very easy to be accidentally turing complete, so it probably is.