What is Gradual Typing

Gradual typing is not the same as optional type annotations. In a gradual type system, the type system is complete. That means if you provide all type annotations, the program cannot fail with static type errors. If you provide partial type annotations, the program can only fail in dynamic code, or at the boundary of static and dynamic code. Systems with optional type annotations do not provide these guarantees.

One of the areas where this really shows up is with higher-order functions. One way of ensuring that statically typed code can't fail is to do dynamic type checks at the transitions between dynamic and statically typed code. That way, the statically typed code can always assume that type declarations are correct, and type errors can always be traced back to dynamically typed code. But what happens when dynamically typed code passes a function, the type of which it does not know, into code that expects, say, a (fixnum -> fixnum)? You can't in general type check the domain and range of an arbitrary function.

One of the key differences between optional type annotations and gradual typing is what happens in that case. In Dylan or Common Lisp, any call to a function where the target is not statically known will pollute the type information.[1] I.e. the type-checker cannot trust that a function annotated (fixnum -> fixnum) will in fact always return a fixnum. It will insert a dynamic type check on the return value. In a gradually-typed system, the compiler can make that assumption, and not insert the type check. In purely statically typed code, the type checker can ensure the type of the function when its identity is taken as a value. If the function comes through dynamically typed code, the compiler will wrap the value in a thunk at the transition point. The thunk will do the type check, and if it fails, you can trace the error not to the statically typed code where the function was called, but back to the dynamically typed code that passed in a function of incorrect type.

[1] In Dylan, you cannot even give a type for a function more specific than 'function'.

Optional type annotations do exist for ages in Common Lisp, and the optimizations are implementation specific. All good implementations do not only check the types, they are mostly used to optimize the data types (raw vs boxed) and reduce unneeded run-time type checks and unneeded generic methods. See e.g. the python compiler for SBCL, formerly knows as CMUCL.

Perl5 also has optional types since 15 years, just the implementations (checkers and optimizers) were broken in the last big refactoring around 5.10, and there's no interest in enabling it again. The optimizing perl5 compiler B::CC honors optional types (besides doing type inference for core types, IV, NV and PV) and gets a typical 2-5x speedup. http://act.yapc.eu/ye2013/talk/4637

BTW: This is a very old article, and was posted here some months ago already.

I really like this idea. Dynamic typing (especially truthy / falsy) gives you a lot of easy flexibility and conciseness, but static typing gives you a lot of "free" documentation and confidence.

So when I use Scala I'm frustrated that I have to dance for the type system to make the damn thing do what I want, and when I use Clojure I occasionally get lost down long holes of confusion only to realise that the map with params I passed to some function somewhere had an element misspelt slightly (an hour lost because I used :url instead of :uri once, no joke).

I've heard good things about core.typed, but have yet to find the time to try it out.

Edit: I've also found that in all the static languages I've tried (Scala being the one with the most comprehensive type system) you get to a point where you can't describe what you want with your type system because it's too conceptually complex, and then all your assumptions about what the type system gives you falls away.

Another interesting approach is 'success typing' in Erlang, as described in this elegant paper:

http://user.it.uu.se/~tobiasl/publications/contracts.pdf

Success typing is optionally refined through typespecs in the code and checked by the Dialyzer tool:

http://www.erlang.org/doc/reference_manual/typespec.html

http://learnyousomeerlang.com/dialyzer

Success typing is open to gradual typing of legacy code, as more typespecs are added, constraints gradually tighten, and Dialyzer finds the inconsistencies.

This is the biggest feature (for me) of Perl 6. Default to the normal dynamic typing, but add type annotations later on, as needed and/or desired.

The Perl 6 compiler will not only shift various warnings/errors from run time to compile time, it will also emit more efficient code!

> It would have been nice if the above error message was more specific and said the instance was of class ‘A’ instead of saying that it is an ‘instance’ of any old class.

It would if you used Python 3 or a new-style class.

Check opendylan [1], which blends dynamic typing with optional type annotations [2]. There's a paper [3] and a "dead" branch in github [4] with an actual implementation of gradual typing.

[1]: http://opendylan.org/

[2]: http://dylanfoundry.org/2014/08/28/type-system-overview/

[3]: http://www.itu.dk/~hame/ilc2010.pdf

[4]: https://github.com/hannesm/opendylan/tree/typed-opendylan

I want more than this. This article talks about adding type annotations, and if the variable has an annotation, then the type is checked. That is, you have to change the source code to use it.

I want a knob I can turn at compile time. "Compile this dynamically, so I can run it and play with the algorithm. OK, now I think I've iterated the algorithm enough times that I'm fairly confident in it, now turn on type errors as warnings. Now that I've cleaned up all of that, let's go back to the default, which is to compile with type issues being errors."

TypeScript is gradually typed then? You have types but also the "any" type.

I love this idea! I want to combine this with git commit checks so I can get through logical flow without types but be forced to do it the right way before I commit.

Sounds like it combines the worst features of each rather than the best. But I'll reserve judgement for using it in anger.

I like this as an idea, and I've been meaning to try it out for ages now. Excited to use it in Python.

I remember vaguely something similar was in the work for Ruby, but i cant find it again.

C# dynamic? http://msdn.microsoft.com/en-us/library/dd264736.aspx

Here is how you do it in D: http://dlang.org/phobos/std_variant.html

It's rather odd that Dart isn't mentioned. Although its types are actually assertions in disguise, they serve a similar purpose.

The `add1` method should be declared static

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.

It seems dishonest to claim to "invent" something that already exists, and is as trivially simple as "ignore errors". Haskell already has this for example in GHC: -fdefer-type-errors. Notice how it is only used for ignoring errors in known broken code, not for actually trying to leave out type checking permanently. That's because the premise that static types get in the way and it is better to not have them sometimes is false.