Hacker News new | past | comments | ask | show | jobs | submit login

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'.




> In a gradual type system, the type system is complete

Exactly!

Edit: Also, the gradual typing theory as described by Siek in a language with a Hindley-Milner like static type system supports type inference, so it will automatically use as much type information as possible.

More on this, including how to smartly compile gradually typed languages so that functions don't explode in size when they are being passed between statically and dynamically typed code, in the paper:

Blame, coercions, and threesomes, precisely Jeremy Siek, Peter Thiemann, and Philip Wadler. Draft, March 2014.

http://homepages.inf.ed.ac.uk/wadler/topics/recent.html#coer...




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: