Proposal: Existential types for interfaces and abstract types

[agocke]

Introduction

Have you ever wanted an interface (or abstract type) to be parameterized on a polymorphic variable to its implementer, but not its users? Have you ever wanted to parameterize over internal state, without revealing what that state contains to your users? This is what existential types allow you to do.

Let's look at an example.

interface class IDataFlow<TLocalState>
{
...
    TLocalState Start { get; }
    void Next(TLocalState);
    List<string> GetCurrentDataFlowDiagnostics();
}

What does this type do? Let's say it walks a data flow tree and produces diagnostics. It does so incrementally -- the user can step through the tree by first calling Start, then moving forward by calling Next and passing the current state. They can't actually view the current state represented by TLocalState, but that's OK, they don't need to! They can view the diagnostics at any point, do some computation, then decide to continue or quit. In this sense, TLocalState is a black box to the user.

However, TLocalState is anything but a black box to an implementer. They care very much that this type is generic; different data flow analyses may have wildly different state implementations depending on what they're tracking. Moreover, since they provide the state, it's not a black box to them, they'll have a concrete type in hand. For instance,

class DefiniteAssignment : IDataFlow<BitVector> { ... }

The implementer of DefiniteAssignment would be able to use BitVector statically in this implementation.

But this presents a problem. This is how a user interacts with IDataFlow:

class C
{
    void DoDataFlowAnalysis<T>(IDataFlow<T> df)
    { ... }
}

Note that the worker method must be generic, even though the type parameter is useless to them. Moreover, they have to flow this parameter around through their whole program until the entry point where they actually pass a specific data flow analysis. And if they have multiple methods that do different analyses, they have to do this for each one, on every method.

So what would we rather have? Probably something like this:

interface IDataFlow<protected TLocalState> { ... }
class DefiniteAssignment : IDataFlow<BitVector> { ... }
class C
{
    void M(IDataFlow df) { ... }
}

Now TLocalState is an existential type.

Details

Of course, the question is what is this and how does it work?

Now may be the time for a quick digression into theory to explain the background of existential types. The name comes from logic, where you can "existentially quantify" a variable, like there exists an x such that x^3 == 9. Similarly, you can also "universally quantify" a variable: for all x, x * 0 == 0.

Due to the Curry-Howard correspondence, the systems of logic and the typing calculus have parallels with one another. In the case of the C# type system, universal quantification equates to generic polymorphism. When we declare a method M<T>, this could be seen as the declaration of a function mapping from all possible Ts to a specialized M for each T. In other words, we're quantifying the method M for all possible Ts.

If we already have an analogy for universal quantification, there's a question of what existential quantification looks like. In the previous example, if we said there's an instance of M<T> for all Ts, existential quantification would say that there's a type U<T> for some specific T. Existential types are a way of working with a type variable that's set to something but you don't know what it is.

With that brief divergence done, we should now talk about how this feature would be implemented. For this, I'm going to turn to a simpler example. Say we have a counter interface:

interface ICounter<protected T>
{
    T Start { get; }
    void Next(T current);
    bool Done { get; }
}

Here's how we could use it:

void M(ICounter ic)
{
    var x = ic.Start;
    while (!ic.Done)
    {
        x = ic.Next(x);
    }
}

This immediately provokes some questions, most importantly, what is the type of x? The answer is, it's ic.T. This is some type that exists on ic. Note, it doesn't exist on ICounter -- it's not static. You can't take another instance of ICounter and unify the two T's. However, it does unify with the other T on ic; the value returned from ic.Next is the same type as the one returned from ic.Start. How exactly we want to represent this in the language is an open question. Here are the specific problems to solve:

• Will we have special syntax for this type?
• Do we need to introduce a binding in some way?
• The type clearly can't be returned or assigned to a field as is, because there is no way to mention it, so is it closer to an anonymous type?

Once we decide how to use it on the interface, we also have to decide how to implement that interface. In this case, it seems little different from an ordinary type parameter:

class Counter : ICounter<int>
{
     int Start => 0;
     int Next(int current) => current + 1;
     bool Done => current == 42;
}

