Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

actor t <: principal #2264

Open
Tracked by #3921
nomeata opened this issue Jan 18, 2021 · 12 comments
Open
Tracked by #3921

actor t <: principal #2264

nomeata opened this issue Jan 18, 2021 · 12 comments
Labels
idl Candid or serialisation language design Requires design work P1 high priority, resolve before the next milestone typing Involves the type system

Comments

@nomeata
Copy link
Collaborator

nomeata commented Jan 18, 2021

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.

@rossberg rossberg added idl Candid or serialisation language design Requires design work P1 high priority, resolve before the next milestone typing Involves the type system labels Feb 2, 2021
@rossberg rossberg mentioned this issue Feb 2, 2021
28 tasks
@nomeata
Copy link
Collaborator Author

nomeata commented Feb 8, 2021

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
Copy link
Contributor

ggreif commented Feb 8, 2021

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
Copy link
Contributor

rossberg commented Feb 8, 2021

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

@nomeata
Copy link
Collaborator Author

nomeata commented Feb 8, 2021

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
Copy link
Collaborator Author

nomeata commented Feb 16, 2021

This is still listed on #2303. Is it worth adding service {} <: principal to Candid? Or shall we just close this as “cantfix”?

@rossberg
Copy link
Contributor

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
Copy link
Collaborator Author

nomeata commented Feb 23, 2021

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
Copy link
Contributor

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

@rossberg
Copy link
Contributor

I suppose we can do it then.

@crusso
Copy link
Contributor

crusso commented Jan 23, 2023

@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
Copy link
Collaborator Author

nomeata commented Jan 23, 2023

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

@crusso
Copy link
Contributor

crusso commented Jan 23, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
idl Candid or serialisation language design Requires design work P1 high priority, resolve before the next milestone typing Involves the type system
Projects
None yet
Development

No branches or pull requests

5 participants