Things that also get my goat (from a less type theoretic point of view): - Assuming that type checking is the only thing you might want to do with your program

Things that also get my goat (from a less type theoretic point of view): - Assuming that type checking is the only thing you might want to do with your program at compile time. There are, in fact, arbitrarily many things you might want to do at compile time. Textual preprocessing, expansion macros, type checking, C++ template metaprogramming, etc. are all obvious examples. The fact that most languages bolt all of these things on as one-off features is a sign that something deeper is being missed (perhaps the 3-Lisp[1] idea, for example, or just consider plain ol' Lisp macros). - Assuming that totality, soundness, and lack of side effects are always type checking virtues. Sometimes I'd like a "typechecker" that isn't always guaranteed to terminate. Sometimes I'd like my typechecker to launch some missiles. This is really more about the previous point. - Assuming that type checking is NOT desired at runtime. Sometimes it is. Clojure's core.typed has the property that it is "just code" and can therefore be run at anytime and used for things other than checking that your code is safe to ship. [2] - Assuming that a program that fails type checking shouldn't be run. Maybe it should and the parts of the program that fail type checking should be run inside some monadic context. Maybe we want not only gradual typing, but gradual enforcement. Maybe if we had richer type data, then "failing type checking" wouldn't be binary. Perhaps a program that fails certain type checks has to add runtime support to enable certain features, but if the same program type checked to be about pure memory locations, the runtime would vanish and a "straight to the metal" program would remain. (In other words, maybe what we currently call a language's "runtime" should just be a residue of things that couldn't be checked at compile time, among other things.) - Assuming that types and the type checker should be a fixed feature of the language. Perhaps type checking should be something that is built as a library from language primitives. Take this far enough and you get something like exotypes. [3] Which reminds me... - Assuming that "type" is the only kind of metadata you might like to attach to a symbol, expression, or value. There are many other things I might like to express, and I might like to use the usual machinery of type checking to analyze or work with those things. Clojure's value-level metadata and Common Lisp's property lists are some good examples of generalizing this. - Focusing on manifest typing for verifiability of programs and ignoring the extra information it gives tooling. Visual Studio's IntelliSense and F#'s type providers are examples. At least one person at Microsoft has trouble sleeping at night because he or she is worrying about when the rest of us are going to figure this one out. [4] - Assuming that most programmers want one or the other. The article touched on this, but I wanted to expound a bit. I would like my original prototype to feel like play-doh and my finished product to feel like concrete. Why do I have to do this in two different languages? "Oh I'll prototype it in python and then switch to Haskell when I want it to be safe." What? - In general, assuming that it is the job of the language designer to provide the safety nets, rather than the DSL or API designer. A suitably designed programming language is one that could prevent operation Foo in layer 3 while allowing it in layers 1 and 2. This is one reason why languages like Idris are so complicated. Dependent types HAVE to be complicated because the language designer feels that it is his or her job to make sure the part of your program that runs at compile time terminates and doesn't do anything "bad". Why do we rarely question this assumption? [1] http://lisp-univ-etc.blogspot.com/2012/04/lisp-hackers-pascal-costanza.html http://lisp-univ-etc.blogspot.com/2012/04/lisp-hackers-pasca... [2] https://github.com/clojure/core.typed https://github.com/clojure/core.typed [3] http://dl.acm.org/citation.cfm?id=2594307 http://dl.acm.org/citation.cfm?id=2594307 [4] http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type-providers-in-pictures.aspx http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type...