Lowering

If that is how the user sees it, we also have to deal with how the CLR sees it. Luckily, we have a theorem in logic that says we can transform existential types into an encoding of universal types. I've used that theorem as a base for a transformation for C#.

Lowering from above code:

using System;
interface ICounter<T>
{
   T Start { get; }
   T Next(T current);
   bool Done(T current);
}

class Counter : ICounter<int>, ICounterWrapper
{
    public int Start => 0;
    public int Next(int current) => current + 1;
    public bool Done(int current) => current == 42;
    void ICounterWrapper.Unwrap<TWitness>(TWitness witness)
    	=> witness.Invoke(this);
}

interface ICounterWitness
{
     void Invoke<T>(ICounter<T> counter);
}

interface ICounterWrapper
{
    void Unwrap<TWitness>(TWitness w) 
        where TWitness : ICounterWitness;
}

struct MWitness : ICounterWitness
{
    public void Invoke<T>(ICounter<T> ic)
    {
        var x = ic.Start;
        while (!ic.Done(x))
        {
            x = ic.Next(x);
        }
    }
}

class C
{
    void M(ICounterWrapper wrapper)
    {
        wrapper.Unwrap(new MWitness());
    }
}

In this transformation, there are two "intermediate" interfaces that are created to transform the existential type production into a universal type production. In addition, the code which uses ICounter<protected T> has been lowered into a synthesized struct, MWitness, that executes the given code. The scope of code currently hoisted into the struct is the whole method in this example, but it it's an open question what the proper hoisting scope is -- and how this interacts with other code hoisting, like nested functions, async methods, and iterator methods.

Similarly, there are other questions like how this interacts with other language and runtime features, especially reflection, but I believe the feature is at least possible to implement on the current CLR.

[CyrusNajmabadi]

This is very very cool and interesting. Thanks for the very clearly written write-up! :)

From my quick reading, this seems to share aspects of the design with Shapes (for example Witnesses). Would this sort of design fall out as a special case of Shapes?

i.e. with Shapes you have to define the actual shape, and then manually provide the witness for specific types to make them works with that shape. It sounds like this proposal can automatically do that for these specific existential types.

Am i understanding this correctly? Or am i way off?

--

I also appreciate that, like shapes, this is a suggestion for a powerful language feature that should not incur implicit, unavoidable, allocation costs if someone uses it. Big +1 on language features behaving that way.

[CyrusNajmabadi]

The scope of code currently hoisted into the struct is the whole method in this example, but it it's an open question what the proper hoisting scope is -- and how this interacts with other code hoisting, like nested functions, async methods, and iterator methods.

It seems like the appropriate location would sometimes have to be as a nested type in the containing class. i.e. ignoring optimizations, you'd generally have to do something like this:

class C
{
  void M(ICounterWrapper wrapper)
  {
    wrapper.Unwrap(new MWitness(this));
  }

  private struct MWitness : ICounterWitness
  {
    private C _this;
    public MWitness(C _this) => this._this = _this;

    public void Invoke<T>(ICounter<T> ic)
    {
      var x = ic.Start;
      while (!ic.Done(x))
      {
        x = ic.Next(x);
      }
   }
  }
}

This way you could appropriate translate calls inside C.M to 'this' into the rewritten instance method. Note: it's unclear how things like base virtual calls would work in a verifiable manner. But perhaps it's ok if they don't or maybe there are tricks to make them work (maybe bridge methods of some sort?).

Actually, given that we support generating nested private classes for all sorts of things today, i imagine that this shouldn't be an issue. Or, at the very least, the same restrictions that exist for those cases would exist for this feature as well.

[CyrusNajmabadi]

