Fractional actors

[ggreif]

This describes an idea I had with @crusso about building a mixin system from actor fragments of fractional type

This is a writedown of a few ideas we tossed around earlier today about incorporating incomplete actors into the type system and allowing such mixins to be combined.

Motivation

Imagine a system where actors are simply non-negative natural numbers. They can receive messages — that are primes —, but only when they have that prime as a factor.
According to the fundamental theorem of arithmetic the actors have a unique decomposition into primes, so 1 will reject every message and 6 will accept 2 and 3 but reject others.

If we want to combine abilities of actors (i.e. their message vocabulary) we multiply them: the 6 we have encountered formerly combined with 5 will give an actor 30 which understands three separate messages.

For technical reasons we only allow prime exponents (≤ 1) in the factorisations, the reason for which will become clear later.

Now let's observe that an actor can send messages to any other, as well as itself, but such a send is only valid if the receiver can understand it. Also we'd like to check if the sends are valid beforehand.

Fragments

Imagine we want to build actors from pieces (a preferable methodology!), like the 30 actor we built above. The 5 fragment eventually can send message 3 to itself, but there is a problem: Checking 5 sending itself a 3 is invalid, and thus rejected.

Is this the end of the modularisation idea? Is 5 (as building block of 30) unable to send a 3 to its eventual self?

Let's entertain the idea of fractional actors: 5/3is not a natural number but a rational one, so it cannot be an actor. But it can be a building block of one with the crucial property that it can (eventually) understand the message 3 to self. So the send can be validated by considering the fragment in isolation.

Building

So, how do we combine actors from fragments? We still use the multiplication rule with the extra condition that p * q/p gives p * q, i.e. the exponent 1 on the prime in the product is dominant. This way 6 * 5/3 becomes 30 as before, and we obtain the same actor.

If the other building block is not having 3 as a prime factor, then the resulting actor is still fractional and thus second class. It still tracks the demand for a building block that can understand the message 3.

How can we extend such an idea to Motoko?

In the motivation above the types and inhabited values coincide, i.e. the fractional actor 7 * 5/3 has this rational number as type (as needed for validation). In Motoko we have a different system for typing actors than the actors themselves.

Extending actor types with demand

In Motoko types like actor { beep : () -> async () } are product types with actor { } as the neutral element under the and operation (greatest lower bound, glb).

To obtain fractional actor types we add fields that indicate demand:

actor {
  beep : () -> async ();  // manifest method
  import yeet : Int -> async Nat; // eventual method
}

Such fractional actor types can be made proper actors (i.e. installable canisters) by combining them using the and type operator. This is creating a product type, which motivates the "fractional" lingo. As with other named fields, import fields can only appear once in any actor type.

Consider

actor {
  beep : () -> async ();
  import yeet : Int -> async Nat;
} and actor {
  import beep : () -> async ();
  yeet : Int -> async Nat;
}

which results in

actor {
  beep : () -> async ();
  yeet : Int -> async Nat;
}

Fractional actors are not shared types, and can't be projected out. They can, however, be passed as arguments, saved as values and returned as results.

actor Values

When building the eventual actor, the type system checks that all import methods are counterbalanced with manifest methods, i.e. the result is not fractional.

One can build (fractional) actors from building blocks with the actor { … } (and <actor>)* syntax where the <actor> part can be an expression of actor { … } type. All fragments will have the same actor as the self reference.

Non-public viscera

The definition of an actor (i.e. Syntax.ActorU) also contains dec_fields which don't show up in the actor type, but need to be desugared in a centralised fashion. These include e.g. private utility functions and stable bindings as well as system functions and upgrade hooks. When the built actor gets lowered to IR these must be joined to a coherent whole from the mixin fragments.

We could allow more labels in fractional actor types to track private, system, stable signatures too. These would represent positive information, but wouldn't participate in sub typing relations. They would, however, be propagated by and.

Discussion

Some meta-thoughts here...

How is this related to open recursion?

This is the recursion part of it. Open means that in an inheritance setting always the most derived method is called (think calls via a vtable). But here we have no inheritance, the vocabularies of the mixins are disjoint.

Is this novel?

Probably not. Amr Sabry et al. had a few papers [1] about negative (travelling backwards in time) and fractional types more than a decade ago. I'll have to dig them out.

Is this worth a paper?

Maybe. I am not sure if there are actual type systems out there that run with the fractional idea...

Is it worth extending to module and object?

Possibly. But for these the self reference seems much less prominent.

References

[1]
Fractional Types
Roshan P. James, Zachary Sparks, Jacques Carette and Amr Sabry
https://www.cas.mcmaster.ca/~carette/PiFractional/frac.pdf

[crusso]

https://hal.science/hal-00310317/file/cmsv-long.pdf is probably a good starting point for the implementation of mixins in a CBV language. Looks pretty complicated though, but maybe we don't need the full generality.

I think it would be good to do a bit of a literature survey to see what the state of the art is. That paper is fairly old, and just a starting point.