[RFC] Kappa and polymorphism

[EliasC]

Problem

Parametric polymorphism is useful for writing general code because it abstracts over the type of arguments and fields:

def id[t](x : t) : t
  x
end

class C[t]
  var f : t
end

In Kappa however, the type of a value sometimes incurs restrictions on how that value may be used, for example by precluding sharing (local) or aliasing (linear). By abstracting "too far", we may lose information about these restrictions and possibly break them:

def duplicate[t](x : t) : (t, t)
  (x, x)
end

def leak[t](x : t) : Thief[t]
  val thief = new Thief[t]()
  thief ! steal(x)
  thief
end

...
var x = new LinearThing()
var tup = duplicate(consume x) -- linearity of x broken!

var y = new LocalThing()
var thief = leak(y) -- y is unsafely shared!

Current approach

In the open Kappa PR, we restrict polymorphic values in two ways. First, we disallow passing polymorphic values to other actors. For the leak function above, the error is

Cannot pass polymorphic expression 'x' to another actor (it may not be safe to share).

Secondly, we disallow using linear (and subord) values as type arguments. When calling the duplicate function above, the error is

Cannot use linear type 'LinearThing' as type argument

The type arguments that are allowed in practice are primitive types, and capabilities with the mode read, local or active. This will most likely cover most use-cases of polymorphism, but since we are developing a language for concurrency and parallelism, it would be a shame to disallow thread communication in polymorphic contexts.

More general solution: bounded mode polymorphism

In a feature branch based on Kappa, I have implemented an extension to parametric polymorphism which allows specifying bounds on the mode of a type argument. To abstract over the types whose values are safe to share across active objects (primitives, read and active), there is a new abstract mode shared. For example, we can safely make the the leak function compile by annotating its type parameter as shared:

def leak[shared t](x : t) : Thief[t]
  val thief = new Thief[t]()
  thief ! steal(x)
  thief
end

When trying to call leak with a local value, the type error is

Cannot use local type 'localThing' as type argument. Expected a shared type.

If we wanted leak to work for linear types as well, we would annotate it as linear, requiring us to consume x when we send it to the Thief. Notably, when leak has a type parameter marked as linear, it is safe to call with non-linear values as well; treating an already aliased value linearly does not break any invariants. However, as long as we have null in the language, not all values can be consumed in a way that makes sense (what is null for an int, for example). Therefore, we require the value being consumed to be wrapped in a Maybe type (whose consuming sets the variable to Nothing):

def leak[linear t](x : Maybe[t]) : Thief[t]
  val thief = new Thief[t]()
  thief ! steal(consume x)
  thief
end

If no consume is used, there is no need to use Maybe. Also, once there is a proper flow sensitive analysis that statically disallows duplicate uses of linear values, this restriction can also be dropped.

When no mode is specified, the semantics are as described in the previous section.

[supercooldave]

Bravo! I want this! I'll read in detail and comment.

[supercooldave]

However, as long as we have null in the language, not all values can be consumed in a way that makes sense (what is null for an int, for example).

What does it mean to consume an int?

[supercooldave]

What about considering bounded type polymorphism? Would that encompass bounded mode polymorphism?

[EliasC]

What does it mean to consume an int?

Well, consuming an int doesn't mean anything, but consuming a variable means promising not to touch it for the remainder of the scope, which makes sense for variables storing ints as well. From a data-race prevention point of view, you never need to treat a primitive linearly, but for polymorphism purposes, you might do so only to be able to use the same function for both linear stuff and primitive stuff.

What about considering bounded type polymorphism? Would that encompass bounded mode polymorphism?

Definitely related, and something that we should be adding! It is however a bit different from mode polymorphism as it typically constrains the interface of the type rather than the mode. With an Any type I guess you could achieve the same thing by writing def foo[shared t]() as def foo[t : shared Any](), assuming that primitives are also subtypes of Any. When we go for implementing bounded type polymorphism, we could consider this as desugaring.

[supercooldave]

Is there something more than consuming access to the variable? For example, are you worried about the reference hanging around for the GC to misinterpret? I guess with fields it is hard to remove the "access the field" capability. Is that why you need some notion of "null"?

[EliasC]

Is there something more than consuming access to the variable? For example, are you worried about the reference hanging around for the GC to misinterpret?

Not really, it's just a matter of ensuring that whoever is accessing the underlying value has exclusive access. It's fine if the pointer is still on the stack, as long as it's not accessed.

I guess with fields it is hard to remove the "access the field" capability. Is that why you need some notion of "null"?

That's right. The current implementation allows consuming Maybe values (leaving Nothing behind), and when we get rid of null this will be the only way to get something from a field of linear type.

[EliasC]

Closing this since #776 was merged!