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