Problem with matching generic types

[cararemixed]

After #2499 was merged, I started seeing some odd errors. I still don't understand the ins and outs of generics in Pony very but I've boiled down an example snippet of something I'm not sure how to express after this change was put in place:

actor Main

  new create(env: Env) =>
    let bx = SimpleBox[U32]
    try
      bx() = 42
      env.out.print("Answer is " + bx()?.string())
    end


class SimpleBox[A: Any #read]
  """Contrived but it's sufficient to reproduce the issue."""
  var _data: (A | None)

  new create() =>
    _data = None

  fun apply(): A ? =>
    match _data
    | let a: A => a
    else
      error
    end

  fun ref update(value: A) =>
       _data = value

This should display "Answer is 42" and does with the 0.21.3 release. On master I get an error. I'm wondering if a bit too much code was removed or if there is a new preferred idiom for this case.

[Praetonus]

This is indeed a bug. Thanks for the report.

[SeanTAllen]

FYI... I don't think we should do a release until this is fixed. Release is currently blocked at my request for Wallaroo Labs so I don't think it matters but I just wanted to make the point we shouldn't have a release with this regression in it.

[Praetonus]

So after thinking about this a bit more, I do think that the current implementation of pattern matching is correct. If the example code here was allowed by the compiler, it could exhibit a surprising behaviour for some reifications. This is related to #2182.

For example, if SimpleBox is reified with Any ref, the type of _data is (Any ref | None val). None provides Any, which means that matching from (Any ref | None val) to Any ref violates capability security since we can't differentiate between a None val and a None ref at runtime (there are some additional subtleties since primitives can't be ref but the actual problem here doesn't change.)

In previous versions where this kind of pattern matching was allowed, the problematic reifications would silently never match. This was done by checking the reified match type during code generation, and not emitting any code for the reified pattern if it couldn't match. This means that for a SimpleBox storing ref objects, apply will always error regardless of what has been stored in _data.

I think rejecting this kind of code at compile time is the correct thing to do, since this has a lot of potential for programmer confusion.

The correct solution would be a functionality resolving ponylang/rfcs#105. A potential candidate would be a notation to exclude a set of types from another set of types (i.e. a relative complement operator.) For example (Any \ None) would be "everything providing Any, except None".

[cararemixed]

That makes sense. Thanks for the explanation, I had not settled that Any would include None.

In my mind, the A was concrete type at the time of the check so it'd know that it wasn't None as part of the reification (or if it was, it could error). But if the check happens before the reification, there's no way to safely decide at compile time. Should this check be done without reification of the specific instantiation?

This seems to be quite easy to get into with any sum type (with or without mixed reference capabilities). Would it be worth having some warning or error when a union is constructed from an unconstrained Any?

As far as more code samples, I've seen these recently (Array rather than a box) but it has the same parameterized pattern matching issue it seems. Finding the right idiom here would be very helpful.

I've also found another slightly more real use of this kind of code: https://github.com/jtfmumm/acolyte/blob/master/src/datast/matrix.pony#L6 and https://github.com/jtfmumm/acolyte/blob/master/src/datast/matrix.pony#L34. Another case in wallaroo: https://github.com/WallarooLabs/wallaroo/blob/master/lib/wallaroo_labs/queue/none_fixed_queue.pony (I haven't tried to compile wallaroo with the master branch of pony because of other blocking issues).

[jemc]

But if the check happens before the reification, there's no way to safely decide at compile time. Should this check be done without reification of the specific instantiation?

Part of the goal of compiling a type that has type parameters is to prove that it will have correctness for any possible reification - this is what type parameter constraints are all about - setting the domain of possible reifications, so that the type system can check that all bounds of that domain are sound.

Taking this approach means that you can create a library that compiles for you in your tests, and it will be guaranteed not to have compiler errors for anyone else who tries to use that library. If we changed this approach, and only did type system checks for the specific reification used, then you wouldn't be able to have this guarantee - you could write code that compiles for you, but will break when someone reifies it with a type argument that you didn't expect.

[cararemixed]

My knowledge around type theory is pretty shallow and mostly from experience with the ML family of languages. What follows is how I'm trying to reason about this case but I'm likely missing something so please to tell me where I might be missing something.

I'm not in disagreement here. For this this specific case of a union, explicitly specifying disjointness of a parameter is certainly a reasonable fix. However, the impact on the match itself seems to not seemed to be addressed well.

In the case of the match, is there an importance in treating ((A \ None) | None) | None different in a match from (A \ None) | None? The question of narrowing the cases that A represents in a match is different from saying it can't match without some sort of RTTI. I'm not sure if this introduces unsoundness in Pony but I'd guess that it'd mostly rely on the property that unions are always treated disjointly.

If this were an ML style variant, it'd be a bit different since we'd be forced to give each case a nominal identifier like:

type 'a thing = 
  | ExplicitThing of 'a
  | NotAThing

Here, we always end up tagging each case. Looking at the polymorphic variant behavior in Ocaml, we see they opt for merging the bounds because disjointness is guaranteed between each polymorphic variant:

type 'a thing =
  [ `ExplicitThing of 'a | `NotAThing ]

let not_a_thing : [`NotAThing] = `NotAThing
let box_it (a : [`NotAThing | 'a thing]) : [`ExplicitThing of 'a | `NotAThing] = a

The type signature of box_it shows that we merge the two cases of `NotAThing as equal. This is where I'm drawing my intuition from and I know Pony is most definitely not OCaml. In this case, we're mixing primitives (very much like polymorphic variants) with references (more like traditionally boxed values in the first example). The trade-off we make might imply something like: "All pritmitive cases in a union are treated disjointly. Any type parameter which can't be proven to be disjoint when matched against will be assumed to be disjoint and only actually allow matches to the disjoint cases."

Edit: Fixing my example code after rereading it.

[Praetonus]

RFC #121 has been opened to handle this.

@strmpnk Your ML analogy sounds a lot like tagged union, which are an alternative that have been discussed on the RFC ticket, and during last week's sync meeting (you can find the recording on the dev mailing list). That discussion might be of interest to you.