As someone who strongly prefers static types, I can't believe I am saying this but I don't love the trend of dunking on dynamically typed languages as "merely" unityped/badly statically typed. Dynamism has its own rich history, including contributions to static typing.
Dynamic programs have driven interest and innovation in subtyping, refinement types, richer type predicates, and flow-sensitive static analysis. All of these directions improve the expressivity of sound static type systems in addition to any gradually-typed applications.
What really bothers me about the "uni-typing" worldview, though, is that it reduces a culturally and intellectually rich field (dynamic typing) to an equivalent formulation (solution to domain equation D≅D→D) while asserting that this notion of equivalence is all that matters.
Like, it's undoubtedly cool and elegant that you can express the untyped lambda calculus using recursive types while preserving the properties of interest to ML-istas/Bob campers. But these still represent a particular choice of properties, a particular definition of equivalence
All types expressed in Hindley-Milner can be expressed with subtyping, but not vice versa. Does that make HM just "bad subtyping"? If you choose to prioritize expressivity then maybe, but sometimes we care about decidability and inference too.
Dynamically-typed languages pioneered work in macros, delimited control, message passing/actor runtimes, and other areas of tremendous relevance to modern programming. Typed variants of the above exist, but the heart of these efforts are closely associated with dynamic languages.
Just because these directions are less interesting to type purists do not make them less globally interesting. Syntactic abstractions and typeclasses are simply two bicycles for metaprogramming in very different ways. It would be weird to criticize one within the other's frame.
Two asides here. First, a lot of static typing superiority is based on comparisons between typed and untyped languages in a situation where types excel, such as large-scale refactoring. Based on these examples, we conclude that static typing is just *better*.
Alone, this is inadequate for rigorous comparison. Consider also situations where dynamism enables things our stringent static types couldn't handle: intricate macro metaprogramming, WebAssembly stack manipulation, and so on. This is where dynamically typed languages shine.
Maybe you're like "meh, Erlang is cool but I care more about provable correctness than having my telecommunications withstand a simultaneous shark attack and server fire". That's fine (same), but the key is to recognize the implicit value judgment. Everything is a trade-off
Second aside: I think people often conflate "experience with static typing" and "experience with particular statically typed languages". A type system is one of many factors; ATS is supposedly god-tier but I don't actually know anyone who has written a program in it and survived
Anyways, defining the untyped lambda calculus using recursive types is clever and elegant, but when it turns into "uni-type" drum-beating it starts to feel a bit like taking the rank-1 approximation of a matrix and just pretending that's the whole thing.
We want better programming languages. I think static types are part of the picture, but it is unquestionably narrow to dismiss contributions from dynamically-typed languages. Btw if you liked this thread, please consider awarding me an NSF GRFP
tl;dr unityped is a very cool equivalence but not a moral judgment so it makes me uneasy when people start deploying it as the latter bc it often works to dismiss the contributions of dynamic langs! (h/t @sivawashere and Pedro Amorim for helping w the wording here)
Correction: assembly, not WebAssembly. One downside of WebAssembly's lovely safe runtime is that it does *not* offer a good stack manipulation API, necessary for implementing performant continuations, exceptions, green threads, etc.
• • •
Missing some Tweet in this thread? You can try to
force a refresh