class C
{
    void M(ICounter counter);

// becomes

class C
{
    void M(ICounterWrapper wrapper)

This is treading into interesting ground for C#. In general the signature you write is the signature you see in metadata. (Though clearly, things like tuples/dynamic show we're moving away from that). Is your thought that things like ICounterWrapper would be completely hidden from users, and people would only ever see this as ICounter ?

[CyrusNajmabadi]

You can't take another instance of ICounter and unify the two T's

This will probably need some very deliberate work to make good error messages.

For example:

void M(List<ICounter> list) {
  var counter1 = list[0];
  var counter2 = list[1]; 

  var start1 = counter1.Start;
  var start2 = counter2.Start;

  // What are good errors here:
  counter1 = counter2;
  start1 = start2;
}

In essence, under the covers this would be treated (AFAICT) as if you had written.

void M(List<ICounter> list) {
  ICounter<UnspeakableType1_UsedFor_ICounter_T> counter1 = list[0];
  ICounter<UnspeakableType1_UsedFor_ICounter_T> counter2 = list[1]; 

  var start1 = counter1.Start;
  var start2 = counter2.Start;

  // What are good errors here:
  counter1 = counter2;
  start1 = start2;
}

I'm not even sure how to best phrase the error for the user. :)

Any thoughts on how to best explain this to hte user?

[alrz]

this seems to share aspects of the design with Shapes (for example Witnesses). Would this sort of design fall out as a special case of Shapes?

Just wanted to point out that shapes can actually use this feature under the hood to provide an implicit type parameter e.g. TSelf which would be the type of the implementation target.

// implicitly defined for all traits
trait Eq< /* protected TSelf, */ Rhs = TSelf> {
// ...
}

implement Eq for SomeType { // TSelf = SomeType, Rhs = SomeType
 // ...
}

From what I've seen in Rust, this type parameter is crucial to define and implement traits/shapes.

[agocke]

@CyrusNajmabadi Very good questions, and I'm not going to pretend I have direct answers for all of them. Here's what I have so far:

i.e. with Shapes you have to define the actual shape, and then manually provide the witness for specific types to make them works with that shape. It sounds like this proposal can automatically do that for these specific existential types.

I think this is correct. I have to read the shapes proposal to understand this more, but I think they have elements of existential types. What I would say is the primary differentiation is that an existential type on an interface is part of the actual type, while shapes seem to be limited to generic constraints on a type parameter.

It seems like the appropriate location would sometimes have to be as a nested type in the containing class. i.e. ignoring optimizations, you'd generally have to do something like this

Yes, this is true. If you can imagine a kind of inline-struct declaration syntax for C#, I think the more appropriate phrasing is something like

void M(ICounterWrapper w)
{
    w.Unwrap(new MWitness : ICounterWitness
{
    void Invoke ....
});
}

This makes it more clear that the scoping of the generated type really belongs to the scope of the method it's used in. This is where parallels with anonymous types and closure conversion come in.

In general the signature you write is the signature you see in metadata

This is, I think, an open question of what we have in source and what we generate in metadata. Maybe the wrapper type is what you see in source and in metadata. Then there's really no difference at the use site. However, at the interface site you'll see a difference between what the source containing type is and the runtime containing type is. I don't yet have a good idea how to resolve these ambiguities.

Any thoughts on how to best explain this to hte user?

This is entering a level of practicality I haven't worked out yet. 😉 Mathematically, I think this is basically explaining to a user that, in terms of universal quantification, List<T> is not the same as List<U>. I'm not exactly sure how to port that explanation over, but I think it should fit in the same mold.

[evincarofautumn]

For functions that take existentials like (∃x. A) → B (e.g. void M(ICounter)), you can encode them as just ∀x. A → B (void M<T>(ICounter<T>)) by Skolem normalisation. The programmer would write void M(ICounter) as you’ve done here, and the compiler would emit void M<T>(ICounter<T>). That solves the problem of having to explicitly thread the type variable through all the use sites, and it’s easy to understand.

You’d still have to do something like your proposed desugaring (CPS conversion) to handle functions that return existentials. (It looks like you’d basically encode A → ∃x. B (ICounter MakeCounter()) as ∀r. A × (∀x. B → r) → r (<R> R MakeCounter(<T> Func<ICounter<T>, R>)) but working around the lack of higher-ranked universal quantification.)

Also, to bikeshed: using <protected T> suggests that something like <private T> or <internal T> might work, but they don’t have any clear meaning. I think <virtual T> would be more illustrative—it’s not an access modifier, but a polymorphism modifier.

[jnm2]

I'm super excited about the idea that we might get associated types! I've thought that would be cool in theory long before I knew what they were called. Also, anything we can do to reduce the need for declaring gratuitous generic parameters (and specifying them for overload resolution) is a welcome relief!

[gulshan]

Does this proposal somehow aligns with my "Type pattern for generic types" #268 proposal, proposing inference of type parameter for generic types in patterns.

[MadsTorgersen]

Great proposal!

This approach to existential types has a lot in common with virtual types in Beta or abstract types in Scala. I wonder if it were more syntactically intuitive to use a notation closer to those, where the type "parameter" is declared as a kind of abstract member of the class:

interface ICounter
{
    type T; // or some such syntax, could have a where clause
    T Start { get; }
    void Next(T current);
    bool Done { get; }
}

class Counter : ICounter
{
     public type T = int;
     int Start => 0;
     int Next(int current) => current + 1;
     bool Done => current == 42;
}

That way it becomes clear that the type T really is a member of a given instance of ICounter, and is tied to the instance.

A problem in both your formulation and mine is that in the usage:

void M(ICounter ic)
{
    var x = ic.Start;
    while (!ic.Done)
    {
        x = ic.Next(x);
    }
}

You assume that ic.Ts coming out of ic can be fed back in as ic.Ts of that same ic. That is only true and sound insofar as you trust the value of the ic variable not to have changed. In a pervasively mutable language such as C# this is far from given. Thus, the feature is probably best when coupled with the ability to declare parameters and locals readonly.

[gafter]

I'm very happy to see @agocke's clear description of this feature, which I think has real potential.

[alrz]

You assume that ic.Ts coming out of ic can be fed back in as ic.Ts of that same ic. That is only true and sound insofar as you trust the value of the ic variable not to have changed

In Rust, you are only allowed to omit associated types if you use the trait as a generic constraint, that would freely give you such guarantee, as long as all variables are of the same type parameter.

