opened 11:29AM - 05 Nov 20 UTC
compiler
language design
typing
P2
### Motivation
Currently, polymorphism is fully parametric and erased in Moto… ko. Consequently, values of variable type cannot be used in any of the operations that requires intensional polymorphism:
- message sends
- async (may be unnecessary)
- serialisation & deserialisation
- structural comparison
- structural hashing
- polymorphic printing
It is neither possible to provide such operations as generic library functions, nor can user code abstract over types that involve such operations. Instead, any relevant operation and abstraction can only be made accessible by adding new primitive syntax in the language. That clearly is an abstraction failure.
### Proposal
This proposal extends the language with _shared type variables_. On the surface, the proposal is simple:
* Allow the annotation `shared` on type bindings:
```
func foo<shared T>(x : T) : Bool { x == x };
```
* Type variables thus declared are of _shared kind_ (a subkind of all types), and qualify as shared types.
* They can only be instantiated by shared types.
### Implementation
The gross of this proposal is under the surface. The compiler lowers shared generics by introducing implicit runtime type arguments to respective functions. For example, the above is lowered to
```
func foo<T>(_T : Rtt<T>, x : T) : Bool { prim_equal<T>(_T, x, x); }
```
where `Rtt<T>` is a runtime representation of the type `T`. This representation is passed to all intensional operators. The lowering also inserts the respective arguments at call sites. In some cases, that involves constructing witness RTT values dynamically, for example:
```
func bar<shared T>(x : T) : Bool { foo<[T]>([x]); }
```
This lowers to
```
func bar<T>(_T : Rtt<T>, x : T) : Bool { foo<[T]>(_rtt_array(_T), [x]); }
```
where `_rtt_array` is an internal intro form or function to construct the RTT for an array.
These techniques are of course well-known from other evidence-passing translations.
Does anybody know the status of this? We’d love to have it for our game, would just make the endpoints so much simpler (we’ve got a huge number of types that get updated via the API). Right now the front end just talks directly to the database using variants and it’s a bit insecure and hard to validate.
3 Likes
cc @claudio as I’m guessing he’s the one that took over this.
Unfortunately, I’ve got no real progress to report here.
1 Like