dfinity / motoko

Simple high-level language for writing Internet Computer canisters
Apache License 2.0
500 stars 98 forks source link

actor t <: principal #2264

Open nomeata opened 3 years ago

nomeata commented 3 years ago

Users currently have to write Principal.fromActor(Foo) to get the principal of an actor (including their own self). This is a bit silly, since an actor reference inherently is represented by a principal (in a way, it’s a principal with some phantom type information attached).

So we could add actor t <: principal to our subtyping rules.

Benefit: No need for Principal.fromActor(Foo).

Implication: Representation has to be the same for actor … and principal, but that’s true now, and I don’t see us changing that soon.

Interaction with Candid: Darn, here is an interaction. As per https://github.com/dfinity/motoko/blob/master/design/IDL-Motoko.md we need

∀ t1 t2 : dom(e), t1 <: t2 ⟹ e(t1) <: e(t2)

i.e. Motoko subtyping must be contained in IDL subtyping. So we can only add this to Motoko’s subtyping if we also add it to Candid’s subtyping, which does not have service <: principal … yet.

nomeata commented 3 years ago

This is really tiny:

~/dfinity/motoko/src $ git diff
diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml
index c72a1e7d7..425413a74 100644
--- a/src/mo_types/type.ml
+++ b/src/mo_types/type.ml
@@ -739,6 +739,8 @@ let rec rel_typ rel eq t1 t2 =
   | Obj (s1, tfs1), Obj (s2, tfs2) ->
     s1 = s2 &&
     rel_fields rel eq tfs1 tfs2
+  | Obj (Actor, _), Prim Principal when rel != eq ->
+    true
   | Array t1', Array t2' ->
     rel_typ rel eq t1' t2'
   | Opt t1', Opt t2' ->
diff --git a/src/prelude/prelude.ml b/src/prelude/prelude.ml
index aebbbaf46..42f8473d2 100644
--- a/src/prelude/prelude.ml
+++ b/src/prelude/prelude.ml
@@ -631,7 +631,8 @@ func time() : Nat64 = (prim "time" : () -> Nat64) ();

 func blobOfPrincipal(id : Principal) : Blob = (prim "cast" : Principal -> Blob) id;

-func principalOfActor(act : actor {}) : Principal = (prim "cast" : (actor {}) -> Principal) act;
+// NB: Obsoleted by subtyping, remove when no longer used in base
+func principalOfActor(act : actor {}) : Principal = act;

 // Untyped dynamic actor creation from blobs
 let createActor : (wasm : Blob, argument : Blob) -> async Principal = @create_actor_helper;
diff --git a/test/run/show-principal.mo b/test/run/show-principal.mo
index 65021d90a..86299cdf5 100644
--- a/test/run/show-principal.mo
+++ b/test/run/show-principal.mo
@@ -1,3 +1,3 @@
 import Prim "mo:prim";
-Prim.debugPrint(debug_show (Prim.principalOfActor(actor "bfozs-kwa73-7nadi")));
-Prim.debugPrint(debug_show (Prim.principalOfActor(actor "aaaaa-aa")));
+Prim.debugPrint(debug_show ((actor "bfozs-kwa73-7nadi" : actor {}) : Principal));
+Prim.debugPrint(debug_show ((actor "aaaaa-aa" : actor {}) : Principal));

so tiny that I finished it before remember that we cannot do this without changing the Candid specification as well…

ggreif commented 3 years ago

This is most excellent, I am doing

        let self = Prim.principalOfActor Self;

all the time!

I love the prospect of not doing this again for defined/imported actors.

rossberg commented 3 years ago

What would break if Motoko had this but Candid didn't?

nomeata commented 3 years ago

It’s the same as always: We’d have

actor { foo : Principal -> async () } <: actor { foo : actor {} -> async () }

but if we import a service reference at the subtype, and use it at the supertype, then we’d encode the message with actor {}, and the other service will fail to decode the message.

Nothing special about Principal here, of course, we need

∀ t1 t2 : dom(e), t1 <: t2 ⟹ e(t1) <: e(t2)

for all types (<: on the left is Motoko, <: on the right is Candid).

nomeata commented 3 years ago

This is still listed on https://github.com/dfinity/motoko/issues/2303. Is it worth adding service {} <: principal to Candid? Or shall we just close this as “cantfix”?

rossberg commented 3 years ago

Hm, how natural would this subtyping be on the Candid level? Is it too odd? Would other languages be able to cope with it in a reasonable manner?

nomeata commented 3 years ago

We already have plenty of odd subtyping Candid, it doesn't harm other languages at all (it only really shows up in the decoder). So it's doable, and I guess it makes sense semantically?

chenyan-dfinity commented 3 years ago

I think it make sense for Candid. People are already confused about service "aaaaa-aa" vs principal "aaaaa-aa" in the textual representation.

rossberg commented 3 years ago

I suppose we can do it then.

crusso commented 1 year ago

@nomeata @ggreif and I were discussing this again. This would solve the problem that you can't obtain the principal of 'this' in an actor's constructor, which is another common issue and inconvenience (e.g. https://forum.dfinity.org/t/heartbeat-improvements-timers-community-consideration/14201/134)

However, that could also be solved by treating this as defined, not undefined, to avoid the undefinedness error. Do you recall why we don't treat this as defined within the initializer? It seems like an unnecessary restriction to me, since you can't do anything with the principal anyway (message sends are verboten from the initializer.)

nomeata commented 1 year ago

I don't recall the reason, unfortunately. I thought it was something with await, but if that's verboten, things are fine maybe?

crusso commented 1 year ago

I don't recall the reason, unfortunately. I thought it was something with await, but if that's verboten, things are fine maybe?

I think its clear we don't want to allow it for non-actors - otherwise an object could read its (uninitialized) fields within a constructor, which is bad. But I think actor's might be ok, since sends are verboten anyway.