Adding some practical tests for intersection types in context of using them for 'refining' types

[radeusgd]

Pull Request Description

Important Notes

Checklist

Please ensure that the following checklist has been satisfied before submitting the PR:

• The documentation has been updated, if necessary.
• Screenshots/screencasts have been attached, if there are any visual changes. For interactive or animated visual changes, a screencast is preferred.
• All code follows the
  Scala,
  Java,
  TypeScript,
  and
  Rust
  style guides. In case you are using a language not listed above, follow the Rust style guide.
• Unit tests have been written where possible.
• If meaningful changes were made to logic or tests affecting Enso Cloud integration in the libraries,
  or the Snowflake database integration, a run of the Extra Tests has been scheduled.
  • If applicable, it is suggested to paste a link to a successful run of the Extra Tests.

[radeusgd]

This was supposed to be an example for the #12143 bug. But apparently this test is already passing?!

I'm really surprised. This was supposed to be a minimal repro of the example that @JaroslavTulach was working-around in commit 9bb73ae.

@JaroslavTulach any idea why you needed a workaround in the Column code but here it seems to work as expected?

I'm a bit anxious that the behaviour seems to be slightly random - in some contexts the intersection is retained and in some it is lost. That is concerning.

I'd be happy if we can fix that, and ideally before - find a repro that actually fails a similar test and add it to the suite.

[radeusgd]

After all I've found a repro: b8407da

[JaroslavTulach]

Many of these tests seem to be duplicates of existing ones. That in my opinion means:

• more tests is better than less
• it is easier to write a new test than read the existing code
• reviewing the code is hard and spotting a problem close to impossible
• if the tests work without changing the implementation
• then they are likely correct
• and more coverage is always good

Thanks for the tests and also thank you for bug reports found while writing them:

• Calling a method that returns 'itself' on a multi-value should not lose multi-value structure? #12143
• Let EnsoMultiValue.to_text delegate to first type to_text #11827
• multi_value.to doesn't work on second & further elements of intersection type #11935
• Structural pattern matching should still work with intersection types #12142

At least that the list of pending issues I am aware of.

[AdRiley]

Great set of tests for showing how all the different combinations of working with these work.

[JaroslavTulach]

• we will have to change this
• because Keep EnsoMultiValue as self when dispatching Any instance methods #12170 changes the way Any instance methods are dispatched
• in your PR a2.is_a B changes self to first value which type has is_a - e.g. A
• with Keep EnsoMultiValue as self when dispatching Any instance methods #12170 the self remains EnsoMultiValue
• and is_a checks dispatch as well as extra types ofEnsoMultiValue.

[radeusgd]

Hmm, I see.

The is_a case is a thing we've been chatting about with @AdRiley today.

After some doubts, I think we reached conclusions that seemingly the current behaviour of is_a made sense.

If I call x.is_a Integer it tells me that I can call all Integer methods on it (without any casting, it already is that value).

Are you telling me that this will no longer be the case? I can check x.is_a Integer but that does not tell me if I can call x.round on it? I'm not sure if this is a good step forward.

The dispatch change is of course correct, but perhaps is_a should rely on a different logic? It is a builtin anyway.

We were considering adding a x.could_be_a that checks the extra types. But IMHO the is_a should focus only on the dispatch types.

[JaroslavTulach]

Changed to 34b6a3d as part of #12170

[AdRiley]

Could x.is_a Integer return true AND you could call x.round on it, be a good solution?

[radeusgd]

Could x.is_a Integer return true AND you could call x.round on it, be a good solution?

I think I was arguing against that mostly because it makes most static analysis rather infeasible.

The problem is that if I hold a value of type x : T, all I know statically about it is that it has type T. If it can have a secondary type (x.is_a U == True) then I don't really know anything. I can no longer statically check that a method call x.foo on x fails because T does not have method foo - I cannot rule out that at runtime x will have a hidden type U that may have the method foo and a call would succeed.

So I think that was partially the idea behind the 'hidden' types requiring a cast to 'uncover' them - the cast is visible by static analysis and x:U assertion tells it "The user asserts that x also has type U, if the control flow has continued that means this assertion was correct - so from now on I can infer calls on x as if it had type U.

With all this being implicit and not visible in the code, the type inference is rather helpless.

Making type inference work is one of my goals as I think improving it will be beneficial to the UX of Enso library developers (and external contributors in the future). But of course if it is clashing with other goals, we can reconsider the solutions. Still I was hoping that we can find a solution that will allow us to have good intersection type behaviour without sacrificing type inference as a whole.

[radeusgd]

One of the ideas was to use x : T & Any as a kind of cast that asserts x is of type T but maybe something more too. Then indeed a value like that could x.is_a U and allow calling U methods on it, because x : T & Any tells us it can be anything.

I like this approach because while after x : T & Any much of type inference is not that capable, it is a 'local only' problem - elsewhere in the code where I have x : T I can still infer normally. Not to say that x : T & Any may have its downsides too (like users perhaps 'accidentally' cutting off some refined types by casting without the & Any suffix). I know @JaroslavTulach was not a fan of & Any approaches and had some reasons for that.