ponylang / ponyc

Pony is an open-source, actor-model, capabilities-secure, high performance programming language
http://www.ponylang.io
BSD 2-Clause "Simplified" License
5.71k stars 415 forks source link

Tuple allowed for unconstrained type param, but not Any #any type param. #1767

Closed jemc closed 7 years ago

jemc commented 7 years ago

I'm finding that tuples are allowed as type args for type params with no constraints, but are not allowed for type params that are constrained on Any #any, or more useful constraints, like Any #share. For example:

primitive Foo[A]
primitive Bar[A: Any #any]
primitive Baz[A: Any #share]

actor Main
  new create(env: Env) =>
    Foo[(Bool, Bool)]
    Bar[(Bool, Bool)]
    Baz[(Bool, Bool)]
Error:
/home/jemc/1/code/gitx/ponyc/test.jemc/test.pony:9:8: type argument is outside its constraint
    Bar[(Bool, Bool)]
       ^
    Info:
    /home/jemc/1/code/gitx/ponyc/test.jemc/test.pony:9:14: argument: (Bool val, Bool val)
        Bar[(Bool, Bool)]
                 ^
    /home/jemc/1/code/gitx/ponyc/test.jemc/test.pony:3:15: constraint: Any #any
    primitive Bar[A: Any #any]
                  ^
    /home/jemc/1/code/gitx/ponyc/test.jemc/test.pony:9:14: (Bool val, Bool val) is not a subytpe of Any #any: the subtype is a tuple
        Bar[(Bool, Bool)]
                 ^
Error:
/home/jemc/1/code/gitx/ponyc/test.jemc/test.pony:10:8: type argument is outside its constraint
    Baz[(Bool, Bool)]
       ^
    Info:
    /home/jemc/1/code/gitx/ponyc/test.jemc/test.pony:10:14: argument: (Bool val, Bool val)
        Baz[(Bool, Bool)]
                 ^
    /home/jemc/1/code/gitx/ponyc/test.jemc/test.pony:4:15: constraint: Any #share
    primitive Baz[A: Any #share]
                  ^
    /home/jemc/1/code/gitx/ponyc/test.jemc/test.pony:10:14: (Bool val, Bool val) is not a subytpe of Any #share: the subtype is a tuple
        Baz[(Bool, Bool)]
jemc commented 7 years ago

The result is that I can create a list of (Bool, Bool), but not a persistent list of (Bool, Bool). This seems counterintuitive to me.

jemc commented 7 years ago

On the sync call, @sylvanc said that this is expected, given that Any is just an empty interface and not a true "top type" that includes tuples.

In other words, an unconstrained type parameter is not equivalent to a type parameter constrained on Any #any, because the former allows tuples and the latter does not.

There's currently no way to specify a reference capability for a type parameter that can include tuples, since tuples currently do not have a reference capability at all.

On the sync call, I proposed a system of inferring a reference capability for tuples based on the ref caps of the elements, such that the ref cap of the tuple would be one whose viewpoint-adaptation set included the set of ref caps of the elements.

plietar commented 7 years ago

This came up again in the context of #1931.

On this week's call we talked about an alternative, fairly simple, solution.

We can add a special case in the type checker to make tuple subtypes of empty interfaces, such as Any. It doesn't matter what capability the parent interface has, since Any is opaque anyway. (I've realised this may not be true, since we still need capability for stuff like safe-to-write and sendability ?)

With this, tuples can now satisfy the Any #any constraint. If we try to upcast a tuple to an Any then codegen has to box it, but according to @sylvanc this should "just work", since it already does this when we upcast a tuple to a union.

jemc commented 7 years ago

I think we do still need to consider the cap of the tuple elements to determine if the tuple is a subtype of a given empty interface, due to the cap of the empty interface.

One of the reasons for that is definitely sendability, as you suggested in your parenthetical, though there may also be other reasons. For example, consider the Promise type in the standard library promises package:

actor Promise[A: Any #share]
  be apply(value: A) =>
    // ...

If we didn't consider the cap of the tuple, this would allow for unsound cases, such as Promise[(String ref, String ref)], essentially allowing the sending of unsendable objects simply by wrapping them in a tuple.

I think the key as I mentioned in my previous comment is to consider the set of valid viewpoint-adapted caps for a given origin cap. Or in other words, to consider the tuple elements as viewpoint-adapted fields in an "object" with unknown cap, in order to determine what caps are possible for the unknown cap of the "object". Note that this doesn't require tuples to actually be objects in the runtime, but just to be treated like objects with fields for the purposes of determining what tuple cap(s) would be sound.

For example, the set of valid viewpoint-adapted caps for a val origin is {val, tag}, so a tuple may only be considered a subtype of Any val if all elements have a cap of either val or tag (or #share, but I was trying to avoid complicating the example with gen caps).

plietar commented 7 years ago

Because we never actually go through viewpoint adaptation, I think we can get away with saying (A k1, B k2) is a subtype of Any k3 only if both k1 and k2 are subcaps of k3. That should be simpler.

This way (String ref, String ref) is not allowed by Any #share, but it is allowed by Any #any. A pair containing a tag would only be a subtype of Any tag.

This is stricter than your proposal, but I believe simpler to implement