Polymorphism
Felix provides a simplified kind of template style compile time
polymorphism. All definitions and declarations can be polymorphic. A
polymophic entity is defined by suffixing its name with a comma
separated list of type variable names in square brackets, which should
be treated as universal quantifiers.
fun
f[s,t] (a:s, b:y) => b,a;
typedef S[t] = U[t,t];
module X[t] { fun g[k](x:t, y:k)=>x,y; }
Instances of polymorphic entities are refered to by supplying a list of
types:
f[int,long]
(1,2L)
typedef intlist = list[int];
Modules cannot really be polymorphic. Instead, the type variables
specified for a module are inherited by each entity defined in the
module. The inherited variables come first.
Entities defined in a polymorphic function also inherit the type
variables of that function, however these are bound implicitly to the
whatever the function's variables are bound to and cannot be specified.
This is necessary to ensure that the entity actually refers to the
activation record of the parent instance.
For functions and procedures, trailing type variables can be elided
from a reference provided they can be deduced. For example:
fun
f[s,t] (a:s, b:y) => b,a;
f(1,2L) // deduce
s->int, t->long
Polymorphic functions can be overloaded similarly to C++. First, lookup
seeks a scope containing at least one matching candidate, and then all
the matching candidates in that scope are selected. Then the most
specialised function is chosen. If there are no matches, or no single
function more specialised than all the others, the overload fails. A
function is more specialised than another if every argument matching it
matches the other, and at least one match for the other does not match
it.
More precisely, matching is a
special kind of unification in
which bindings are found for type variables in the LHS (parameter) so
that the type is the same as the argument; variables in the RHS are
treated as constants (free variables, independent variables) and cannot
be bound. This matching is the same for matching a function signature
with an argument, and for determining if a function is more general
than another.
A special sugar allows implicit specification of some type variables by
eliding the type on a function argument, for example:
fun
swap (x,y) => y,x;
is equivalent to
fun
swap[s,t] (x:s,y:t):t*s => y,x;
except that the type variables are anonymous and cannot be named
directly. The can, however, still be refered to using the typeof() operator applied to
the parameters:
fun
swap (x,y): typeof(y) * typeof(x) => y,x;
Although Felix polymorphic functions seem much like C++ templates they
are fundamentally different. Felix polymorphic entities are guarranteed
to be parametrically polymophic,
although polymorphic C bindings need not be (because the can bind
to nonparametric templates).
The difference is apparent in that Felix
does not support two phase lookup. All lookup is done in the
context of definition, so that everything other than the type variables
are fully determined in that context. For example this code is legal:
fun
f[t] (x:t) => g x;
if, and only if, g has a single polymorphic argument. In particular,
fun
g[u] (x:t)=>x;
fun g(x:int)=>x + x;
f 1; // calls the first g, result
is 1
Parametricity is absolutely vital for consistent behaviour: the
requirement comes directly from the underlying category theoretic
notion that polymorphic types are functors, and polymorphic functions
natural transformations. In particular, any function called from
inside a polymorphic function is invariant: it cannot change for any
bindings of the type variables. Therefore, selective hijacking is
impossible.
Note that the following C binding is not parametric:
fun add[t]: t * t -> t = "$1 + $2";
because the operator+() chosen depends on the argument type. This can
result in an instantiation time failure if, for example, there is no
overload for a particular type. Such a failure will occur in the C++
compiler because it is a C++ failure.
If a Felix polymorphic function type
checks all instantiations are guarranteed to work.