Throughout the last section, we had to reiterate that coroutine specs were not themselves types, but a generalization of the usual function type. That was only partly true, a simplification we made to introduce the concept. Coroutine specs can be considered as types, but they are very different from ordinary types in a language like Rust. We did leave one hint though; we first gave a definition for a coroutine interface as a trait, an interface that various types can be declared to implement. In fact, we did the same when we defined Choice. As experienced Rust developers will know, and has been assumed throughout this document, this is exactly how Rust handles function “types” already, and they are fundamentally of the same nature as coroutines and choice in this respect. All of these can be treated as “types” in the same way.
The treatment presented here is directly based on the concept of type polarity, as well as Paul-Blain Levy’s related Call-By-Push-Value. The fundamental characteristic of these systems is the division of types into the familiar data types, also called value types or positive types, and the less well-known computational types, also called codata types or negative types. Simply put, data types describe the parameter types of a function, and computational types describe the return type of a function (or perhaps more accurately, the computation that the function is doing).
The vast majority of types in Rust, in particular those that are Sized and Unpin (moveable),
are constructing by moving or writing data into a target location, whereas they can be eliminated in place
by reading this data. From a theoretical perspective, the relative order of these read operations cannot change the computation,
and thus the treatment I learned in school referred to these elimination operations as asynchronous. There is a certain sense that I won’t go into here in which this operation
loses no information.
In contrast,
because data can no longer be read once it has been moved somewhere else, the order of write operations
relative to anything else is relevant. Such construction operations are correspondingly called synchronous,
and in the same sense they do lose information.
A positive type is one whose construction is synchronous but whose elimination is asynchronous.
Expressions of such types are eagerly evaluated.
Such types tend to be inductively defined by their constructors, or what functional programmers
call data types.
In contrast, functions are something constructed entirely at compile-time; by themselves no data is moved around at runtime except for a function pointer being copied. This construction operation is asynchronous. When we do need to move around data is when we pass an argument to the function in order to eliminate the latter; this is when the real computation actually happens. The elimination of a function is thus synchronous. A type with asynchronous construction and synchronous elimination is a called a negative type. Expressions of such types are essentially lazily evaluated. Such types tend to be coinductively defined by their elimination operators (which I may at times refer to as destructors), and thus are sometimes called codata types. Functions, too, are technically defined by their elimination: the function body specifies what will happen at elimination time.
As I mentioned, most traditional data types are positive, including structs and enums. Functions types are the prime example of a negative type, except that there is no such type in Rust, only traits. Choice and coroutines also have negative “types”, since they are constructed by defining the computations that will run at elimination time. As with functions, Rust can only express such “types” as traits. However, a Rust-like language could understand these as types by accepting that negative types lack some of the capabilities of positive types. This is possible if we restrict function types to having positive parameter types and a negative return type — thus why I used those terms at the start of this page. Positive type operators must be used with positive types, and negative type operators with negative types. We also need to restrict variables of negative types, which for now means disallowing them entirely.
We can then write “curried” function types like FnOnce(A) -> FnOnce(B) -> C.
Of course, normal functions return data types all the time, and functional programmers
are used to being able to pass around functions as values. The way that polarized presentations
understand this is that we have types that convert between positive and negative types.
The negative to positive conversion, for a negative type T, can be understood as a generalized closure type:
a type that stores an ‘environment’ of some type G and is associated with a function FnOnce(G) -> T.
This should be very familiar to Rust and functional programmers.
In keeping with Rust syntax, let us say that impl T can be used where appropriate to
refer to any closure type of T known at compile time and dyn T to the general
type of all trait objects with a closure type of T and a pointer to the corresponding function.
Let us say that the syntax for creating a closure from an expression of negative type is to just
write the expression wherever the closure type is expected, such as a function argument or
a variable definition, and it will automatically be converted into a closure. Of course,
the type itself needs to be the closure type and not the negative type.
Rust does not support the use of impl in argument position, but it’s not hard
to imagine it as getting turned into a generic function.
fn invoke(f : impl FnOnce(A) -> B) -> FnOnce(A) -> B
{
...
}
doSomething(invoke(myFun))
Rust also does not support the use of dyn outside of some sort of pointer type,
but there’s no reason we could not pass in a dyn by making the pointer invisible.
fn invoke(f : dyn FnOnce(A) -> B) -> FnOnce(A) -> B
{
...
}
doSomething(invoke(myFun))
However, I think in an actual programming language, having a syntactic distinction between
positive and negative types is not very friendly.
Thus, let us instead say that all types have different “implementations” in argument and return position.
Positive types are interpreted to follow a particular calling convention when used in return position or some other
place expecting a negative type,
and similarly let us say that a bare negative type in argument position or some other positive usage
gets automatically interpreted as a positive type, dyn T conceptually but
impl T may be used for the actual implementation if possible.
Then we can just write:
fn invoke(f : FnOnce(A) -> B) -> FnOnce(A) -> B
{
...
}
doSomething(invoke(myFun))
Applying this same principle to variables implies that we can have variables of “negative type”, but they will be using the closure implementation to do so.
fn invoke(f : FnOnce(A) -> B) -> FnOnce(A) -> B
{
...
}
let g : FnOnce(A) -> B = invoke(myFun);
That being said, an ideal compiler would inline uses of negative variables where possible.
We can also still add traits to this with the T + Trait1 + Trait2 syntax.
For positive types though, if T does not already implement all these traits then it will
mean a closure that returns T that does implement all these traits. This would make more sense
if we could actually guarantee these closures were pure, and ideally we would not be explicitly providing
a closure but just an expression of type T.
A useful example is T + Copy for a T that is not ordinarily Copy.
For consistency’s sake, let us say that the impl T and dyn T syntax works for all types T, not just negative T,
but for positive T they both mean just T itself.
We actually already have a candidate from the last page for the positive to negative direction:
FnOnce(Return<T>) -> noreturn
In general, we can understand the conversions from positive to negative types
as creating different calling conventions.
For consistency with existing syntax though, let us say that a positive type
that appears in a return type position is automatically converted to a negative type according
to the “ordinary” calling convention for the language, whatever that may be.
This is also when the return keyword becomes available for usage;
other return types will not be able to use that.
The use of Return<T> above probably raised the question “what about continuations?” Are they positive
or negative? Well, that gets a little complicated. You might expect that since we described
continuations being like functions, they would be negative. You might also recall
that I said that choices are the continuations of enums and coroutines are the continuations of structs,
which would seem to support that. I also said that this works in the opposite direction, which would seem to require that
continuations are positive.
Well, the truth is that we really need Return<T> specifically to be a function argument above, so it has to be positive.
It may be more fair to say that Return<T> is a specific closure type of continuation. We also said that
Return<T> cannot itself be returned. For the general concept of a continuation, though,
theory suggests that it should reverse the polarity of what it is given, and that (FnOnce(T) -> noreturn) -> noreturn should
be equivalent to T. That is for a pure lambda calculus however. While it is certainly true that
we can extract a value of type T from this “double continuation,” when it comes to actual computation with effects,
the pure theory doesn’t quite hold as the double continuation is closer to a computation FnOnce() -> T, which I suppose without effects
would be equivalent to T but here isn’t. The trick is that FnOnce(T) -> noreturn is really dyn FnOnce(T) -> noreturn here,
not itself the type of continuations of T but rather the type of closures of continuations.
The closure is positive, so its continuation, which is not the true double continuation, is negative.
In fact, because we said that only positive types can be used as argument types, we can expect that
any continuation type that we can actually write as a function type FnOnce(T) -> noreturn must have a positive T
and thus itself be negative. More productive might be to explicitly define what the continuation type is.
trait Continue
{
type Cont;
fn resume(self : Self, cont : Cont) -> noreturn;
}
For positive types, Cont can just be FnOnce(Self) -> noreturn,
though there may be equivalent formulations that are more convenient.
Without the continuation caveat, our primitive type operators would be split evenly between positive and negative types.
Even with the caveat, though, all of our negative type operators can be expressed as the continuation of one of the positive type operators.
It is my suspicion that negative types in general arise as the continuations of positive types. If so, then it might make
sense to define a Negative trait as:
trait Negative where <Self as Continue>::Cont : Positive
{
fn from_return(ret : Return<Cont>) -> Self;
}
This allows us something similar to the return keyword for other return types.
Of course, without defining what it means for Cont to be Positive, this doesn’t mean much —
but that is a topic for another day.