12 ms·
Typing Is Hard
- deleted 6y ago[deleted]
- enricozb 6y agoWhat a cool resource. I've been meaning to finish an MVP for a programming language I've been trying to write, and it's pretty encouraging how many languages use undecidable type systems.
- clashmeifyoucan 6y agoAh, I recently started using type hints in Python. Would've loved to see how that compares even though it's not inherently a statically typed language!
- singhrac 6y agoPython's type system is an instance of "gradual typing" (like e.g. TypeScript). PEP 483 is actually a nice introduction to this: https://www.python.org/dev/peps/pep-0483/ https://www.python.org/dev/peps/pep-0483/
- clashmeifyoucan 6y agoRight, it should still be possible to statically type it for the purpose of testing. Wouldn't really be close to practical usage but I'd still be interested in seeing how it compares.
- deleted 6y ago[deleted]
- kps 6y agoIf you have some form of Turing-complete macros, then macro processing might not terminate. I don't see why this is anything but trivial, or a compelling argument against Turing-complete macros.
- tlb 6y agoI don't think it's a compelling argument against having such a language. But you might want to know what you're up against if, say, you decide to write an autocompleter for your editor that needs to know types.
- gpm 6y agoIf you're writing an autocompleter, you have the bigger problem that it has to function when the program isn't valid syntax, or is valid syntax but has just plain contradictory type information and doesn't typecheck. Non-terminating typechecking seems easy to handle in comparison.
- minerjoe 6y agoIn lisp and in other languages you just ask the running process.
- greggman3 6y agoBecause turing complete macros are super powerful. See lisp
- jolux 6y agoThis page isn't arguing against anything though.
- orthoxerox 6y agoA Turing-incomplete macro system will always terminate, but it may terminate in 2 years.
- curryhoward 6y agoThat's true in practice, but technically speaking it's false. You could imagine a contrived system which is not Turing complete but still contains a (rather useless) primitive that causes an infinite loop.
- 6y ago
- rtpg 6y agoAfter hearing "but Typescript is unsound!" a billion times.... kinda glad to se that being unsound is the "state of the art". 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
- gpm 6y agoI don't see how this article supports the idea that "unsoundness" is state of the art?
- elmo2you 6y agoIt may depend on age, overall knowledge of CS (including its history) and level of experience with multiple programming languages. Maybe the article itself does not literally support the idea, but it might still be inferred from it. It might also be the resulting discussion and responses, or additional field experience, that might give rise to this conclusion. 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.
- bitwize 6y agoStatic typing takes the burden of verifying certain forms of program correctness off the programmer and puts it in the compiler where it belongs, thus expanding the space of correct code the same programmer can write per unit cognitive load. The more kinds of things you check for in the type system (static lifetimes in Rust, for instance), the more benefits you get. It doesn't serve as a substitute for good taste, because while a mediocre programmer's reach is extended, a great programmer's reach is even further extended. Mediocre programmers can thus meaningfully contribute to embedded and kernel-level code under the tutelage of a good programmer without risking blowing the whole thing up, and increase their skill.
- xiaodai 6y agoWhat Julia?
- choeger 6y agoJulia has no (what some call "static" but that's actually the only form that matters) type system. It also has lisp-like macros.
- remexre 6y agoHaving no type system (e.g. Forth) is different from having dynamic checking for your types (e.g. JavaScript, Python, Julia iirc), though. 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.
- throwaway894345 6y agoI don’t see how JS or Python (not so sure about Julia) meaningfully have “dynamic checking for types”. If I have a function ‘def foo(a): return a.startswith(“foo”)’ and I pass an int in, Python doesn’t insert something like ‘if not isinstance(a, str): raise TypeError(“...”)’, partly because Python doesn’t even know that a str is expected; only that the param has a method called startswith(). And fair enough, maybe the type isn’t str in a statically typed language, but a Go-like structurally typed interface with a startswith() method; however, the function also isn’t inserting any meaningful check until the last possible moment when there is nothing left to do but blow up anyway, so I don’t see how this can meaningfully be called “dynamic type checking” when the types are all implicit and maximally abstract and the “check” is only dynamic dispatch. Pretty sure this all applies equally to JS except that a failed dynamic dispatch doesn’t raise an AttributeError but “undefined is not a function” IIRC. 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.
- 6y ago
- ekidd 6y agoPretty much any language supporting something like C++'s "template metaprogramming" will allow the programmer to perform arbitrary computation at compile time. This is, of course, "undecidable", because it's Turing complete. 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.
- guerrilla 6y ago> Pretty much any language supporting something like C++'s "template metaprogramming" will allow the programmer to perform arbitrary computation at compile time. 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.
- bmc7505 6y agoJust because the current implementation of the Idris type checker always terminates due to the size change termination heuristic does not mean that type checking Idris is decidable. If the type system as specified allows an author to express undecidable statements, it should not be considered decidable, regardless of whether one type checking implementation terminates on all inputs. If some type checker does not implement its type system, this is a property of the implementation, not the language. Otherwise any undecidable type system could easily call itself decidable by checking only a subset of the specification (in fact, this is exactly how most checkers for undecidable type systems work anyway). If the type system for a language is undecidable, type checking that language is undecidable.
- guerrilla 6y ago
- deleted 6y ago[deleted]
- fnord77 6y agowhat's the connection between being undecidable and turing complete?
- guerrilla 6y agoType checking is undecidable for type theories that are Turing-complete. Type theories are Turing complete if they can simulate a turing machine. Roughly, type chicking for a type theory is undecidable if its not decidable whether every term has the type assigned to it by the programmer. The halting problem is the connection, which the website states but the author is inviting bug reports, so maybe its a good idea to ask them to clarify it.
- pcstl 6y agotl;dr: Every Turing Complete system is undecidable - i.e. for every Turing Complete system which answers "yes" or "no", you can't determine in finite time whether, for any given input, the program will accept it or not. 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.
- gpm 6y agoIf your type system is turing complete, then it's undecidable. This is easily seen through rices theorem [0] which states that all non-trivial (not always true or always false) semantic properties (i.e. about what inputs it maps to what outputs) of turing complete programs are undecidable. In particular what type something is going to be is undecidable. 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. [0] https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem
- riwsky 6y agoCorrection: Java’s type system has been unsound since version 5; version 8 (which TFA describes as the start of the issue) just happened to be the latest version at the time it was discovered.
- ThreeFx 6y agoThanks, fixed!
- Lammy 6y agoThe headline made me hope for an article about ergonomics.
- riwsky 6y agoPeople keep arguing for array covariance as if soundness and developer ergonomics were in conflict, but upgrading your type system from a laptop keyboard to some infamously-sound Cherry MX blues shows you indeed can have both. 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.
- kjeetgill 6y agoUgh, I hate to do this, but GPT-3? Am I being paranoid? Edit: Nevermind, I think I just missed the joke maybe
- rrajasek 6y agoHeh, it accidentally ended up type punning.
- Roboprog 6y agoI was expecting something about carpal tunnel syndrome or Dvorak keyboards as well. Then I realized it was Haskell zealotry :-(
- Iceland_jack 6y agoI wish
- mathgladiator 6y agoThis is great, and I'm developing a static type system for my programming language (for board games), and I've messed up the type system so many times. 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.
- teen 6y agoPlz add dart to your list :)
- ThreeFx 6y agoIf you have resources for dart I'd be happy to include it :)
- Gehinnn 6y agoWait, C#s type system is turing complete?? Does somebody have an example type that the compiler cannot check?
- namelosw 6y agoMe too wondering if anyone can show us a proof.
- MaxBarraclough 6y agoGreat list! Can anyone comment on Ada's type system?
- p0llard 6y ago> There exist many type inference algorithms, the best known one is the so-called Algorithm W. 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/milner-type-polymorphism.pdf https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/...
- ThreeFx 6y agoBest known is indeed meant as "most widely known" (although that may be true for only my little bubble). I think it's taught in most type theory / formal methods courses though. If anybody has facts for/against this claim I'd be happy to update the page.
- kevincox 6y agoIt might make sense to update to "most widely known" to avoid that source of ambiguity. You can take that sentence as ((best known) algorithm) or (best (known algorithm))
- p0llard 6y agoYeah I think you're definitely right, and Algorithm W is how HM was introduced to me when I studied it. kevincox's comment sums up my misunderstanding.
- dnautics 6y agoIs the comment about zig correct about its typing? It's certainly true about its compilation, but that's not the same thing. Also, if you're going to have a turing-complete compile time, you might as well have it in something that looks like a programming language, since that will fit your debugging mental model.
- ThreeFx 6y agoSince you can pass types to compile-time functions, yes that is correct. Take the example [from the 0.6.0 documentation](https://ziglang.org/documentation/0.6.0/#comptime https://ziglang.org/documentation/0.6.0/#comptime) for example: At compile time the compiler has to figure out whether to type the `max` function using `u32` or `f64`. Since you can make the boolean condition arbitrarily complex the _type_ of max function called is undecidable in general. I'm not arguing for or against undecidability in type systems, the page aims to be present the information neutrally.
- dnautics 6y agoSorry, I wasn't defensive about the decidability of the type system, just curious about the analysis, which squares with my understanding of zig now! Thanks for the clarification; it might be helpful to expand on that in the doc.
- IshKebab 6y agoIt would be interesting to know the practical implications - given how many of these languages are very popular I'm assuming it doesn't really matter?
- Roboprog 6y agoReminder: strict type checking is more trouble than it’s worth for some of us. 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.
- lostmyoldone 6y agoI generally agree, except if I don't. Whether or not that is the case, I'm entirely uncertain about! 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.
- Roboprog 6y agoOne thing I don’t miss is C style Wild West access. 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.