Add support for type dynamic

[rossberg]

To represent generic data, as discussed on #245 ("Idea 1") on various occasions.

A value of type dynamic is serialised as a nested self-contained Candid blob.

[crusso]

That looks plausible but only deals with a single value, right? For the use case we were discussing, the arguments and return of a generic call forwarding mechanism, wouldn't the dyn value need to pack a sequence of values? The forwarding mechanism needs to work for any arg/return arity.

[crusso]

@nomeata, interested in your view on this (but can't add you as reviewer).

[nomeata]

Yes, the second class nature of the argument tuple type may cause issues here.

[matthewhammer]

Not sure where to discuss this, but I find that the content in the issue has been helpful to remind myself of the past discussion, so I added a comment there:
#245 (comment)

[rossberg]

As mentioned elsewhere, I think I'm fine if this works just for a fixed arity for now. The wallet example could add methods for different return arities if that's needed. Happy to defer thinking about tuple conversions later.

I think the bigger problem with the wallet example actually is a different one: the callee that somebody wants to forward to presumably is not expecting a dynamic value. So, for this to work, we'll need to support implicit conversions in and out of type dynamic, very much like with gradual typing. That requires extending our subtype relation in a way that makes dynamic both a sub- and super-type of every other type. Doable, I suppose, but I'm not entirely sure about the consequences. @nomeata, do you have any intuition on that? Unfortunately, that seems unavoidable for making dynamic generally useful as a poor men's generic type.

[rossberg]

[Deleted, wrong PR. :)]

[nomeata]

From an implementation point of view, I think it wouldn't be too much of an issue - just recurse into the nested encoding. Although, what do we do on failure - trap? Let the application handle that? Is dyn only a subtype of opt t to express failure?

I'd be inclined to let these dyn values be complete encoded candid sequences, with type table, for the same reasons as in the closure discussion.

[matthewhammer]

Let the application handle that?

That would be nice. Is that possible?

[nomeata]

Not sure. If we have dyn <: opt t only, then a decoder could sensibly fail if the types don't match. But that of course limits where you can send the dyn value, so maybe missing the point.

[matthewhammer]

the callee that somebody wants to forward to presumably is not expecting a dynamic value.

Let's discuss that, perhaps?

To me, it seems reasonable to treat these dyn values as something that require explicit language primitives, or even a library, to intro and elim in Motoko (or Rust, or whatever).

Later, when it becomes clear how to make everything that developers and we understand explicitly into something more implicit, I would embrace that too.

So, for this to work, we'll need to support implicit conversions in and out of type dynamic, very much like with gradual typing

I don't see why this is necessary -- the goal is generic data, and that could reasonably mean explicit generic data, so long as there are (explicit) conversions in Motoko and the dyn type is recognized by Candid.

[rossberg]

@matthewhammer:

To me, it seems reasonable to treat these dyn values as something that require explicit language primitives, or even a library, to intro and elim in Motoko (or Rust, or whatever).

To be clear, I'm not saying we should not have an explicit representation of type dyn in Motoko as well. But that's not enough, to emulate "generic composition", you also need interconvertibility with other types. Consider the wallet use case of a generic forwarding function (which is really just a nullary "apply" function):

forward : (closure () -> dynamic) -> dynamic

This is supposed to be generic, i.e., work with any function, including all those whose result has not been typed as dynamic a priori, for example, one whose (closure) type is () -> (int). It really takes the equivalent of gradual typing to make that work, I think. The only alternative would be proper generics, AFAICS.

@nomeata:

From an implementation point of view, I think it wouldn't be too much of an issue - just recurse into the nested encoding.

I'd hope so, but don't know how well-prepared the decoder is for reentrancy.

Although, what do we do on failure - trap? Let the application handle that? Is dyn only a subtype of opt t to express failure?

If we allow both a Motoko-side dyn type but also make it gradually compatible with specific types, then it's up to the user to make their pick: with dyn, they can handle it themselves (and potentially abuse this for reflection), with a concrete type it would just trap implicitly.

I'd be inclined to let these dyn values be complete encoded candid sequences, with type table, for the same reasons as in the closure discussion.

Isn't that what they are already? (Note how the encoding uses the B function.) Or do you mean something else?

[nomeata]

Isn't that what they are already?

Yes, my bad, I had pages out the concrete proposed change.

[matthewhammer]

While gradual-typing-like features seem inevitable in the limit, I wonder if something much simpler and more explicit could still work in the interim?

My thinking was that the MVP would merely introduce dynamic as a special kind of Blob that is always encoding an argument sequence in Candid, and not arbitrary binary data. There'd be no special lubrication to coerce into or from this type. Rather, there'd initially just be a manual API for consumers/producers of a dynamic, in each language.

Hence, a closure of type closure () -> (int) would not be typable as closure () -> dynamic in Candid, since there would be no way to relate dynamic and (int).

