> 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-Milne

> 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#coercions http://homepages.inf.ed.ac.uk/wadler/topics/recent.html#coer...