Unsound matches with unconstrainted type parameters of different caps. about rfcs HOT 14 OPEN

This is related to exhaustive match. When a match is exhaustive, the next_block will be NULL (as it is here). In those cases, we're never supposed to jump to the next_block (as we do here).

We need to step through this and figure out how to properly handle this case without jumping to the next_block (because there is no next_block).

from rfcs.

@jemc 's diagnosis is right. @Praetonus says we should set the next_block to a block with an unreachable block terminator, as that branch should never be taken.

from rfcs.

Sounds right to me 👍.

from rfcs.

Hm no, the unreachable solution doesn't seem correct. I'll investigate more.

from rfcs.

Since an equivalent code without generic types results in a compilation error, I think this match should either result in a compilation error or be considered non-exhaustive. I'm not sure which one is correct.

from rfcs.

@Praetonus - it's definitely an exhaustive match, so it probably needs to be a compilation error.

Note that the error message you get when removing the indirection of the type parameters/arguments is:

Error:
main.pony:10:7: this capture violates capabilities, because the match would need to differentiate by capability at runtime instead of matching on type alone
    | let a: I32 => a
      ^
    Info:
    main.pony:8:13: the match type allows for more than one possibility with the same type as pattern type, but different capabilities. match type: (I32 val | I ref)
      fun f(x: (I32 | I)): (I32 | I) =>
                ^
    main.pony:10:7: pattern type: I32 val
        | let a: I32 => a
          ^
Error:
main.pony:11:7: this capture violates capabilities, because the match would need to differentiate by capability at runtime instead of matching on type alone
    | let b: I => b
      ^
    Info:
    main.pony:8:13: the match type allows for more than one possibility with the same type as pattern type, but different capabilities. match type: (I32 val | I ref)
      fun f(x: (I32 | I)): (I32 | I) =>
                ^
    main.pony:11:7: pattern type: I ref
        | let b: I => b
          ^

Note that I here is effectively the same as Any - an empty interface that is a supertype of everything. So the main issue is that I32 <: I, but they are different caps (val/ref), which means that you're matching on capability at runtime, which isn't allowed. The error goes away if you change interface I to interface val I.

So, exhaustive match doesn't really have anything to do with that problem - it would be the same problem for a non-exhaustive match.

This is an interesting case, because the only way to make this match safe would be to prove that either A and B are disjoint types, or that they have the same cap. It's interesting, because I don't know of a way to express either one of those conditions with type parameter constraints. So we end up with a situation where this very useful snippet (matching object type at runtime, from one of two type parameters) is seemingly impossible to write, even though there are many reifications of it that should be allowable.

Perhaps what we need are some new possibilities for expressing constraints? I'm not really sure what that should look like.

from rfcs.

Sync consensus is that we want to remove crashing aspect of this (the bug) without disallowing valid code.

from rfcs.

This was discussed on the 2017-09-06 sync call.

It's important to mention that this wouldn't be a problem if capabilities were present at runtime, rather than being a zero-cost abstraction that falls away at compile time. @sylvanc brought up that if we could still make them trivially cheap at runtime, this could be a good option, though we'd have to weigh it carefully because the zero-cost-abstraction part of capabilities that we have right now is really nice.

In the absence of that, we have to come up with a solution that disallows the unsafe case, even if it may also disallow some safe cases.

Our possible solutions are constrained by two requirements that we agreed on:

• We want the compiler to issue a typechecking error for this unsafe case.
• We don't want the compiler to have to know the type arguments when typechecking the body of a type-parameterized method (as this would allow the possibility of creating generic types that compile for some type arguments, and don't compile for others, which would quickly our poor programmers into the fiery pits of compiler hell)

With these in mind, we agreed our best choice for action was to modify the is_matchtype function (or rather, the static functions that implement it), which currently allows an unconstrained type parameter to be considered to potentially match anything. There are two places where this happens (one for the left side, and one for the right side of a match):

https://github.com/ponylang/ponyc/blob/021e3d4bf00e38a1d7c31e82926b339ee5626f9c/src/libponyc/type/matchtype.c#L407-L414

https://github.com/ponylang/ponyc/blob/021e3d4bf00e38a1d7c31e82926b339ee5626f9c/src/libponyc/type/matchtype.c#L165-L172

After we explored a lot of options, the only feasible one we came up with was to change the compiler to assume that an unconstrained type param cannot be guaranteed to match any type, because we have no clue what the type argument is, and for any given type on the other side of the match, there are examples of type arguments that will be a match that "violates capabilities" in the way described in my previous comment. In other words, we should return MATCHTYPE_DENY instead of MATCHTYPE_ACCEPT.

I'm marking this as an "easy" task, since now that it has been fully discussed, the solution is quite simple.