 interface ICounter {
    type T;
    T Start { get; }
    T Next(T current);
    bool Done { get; }
 }

void M<C>(C ic)
  // it's only allowed as a type constraint when type arguments are omitted 
  where C : ICounter 
{
    var x = ic.Start;
    while (!ic.Done)
    {
        x = ic.Next(x);
    }
}

So the above could be lowered to the following (considering that restriction),

void M<C, __T>(C ic)
  where C : ICounter<__T>
{
    var x = ic.Start;
    while (!ic.Done)
    {
        x = ic.Next(x);
    }
}

No need for x to be readonly at all.

Note: the generated type parameter __T would need to inherit all the constraints from C::T. It'd be called an "associated type" due to the fact that it's associated with the type C.

--

I think something like "inline type constraints" (#279) could help here to bring the constraint closer to the type parameter declaration for the sake of readability.

void M<C : ICounter>(C ic)

Again, in Rust you can refer to associated types with a :: operator. In C# that would look like this:

void M<C : ICounter>(C ic, C::T item)
// ->
void M<C, __T>(C ic, __T item) where C : ICounter<__T>

And if you do want to explicitly provide type arguments (for example, if you want to use it in fields, parameters, etc), you could use "named type arguments" (#280)

void M(ICounter<T: int> ic)

[alrz]

We could avoid all the new syntax here by converting

void M(ICounter ic)

to

void M<__C, __T>(__C ic) where __C : ICounter<__T>

That would save a lot of syntax changes. But I'm not sure if we could actually allow this for all interfaces?

(however, there would be no way to refer to the type __T here i.e. C::T in the examples above.)

[agocke]

@alrz I think your transformation is unsound. Aside from making an existential type viral, as you'd now have to push your hidden type parameter all the way up the chain, consider

void M(ICounter c1, ICounter c2)
{
    c1 = c2;
}

Both terms should have the same type, so this should be legal. But with your transformation this is probably something like

void M<__C1, __T1, __C2, __T2>(__C1 c1, __C2 c2) 
    where __C1 : ICounter<__T1>, __C2 : ICounter<__T2>

which does not type check.