[kccqzy]

> Most other languages I know of only have a single type for a variable

This may be pedantic, but with subtyping many OO languages can give many different distinct types for a variable. In Java you can assign any non-primitive typed expression to a variable of type Object. So almost any expression in Java can be typed as Object.

What you are describing as novel is rather the phenomenon of type refinement in a pattern match or conditional expression. When an expression undergoes pattern matching, its type becomes increasingly refined. This is a useful feature in intermediate-to-advanced Haskell (known as GADT) as well as dependently typed languages.

[alexcole]

> In Java you can assign any non-primitive typed expression to a variable of type Object.

Sure, but if you do this in Java you must use different variable names for the reference of type Animal and the reference of type Object.

I think algebraic data types and type refinement are great, but I’m not a fan of automagically changing the types of variables in different scopes if it can’t be applied consistently.