from rfcs.

Marking as needs discussion because this change has implications for the collections/List implementation. Specifically, ListNode.apply fails to compile: https://github.com/ponylang/ponyc/blob/master/packages/collections/list_node.pony#L16

We should consider a possible special case for as expressions

from rfcs.

During the last sync meeting we found that the failure to compile ListNode.apply was actually an example of a bug in the current compiler.

from rfcs.

Right, and just to follow that up, it spurred me to add #105.

from rfcs.

Found another case where the compiler was allowing matching on capability only, due to an unconstrained type param: https://github.com/ponylang/ponyc/pull/2289/files#diff-35e468e76bf0c02622ffcf7465e7cf82L411

from rfcs.

I'm not sure the implementation solution described by @jemc above is correct, since it would forbid matching from a type parameter to the same type parameter (e.g. if the match type is a union containing the type parameter.)

I think a better solution would be to allow the match if the operand and pattern refer to the same type parameter with compatible caps, and to match on Any #any otherwise.

from rfcs.

@jemc wrote:

Note that I here is effectively the same as Any - an empty interface that is a supertype of everything.

That’s a problem with structural interfaces. With (nominally or structurally selected) type classes which in my opinion would be preferable to interfaces and traits, AFAICT you wouldn’t have this problem.

If I remember correctly, it was @keean who taught me that (in his opinion) Any shouldn’t even be in a statically type programming language. You may need top and bottom types for the type checker but no actual type created by the programmer should ever equate to Any. So if you need Any, then I think it indicates there’s likely some fundamental design flaw in the language?

This is an interesting case, because the only way to make this match safe would be to prove that either A and B are disjoint types, or that they have the same cap. It's interesting, because I don't know of a way to express either one of those conditions with type parameter constraints. So we end up with a situation where this very useful snippet (matching object type at runtime, from one of two type parameters) is seemingly impossible to write, even though there are many reifications of it that should be allowable.

Are y’all familiar with Stephen Dolan’s MLsub thesis? He points out that type systems that have unions and intersections and that don’t put the unions and intersections (all types) in the ground types have an unwieldy algebra that is very difficult if not impossible to prove sound. Perhaps §2.1.5 Distributivity and subtyping on pg. 21 is also applicable.

I’ll quote:

^{Despite the succinctness of this definition, these types have a remarkably complicated and unwieldy algebra. Pottier gave the following example illustrating the incompleteness of a particular subtyping algorithm…}

So if all types are in the ground types, then there’s a distributive lattice and I think the disjointness you need is guaranteed? I need to reread that MLsub paper to be sure about this.

If the above is correct about your design being fundamentally unsound, then more cases will be discovered as more Pony code is written. And special case “fixes” would proliferate. In that case, perhaps it would be wise to bite the bullet now and scrap current design for a design that would be sound? Especially if the replacement would provide superior functionality and expression for the programmer.

EDIT: I posted that at 3am my time. After thinking about this more, nominal subtyping (e.g. traits) also prevents the needed disjoint invariant of the types (e.g. A is an Animal and B is a Cat, so is A also a Cat?). Without disjoint invariant of types in the union and intersection types, I imagine the reasoning about the type system has corner cases. The plan I had been formulating for a type system would only have subtyping from the anonymous, structural union types and no nominal subtyping. And no structural interfaces. The type classes would replace everything you currently use classes, interfaces, and traits for. And I think I would opt for nominal instead of Haskell’s structural type classes.

Also anonymous, structural (i.e. not nominal) intersection types seem to cause problems in a type system. If there’s no traits nor interfaces, then I don’t think they’re needed (not accessible to the Pony programmer) except perhaps only in the type checker as the dual to anonymous, structural union types. @keean had demonstrated to me that intersections of first-class functions can cause unification to be undecidable. We see another example of unsoundness due to intersections in §2.6.4 Modelling Challenges of the recent paper by George Steed about improving Pony.

FYI: this post of mine might subsume the Subtyping exclusion RFC.

EDIT#2: some additional thoughts.

Note that to exclude the vacuous reasoning, I posit not only would need to exclude traits and interfaces (i.e. subtyping other than for anonymous, structural unions) from the programming language, but would also need to exclude anonymous, structural unions from type parametrised cases that can cause undecidable cases such as the example of this thread. I think that could be accomplished by only applying type class bound operations on anonymous, structural unions, which effectively removes any overlapping non-disjoint portions of any union of said unions because the type class instances are resolved at compile-time and can’t be overlapping.¹ Understanding my posited point may be aided by reading this.

¹ _{Haskell does have an optional extension for overlapping instances but presuming not enabling overlapping instances.}

from rfcs.