[patricksli]

Optional typing is the general term for such type systems. "Gradual typing" was coined originally in a paper by Jeremy Siek and refers to a specific set of axioms that must be satisfied.

Thank you for the link though. I will see how the term is used colloquially nowadays.

[jswrenn]

The PL academic community here in New England seems to use the word in fairly broad sense. (Admittedly, type theory isn't my area, and they very well may use a different term when they actually write papers.)

There seems to be a lot of variance in what people mean by gradual/optional typing.

For example, Pyret (a language I work on) has both typed and untyped semantics. In both semantics, bindings can be optionally annotated with a type, and any Pyret program can be executed with dynamic type checking, or can be first statically type checked before executing (but doing so does not remove the dynamic checks). What should this be called? The practical effect is much the same: users can gradually add type annotations.

On the other hand, it's a far simpler approach than typed racket or reticulated python. We made the conscious decision only to include language features for which we had a static type-checking story for, wrote the compiler as if there was no static type checking, and then wrote a type inferencer/checker for the language which can be optionally enabled.

[patricksli]

Ah I have skimmed through the webpage for Pyret before. It's nice to meet you. I have some questions for you about that that I'll ask you later.

What you're describing is, I believe, one particular strategy among many with the goal of allowing users to gradually add type annotations. The goal itself is not new, and is often called optional-typing. The two words "gradual typing" specifically is also one particular strategy for optional typing but is under the ownership of Jeremy since he coined it. Informally, people do seem to use the term in a looser way.