Static Typing (by alaric)
I read this fine blog post
And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single [sum] type!
Ah, bless. The author means well, but is confusing matters. They're kind of right that the distinction between so-called "dynamically typed languages" and so-called "statically typed languages" isn't what people think it is, but I think they've still not quite grasped it, either.
Certainly, almost all languages have types of some kind (the only real exceptions are ones that directly operate on memory as an array of bits, and expect the user to request the interpretation of any given region of memory in each operation, such as assembly language). So-called "dynamically typed languages" (let's call them SCDTLs from now on, and SCSTLs for so-called "statically typed languages") usually have numbers, and strings, and so on as separate types. What is missing in them compared to SCSTLs is the ability to say "This variable will only ever hold variables of a given type"; and the argument of the author is that, therefore, SCDTLs force every variable to be of a single "could be anything" type, while SCSTLs let you be more expressive. And in an SCSTL you could indeed create a big sum type of everything and use that for all your variables and, pow, it'd be just like a SCDTL, once you'd written all the clunky wrappers around stuff like addition to throw a run-time error if the arguments aren't all numeric, and unbox them from the sum type, and box the result up. Oh, and you need to maintin your giant Anything Sum Type, adding any user-defined types to it
That's what the author omits to mention. SCDTLs have all this automatic machinery to do that for you, while in SCSTLs you need to do it by hand! Eugh!
Working with sum types is useful. It's handy for writing programming tools such as generic container data structures. SCSTLs tend to have tools such as parametric types to act as a short-cut around the difficulties of doing that stuff with explicit sum types, but it boils down to the same kind of thing under the hood.
Now, a lot of the rhetoric around SCSTLs via SCDTLs comes from a rather blinkered viewpoint, comparing something like PHP (almost everything fails at run time!) to something like C (sum types are like pulling teeth!) - both sides have come together a long way.
Haskell is perhaps the shining example of a SCSTL nowadays, with its polymorphism and parametric typeclasses offering advanced ways to express huge sum types without having to spell them out.
And from the SCDTLs side, Common Lisp lets you declare the types of variables when you want, meaning that they are assigned the "Anything" sum type by default, but you can narrow them down when required. That gives you the convenience of an automatically-specified and automatically-unboxed Anything sum type when you want it, plus the static checkability (and efficient compilation) of finer-grained types when you want them. (And Chicken Scheme's new scrutinizer and specialisation system is a rapidly-developing example of a similiar model for Scheme, too).
And there's no reason why the SCSTLs can't come further, with an inbuilt Anything type and automatic boxing and unboxing of sum types, and more flexible type systems that can express more subtle distinctions, reducing the cases where "it's just too complex and we need to go dynamic".
Then we'll meet in the middle, and the only difference will be that SCDTLs have a syntax where type declarations are optional and default to Anything, while SCSTLs have a syntax that makes you declare types, even if they're Anything. They'll largely become interchangeable, and instead, we'll compare languages' type systems on a different scale: how complicated they are.
You see, Haskelll's type system can be hard to understand. It's quite complicated, in an attempt to be able to statically describe all the sorts of cases where people might wish they had a SCDTL instead. The development of type systems has largely been one of dealing with this; starting with things like generic container classes, then getting into complex stuff about being able to make the types of parts of a product type dependent on the values of other other members and whatnot, fine-grained types such as "odd integer", and so on. As SCDTLs gain the ability to declare types, they tend to start off with quite simple type systems, as it's easy to "just go dynamic"; they're initially happy to put in a bit of typing to speed up inner loops of numerical code and to tighten up error checking on interfaces. While languages without easy access to an Anything type rely on having a type system that can express lots of things, because it's a real pain when they have to escape it. But if they meet in the middle, the tradeoff will, instead, be one of a more complete type system that lets you check for more at compile time and gain more efficient code generation - versus the mental burden of understanding it.
I suspect that Haskell is, perhaps, a bit too far in the "complex" direction, while the support for parametric containers in Chicken Scheme is weak (why can't I define my own complex type if I create a "set" or "dict" container implementation, for example?) - we'll meet somewhere in the middle!
[Edited: Clarified the initial paragraphs a bit]
Fri 9th Nov 2012 9:58 pm 
Subscribe
By endofunctor, Sat 10th Nov 2012 @ 7:25 pm
That's quite naive, I'd have expected better from the likes of you! Built-in support of dynamic typing has benefits, just like built-in support of regular expressions (as in Perl). It's a shortcut. The fact that completely emulating dynamic typing with all its features and misfeatures in a static language tends to become unwieldy doesn't mean that its advantages can only be had this way. The static world offers several approaches to this that preserve the beneficial properties of not being so brutal as to submit to type erasure, like dynamically typed systems do. One of them and, arguably, the most important of them is that defining denotational instead of operational semantics becomes possible. That alone is sufficient to debunk the notion that it boils down to the same thing.
This also means that when both camps' languages converge at some point in the future, one will have the backing of formal methods and sound principles, and one won't, excepting herculean efforts to retrofit those.
By alaric, Mon 14th Jan 2013 @ 1:15 pm
Hmmm, a challenge! 🙂
What exactly do you mean by type erasure in this context? I'd have thought that static systems permit type erasure by statically knowing the types and generating code with that assumption, so type information is not required at run time, while dynamic systems don't have the luxury, but I'm not sure how to square that with your statement!
And how does dynamic typing hinder the definition of denotational semantics? I can define that [[1+1]] = Just 2 and [[1+"hello"]] = Nothing, surely? 🙂
Now, I think that the nature of the merging between static and dynamic languages - through dynamic languages using optional static typing, creating islands of static-ness in dynamic programs that grow and grow as the type systems get better - will inevitably entail formal methods and sound principles to build the type inferences/checkers that operate over the code in those islands... Chicken Scheme's scrutinizer, for instance, implements a pretty standard dependent type inferencer!