[bitc-dev] Polymorphism in BitC / Cyclone

[Swaroop Sridhar]

Cyclone enforces a rule that only function definitions can be 
polymorphic [1] {a} {b}. This is a reasonable thing to do in Cyclone, 
where there is a distinction between functions (code) and
function pointers (data). Moreover polymorphism over functions is by far 
the most useful form of polymorphism.

However, in BitC, we cannot enforce a similar rule since functions are 
first class values.

Suppose that we said that functions are polymorphic only if they occur 
in a `defun' form:

(defun (id x) (vector 10:int32))

We can give id the principal type:
id: (forall ('a) (fn ('a) (vector (maybe int32)))

However, this rule will preclude polymorphic function references or 
other data-structures and objects containing polymorphic functions.

If we do not enforce this rule, when we cannot in general determine 
whether a function definition refers to an immutable function or a 
(possibly) mutable function (``pointer''). Therefore, as explained in 
[2], we cannot in general infer principal types (at least in the case of 
let-polymorphism).

[1]  D. Grossman, "Quantified Types in an Imperative Language" ACM 
Transactions on Programming Languages and Systems 2006.

[2] Design of Type and Mutability Inference in BitC
http://www.coyotos.org/docs/bitc/mutinfer.html

{a} The paper actually proves a stronger property than what is enforced, 
but this will not help in our inference problem.

{b} Cyclone has first-class polymorphism but requires annotation of 
function types; BitC is let-polymorphic.


Swaroop.