Rather, that coercion (which could fail) happens when some response-handling Motoko/Rust/Wasm code eventually tries to unpack and use the dynamic as an (int), explicitly.

I realize that my more limited conception of this feature is not as powerful as the one that @rossberg envisions.

But, I'm not in favor of having silent, implicit traps when these coercions fail, at least not in the MVP. Wallets and use cases like them are not that common, and we do not need to optimize the code's concision for them yet. IMO this implicit feature does not offer enough "bang" to justify all of the many, many footguns that could be fashioned from it from its misuse.

@rossberg

If we allow both a Motoko-side dyn type but also make it gradually compatible with specific types, then it's up to the user to make their pick: with dyn, they can handle it themselves (and potentially abuse this for reflection), with a concrete type it would just trap implicitly.

Ah, I see --- that's a more liberal design that I first imagined. I was only thinking about the former choice, and not considering that we support the latter initially.

Is there a way to avoid offering the second choice initially? You seem to indicate no, but I still wonder:

you also need interconvertibility with other types. Consider the wallet use case of a generic forwarding function (which is really just a nullary "apply" function): forward : (closure () -> dynamic) -> dynamic. This is supposed to be generic, i.e., work with any function. It really takes the equivalent of gradual typing to make that work, I think. The only alternative would be proper generics, AFAICS.

I think there's room for a "less generic" interpretation, where all of the types match on the nose and there is no implicit conversion -- in that realm, dynamic has no special status in the encoder or decoding steps. Instead, I had assumed that the caller must prepare the argument (or have the argument from somewhere) as a dynamic, using the explicit API for doing so, and also accept the response as a dynamic. All of the encoding and encoding would be explicit, at the application/library level.

[rossberg]

My thinking was that the MVP would merely introduce dynamic as a special kind of Blob that is always encoding an argument sequence in Candid

Hm, an argument sequence makes no sense for most use cases. Typically, you need individual values, e.g. the generic value of a key/value store.

I think there's room for a "less generic" interpretation, where all of the types match on the nose and there is no implicit conversion

But how would that address the wallet use case? The wallet doesn't get to choose whether some other pre-existing interface uses return type dynamic. And if it actually did, it would ultimately mean that everybody would have to use dynamic for every method, which obviously is highly undesirable.

[matthewhammer]

Typically, you need individual values, e.g. the generic value of a key/value store.

Some explicit primitives, e.g., in a Motoko library, would introduce and elim the argument sequences (much like we envision for converting to/from Blob), and they'd have dynamic type errors when eliminating to the "wrong type(s)".

...And if it actually did, it would ultimately mean that everybody would have to use dynamic for every method, which obviously is highly undesirable.

Well, no, only the methods that are to be used in a higher-order and generic way need to use this type. Presumably, not every API call needs to be used that way, and the ones that do can be re-exposed with the requisite dynamic type, once wallets (or whatever else) start to support calling them that way.

Do I think this is the "right design"? No, of course not. I'm merely pushing back on the idea that we must have implicit type coercions to have an MVP that has some value. Arguably, this idea lacks sufficient value to execute (for the reasons that you are giving, which I find compelling), but to me, that's a separate question. ;)

[matthewhammer]

the word "opcode" got dropped during the edits?

[rossberg]

Oops, fixed.

[rossberg]

Well, no, only the methods that are to be used in a higher-order and generic way need to use this type.

Hm, I believe it's a crucial point for an abstraction like the wallet's call forwarding that it's applicable to every method.

Without this ability, it's not a solution to that problem, and in addition, would create bad incentives (like using dynamic everywhere where you shouldn't).

[rossberg]

Okay, I extended the proposal with proper support for gradual typing.

[rossberg]

I just noticed that the sketched http_request interface also works around the lack of a generic type, as it has this:

// There is no generics in Candid, so we use a `t`, which would be a generic
// once Candid has support for it, to signify this value can be any valid
// Candid value (as the Spec) and will be passed through by the HTTP Server
// as is.
// In a canister, this could be a properly typed field. It is only untyped
// here as reference for this specification.
//
// Any HTTP Server which implements this protocol MUST pass this field
// without any modifications (e.g. it CANNOT drop fields from a record).
type Token = T;

It then uses Token inside parameter and result type.

[nomeata]

That's a bit too sneaky; if we go this route we should explicitly define this function to be partial (it was total before), with suitable notation. Also the interaction with opt stuff needs to be clear, especially if we go back to making that more dynamic again.

How does this affect our formal guarantees? They can only hold when no dynamic is in use, right?

[rossberg]

Fair enough. It's probably necessary to distinguish gradual conversion from subtyping anyway, because transitively, subtyping collapses with the above rules, i.e., everything becomes a subtype of everything.

[rossberg]

@nomeata, you are right, this was taking at least one shortcut too many. I pushed a change that should properly separate graduality from subtyping and coercions. Subtyping now only allows t <: dynamic, but not the other way round. Graduality itself is handled in de/serialisation itself. Let me know what you think.