It's unfortunate that the only statically-typed languages mentioned are Java, C#, C and C++, which are verbose, unsound and very limited. In fact, one of the criticisms given in the good/bad list is "Type checkers only check fairly simple properties of your program.", which is true for those languages, but not for better type systems (eg. those of Idris or ATS).

There seems to be a lot of wooly-thinking going on throughout the article, which unfortunately seems typical of many pro-dynamic-typing pieces (I used to be guilty of this too, although I've since switched sides). For example, we can compare this gradually-typed Python implementation to Haskell's Data.Dynamic module (where the article's "?" is equivalent to Haskell's "Dynamic").

For example:

> the argument bound to x will be checked at run-time to make sure it is an integer before the addition is performed.

How can we "make sure" the argument bound to x is an integer? It's not specified.

We could treat the value as a blob of arbitrary bits, representing some integer in binary; however, that's not really "checking to make sure", that's "forcing it to be". It's equivalent to coercing a void* to an int* in C.

The other way, which is actually the case, is that values of type "?" don't just contain data of some unknown type, they also contain a 'tag' which indicates the type. When we "make sure it is an integer", what he really means is that we check whether the tag stored in x matches the tag we're using for integers.

This has two important consequences:

Firstly, the types in "dynamically typed" programs never change; they're always (tag, data) tuples. They are, in fact, static. We can write them easily in a statically-typed language like Idris:

    data Tag : Type where
      int : Tag
      bool : Tag
      function : Tag -> Tag -> Tag
      string : Tag
      error : Tag
      void : Tag

    -- We can compare Tags for equality 
    instance Eq Tag where
      int == int = True
      bool == bool = True
      -- ...and so on
      _ == _ = False

    typeOf : Tag -> Type
    typeOf int = Int
    typeOf bool = Bool
    typeOf (function x, y) = (typeOf x) -> (typeOf y)
    typeOf string = String
    typeOf error = String
    typeOf void = ()

    Dynamic : Type
    Dynamic = (t : Tag, val : typeOf t)

    null : Dynamic
    null = (void, ())

    true : Dynamic
    true = (bool, True)

    false : Dynamic
    false = (bool, False)

    someDynamicValues : List Dynamic
    someDynamicValues = [true,  false, (int, -123), (function int int, (+))]

    -- Function application
    applyDynamic : Dynamic -> Dynamic -> Dynamic
    applyDynamic (function i o, f) (t, x) | t == i = (o, f x)

All of these (tag, data) pairs will be statically checked, so `(int, True)` is a type error. It's not difficult to wrap this up in a nicer syntax to avoid the explicit annotations.

Secondly, what happens when the tags don't match? All the article says is this:

> Allowing the implicit converson[sic] from ? to int is unsafe, > and is what gives gradual typing the flavor of dynamic typing.

Being unsafe is a bit crap, considering that (with a bit of squinting) we can do all of this statically. In fact, does that mean we've managed to break the type system of Idris?

No; the reason this is unsafe has nothing to do with types, it's a matter of totality.

If we look at the definition of `applyDynamic`, we see it's only defined in the case where the first argument is a function (from `i` to `o`) and the second argument is a valid input to that function (`t == i`). In all other cases, the result is undefined. Hence "dynamic type errors" are actually unhandled cases (in Haskell-speak "non-exhaustive patterns"). Note that it's trivial to catch these errors statically (eg. the Glasgow Haskell Compiler gives warnings for them).

This the crucial realisation for me: dynamic typing turns ill-typed functions into a well-typed, partial functions. It lets us trade-off between rich types and expressive code, while remaining well- (statically-) typed.

With this in mind, it's clear that dynamic languages don't actually implement dynamic types very well: how do we specify what to do for unhandled cases? There are various approaches, most of which seem to be hard-coded into the language and require new, special features to be added to the interpreters. For example Python throws "TypeError" exceptions; PHP will sometimes convert values of one type to another, and other times trigger a notice/warning/error. SmallTalk's "doesNotUnderstand" approach is quite nice, but it still requires special-case handling and comes associated with a whole load of OO baggage.

In a static language, unhandled cases are trivial to fix: just wrap the result in a `Maybe` and return `Nothing` from all the unhandled cases!

    applyDynamic : Dynamic -> Dynamic -> Maybe Dynamic
    applyDynamic (function i o, f) (t, x) | t == i = Just (o, f x)
    applyDynamic _ _ = Nothing

This is the approach taken by Haskell's Data.Dynamic module, which defines the polymorphic function `fromDyn :: Dynamic -> Maybe a` to extract data out of Dynamic values. The nice thing about this approach is that Maybe forms a monad, so error-handling is performed automatically:

    dynamicMaths df dx dy = do f <- fromDyn df
                               x <- fromDyn dx
                               y <- fromDyn dy
                               return (f x + f y)

This will be `Nothing` if `df` doesn't contain a function, if `dx` or `dy` don't contain appropriate arguments for that function, or the results of that function aren't numeric. Otherwise it will be `Just n` for some number `n = f x + f y`. Since the result is also a Maybe, this will compose nicely with any other code using `fromDyn`.

So really, dynamic typing is just a design pattern for statically typed programming. If we look at the virtues of dynamic typing listed in the article we see:

> Dynamic type checking doesn’t get in your way: you can immediately run your program > without first having to change your program into a form that the type checker will accept.

As we've seen, programming with dynamic types is writing your program in a form that the type checker will accept! Specifically, we end up with `Maybe` types all over the place, which are trivially satisfied by `Nothing` (the monad takes care of that for us).

> Dynamic type checking makes it easy to deal with situations where the type of a value depends > on runtime information.

This is another wooly statement, since it conflates static types with dynamic types. As we've seen, the static types never depend on runtime information; they're all just `Dynamic` (AKA "?"). Since the type-checker only cares about the static types, it can all be inferred and checked without any effort from the programmer.

The dynamic types (the Tags) are just data, which we can handle just like anything else. Those 'situations where the [dynamic] type of a value depends on runtime information' are just situations where one element of a tuple depends on another.

Since dynamic languages don't let us access these tags directly, they force us to go through special-purpose reflection APIs like "typeof", "instanceof", etc. which I would argue is harder.

What about the drawback of static types that's mentioned?

> Static type checking makes you think more seriously about your program > which helps to further reduce bugs.

That's a bit of a misnomer; static type checking allows you to think more seriously about your program, if you want to. You might decide that rich types aren't worth using and follow a dynamic typing pattern instead, but at least you get to choose. Of course, that's a false dichotomy anyway; we can have some parts of our program use weak, dynamic types and others use strong, rich types. It's all still static.

The point is, in statically-typed languages, dynamic typing (and gradual typing) is just a design pattern. Not only is the expressiveness problem a strawman (we can write dynamic code in a static language, or trivially parse a dynamic "front end" language into an equivalent static form), but static languages give us more expressiveness (dynamic types are just regular data, "dynamic type errors" are just regular branches), more safety (by limiting which parts are dynamic, checking (static) types and totality automatically, etc.) and require no special language features. We can do this right now with existing languages.