Trait theory

[kikofernandez]

I would like to be able to group things such as class Object : read TObject * linear LObject and ensure that both traits satisfy the same interface (methods), so that I can dynamically dispatch based on their mode. For instance, the following example is not allowed:

read trait TObject
  require val x : String
  def foo() : unit
    ()
  end
end

linear trait LObject
  require var x : String
  def foo() : unit
    ()
  end
end

class Object : read TObject * linear LObject      -- [ERROR in this line]
end

active class Main
  def main(): unit
    ()
  end
end

The error reads:

Conflicting inclusion of method 'foo' from trait 'TObject' and trait 'LObject'
In class 'Object'

I believe this is useful because Encore infects the modes from the inner to the outer, i.e. Par[read t] makes the type of the ParT read Par[read t]. This prevents me from writing linear Par[t] -> read Par[t] -> linear Par[t]. Same with classes: a class needs to be moded or defined by its traits, which already posses restrictions on mixing and matching read and linear, because it cannot be both at the same time and dynamically dispatch (current status that I am aware of).

In the example at the beginning, I believe it would be useful if we can abstract the mode over the class. Enters the concept of theories:

A theory statically ensures that traits with different modes implement the same interface. Example:

theory TCommon[t]
  require def foo(x: t): t
end

read trait RVector[t] : TCommon
  require val arraySize : int

  def foo(x: t): t
    print("read")
  end
end

linear trait WVector[t] : TCommon
  require var arraySize : int

  def foo(x: t): t
    print("linear")
  end
end

class VVector[t] : (RVector[t] * WVector[t]) ++ TCommon
  ...
end

active class Main
  def main(): unit
    example(new VVector(), new VVector())
  where
    fun example(v1: RVector, v2: WVector)
      dynamicDispatch(v1)     -- prints read
      dynamicDispatch(v2)     -- prints linear
    end

    fun dynamicDispatch(v : VVector): unit
      v.foo()
    end
  end
end

Based on this, we could Par[WVector] -> Par[RVector] -> Par[VVector]. From the ParT perspective, we can p >> fun (v : VVector) => v.foo() because its trait theory guarantees that the behaviour is allowed.

Notes to Kiko:

• I believe that we should make a distinction between what is common knowledge (all the traits that implement a theory have guarantees to be sound and safe) and behaviour that is specialised for the trait, aka traits with different methods. This means that even if we can statically know that not all traits in VVector implement the required method, it's more useful to explicitly state what is common knowledge and what is not (as interfaces do in Java and other PLs)
• ParT is a functional abstraction, so it's always safe to share as long as its content is safe. This means that, based on the example above, p : Par[VVector], I don't care about whether the ParT is linear or read, it's safe in any case! If we were to say p : Par[WVector], then we know that the ParT inherits the mode of the WVector.
• If we allow linear Par[t] -> read Par[t] -> linear Par[t] somehow without theories, then the idea of theories is still useful (although a bit less)