What's the best way to minimize the need of run time checks?

[Chris Angelico]

On Sun, Aug 28, 2016 at 4:13 PM, Jussi Piitulainen
<jussi.piitulainen at helsinki.fi> wrote:
>> This is where I'm less sure. Sometimes a variable's type should be
>> broader than just one concrete type - for instance, a variable might
>> hold 1 over here, and 1.5 over there, and thus is storing either "int
>> or float" or "any number". If you have a complex hierarchy of types,
>> how do you know that this variable should be allowed to hold anything
>> up to a certain level in the hierarchy, and no further?
>
> It's not just literal values that give potential type information in a
> dynamically typed language. Another source is functions that the
> compiler knows, and this information propagates back and forth in the
> analysis of the control flow.
>
> For example, below the compiler might infer that x must be a number but
> not a complex number, then generate one type check (which it might be
> able to prove redundant) and calls to specialized versions of ceiling
> and floor.
>
>     d = ceiling(x) - floor(x)
>
> Also known is that the results of the calls are numbers and the
> difference of numbers is a number, so d gets assigned a number. Perhaps
> ceiling and floor in the language always return an int. Then d is known
> to be an int. And so on.

Right, and I understand this concept. Consider this code:

x = 5;
...
if (some_condition)
    x = "five";
else
    x = [0, 0, 0, 0, 0];

(adjust syntax to whatever language you like)

Does this mean that the type of x is int|string|list, or will this be
an error? Assuming the condition can't be known until run time (eg it
involves user input), there's no way for a static analyzer to
differentiate between this code and the form that Steven put forward:

> x = 1
> x = "hello"  # a type error, at compile time

Simple type inference would either see this as meaning that x is
int|string, or possibly it'd say "x is an int up to that second line,
and a string thereafter" (which is basically like dynamic typing but
statically checked - it's the value, not the variable, that has a
type, and checks like x.upper() would take note of that). But if it
flags it as an error, that would basically mean that the type system
is (probably deliberately) simplistic and restrictive, requiring that
x be EITHER an integer variable OR a string variable, and not both.

Which is a perfectly viable stance, but I'm just not sure if it's (a)
what is done, or (b) ideal. Particularly since it'd end up requiring
some annoying rules, like "integers and floats are compatible, but
nothing else, including user-defined types" or "integers and floats
are fundamentally different things, and if you want your variable ever
to contain a float, you have to always use 1.0 instead of just 1",
neither of which I like.

ChrisA