10.10.12  The Value Restriction

In general the Mythryl compiler attempts to deduce the most general type for each function. Thus, for example, the function

    fun swap (x,y) = (y,x);

could logically be assigned any one of a literally infinite number of possible types such as

    (Int, Int) -> (Int, Int)
    (Float, Int) -> (Int, Float)
    ((String, Int), Int) -> (Int, (String, Int))
    (X, X) -> (X, X)
    (X, Y) -> (Y, X)

Of these, the last is by far the most general; it allows the function to be used in the most possible contexts subject to correctness constraints. Thus, it is the most desirable from a code re-use point of view, in general. (In a particular case, of course, the programmer may intend that it be used only on more restricted types, and may explicitly declare that.)

There are some cases in which a most general type cannot be reliably induced by the compiler. For example, the problem of inferring a most general type for a set of mutually recursive functions is in general undecidable. (That is a precise mathematical term which in practice means "impossible".)

There are other cases in which it would be unsound to generalize the type of an expression. (By "generalize" we mean essentially "introduce type variables into".)

The rule univerally adopted in the functional programming world, and used by the Mythryl compiler, is called the value restriction, and says that type generalization is done only on expressions which involve no runtime side-effects — expressions which are values.

In this sense, a function is a value — it has no effect when defined, only when called. A number, or a string is also a value.

Since type generalization is rarely relevant to expressions like numbers or strings, in practice the value restriction may be taken as saying that only functions are type generalized — and only functions which are not members of mutually recursive sets of functions.

Comments and suggestions to: