Intersection types & type checks

[JaroslavTulach]

Pull Request Description

Implementation of type checks for intersection types. The idea is to split the list of types[] in EnsoMultiValue into two parts:

• first methodDispatchTypes represent the types the value "has been cast to"
• the rest of the types represent the types the value "can be cast to"

By performing this separation we address the #10882 requirements. After a type check only methods available on the methodDispatchTypes can be invoked. However the value can still be cast to all the possible types.

Checklist

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

• The documentation has been updated: read intersection types docs here!
• All code follows the
  Scala,
  Java,
  style guides.
• Unit tests have been written where possible.
• Test multi values in a Dictionary - e.g. == and hash consistency - test written in 91987ca and bug EnsoMultiValue == isn't transitive #11845 reported

Followup Issues

The goal of this PR is to get dispatch/cast logic right. There is a lot of additional work to do:

• make it fast - Benchmark EnsoMultiValue and speed it up #11846
• Let EnsoMultiValue.to_text delegate to first type to_text #11827
• Pattern matching a EnsoMultiValue ignores 2nd & co. types #11828
• EnsoMultiValue == isn't transitive #11845

[Akirathan]

Idea for increasing test coverage of EnsoMultiValue: Manually create some Truffle nodes and explicitly call them. Inspiration from EqualsTest and HashCodeTest.

[GregoryTravis]

Approve libs change.

[JaroslavTulach]

Idea for increasing test coverage of EnsoMultiValue: Manually create some Truffle nodes and explicitly call them. Inspiration from EqualsTest and HashCodeTest.

• some EnsoMultiValue tests have just been created as part of Giving TypeOfNode richer query API #11618
• I have a much better feeling with such tests!

[JaroslavTulach]

Pattern matching on type on first value of a EnsoMultiValue works, but we want to match on other values as well:

diff --git test/Base_Tests/src/Semantic/Multi_Value_Convert_Spec.enso test/Base_Tests/src/Semantic/Multi_Value_Convert_Spec.enso
index ca768daaa0..2e54642532 100644
--- test/Base_Tests/src/Semantic/Multi_Value_Convert_Spec.enso
+++ test/Base_Tests/src/Semantic/Multi_Value_Convert_Spec.enso
@@ -84,6 +84,41 @@ add_specs suite_builder =
                 _ -> "what?"
             c1 . should_equal "c"
 
+        group_builder.specify "case of second" <|
+            abc = 3.14 : A&B&C
+            c1 = case abc of
+                b:B -> b.b
+                a:A -> a.a
+                c:C -> c.c
+                _ -> "what?"
+            c1 . should_equal "b"
+
+        group_builder.specify "case of third" <|
+            abc = 3.14 : A&B&C
+            c1 = case abc of
+                c:C -> c.c
+                b:B -> b.b
+                a:A -> a.a
+                _ -> "what?"
+            c1 . should_equal "c"
+
+        group_builder.specify "case of second from extra types" <|
+            abc = 3.14 : A&B&C
+            c1 = case abc:A of
+                b:B -> b.b
+                a:A -> a.a
+                c:C -> c.c
+                _ -> "what?"
+            c1 . should_equal "b"
+
+        group_builder.specify "case of third  from extra types" <|
+            abc = 3.14 : A&B&C
+            c1 = case abc:A of
+                c:C -> c.c
+                b:B -> b.b
+                a:A -> a.a
+                _ -> "what?"
+            c1 . should_equal "c"
 
 main filter=Nothing =
     suite = Test.build suite_builder->

[JaroslavTulach]

• Pattern matching a EnsoMultiValue ignores 2nd & co. types #11828

[radeusgd]

These tests look great

[radeusgd]

I've created a PR-to-your-PR #11838 that suggests some changes to the documentation. Please let me know what you think of them and if you are happy, you can just merge that PR into yours.

[radeusgd]

I'm confused about this test.

Isn't a type-asserting expression (uv:A) supposed to work as the 'explicit' instanceof-like conversion? Then it probably should be able to extract the A type hidden from the multi-value abc upon the uv = abc : U&V conversion, no?

If that was a method call, e.g.:

f (a:A) = ...
...
f uv

then I agree this should yield a type error.

But here it is a 'type-asserting expression' which I thought according to our spec was supposed to act like instanceof and uncover any 'hidden' part of the type. What am I missing here?

[radeusgd]

This test is great and it tests both method dispatch and type asserting expressions (although as noted above I'm not sure if the behaviour is correct?).

But the test seems to be lacking any argument-type check tests. Can we add these? These would be similar to the expressions uv:A but instead we'd pass the uv value to a function with checked argument type:

f_a a:A = a.a

And see that if the type is 'hidden' then it cannot be uncovered in the argument type check.

[JaroslavTulach]

Argument checking test is here https://github.com/enso-org/enso/pull/11600/files#diff-fb0aa503a2a28b6e78764cf7ae6642ffdc2bfb775fa08e0ee7ce73b44fde4d45R97

[JaroslavTulach]

it is a 'type-asserting expression' which I thought according to our spec was supposed to act like instanceof and uncover any 'hidden' part of the type

This test has been integrated in 1167b52 together with documentation for "converting type check". The test checks the behavior exactly as documented.

Remember, we are implementing variant 1. E.g. when we have to built new intersection type by using conversions, then we start from scratch. As such uv has no traces of abc.

[radeusgd]

So we are in disagreement over what variant 1 constitutes. I know you don't like my pseudocode but I used it as it allowed me to precisely describe what I mean, perhaps I could try using normal words but I'm sure I wouldn't be as precise.

In my variant 1 the explicit cast removes the 'unused' types from the visible type (Set<T> resultTypes = Set.empty();) but it actually still keeps them in the hidden part (List<T> remainingTypes = allInputTypes.removeAll(resultTypes); return RuntimeType(resultTypes.toList(), remainingTypes);. But your solution instead removes them altogether, 'clearing' the hidden part.

Are you sure that is right? How does that relate to the subclass metaphor? If a conversion is used, does that mean that we are losing the 'subclass' altogether and getting a new fresh class?

If we did uv = abc:(A&B&C&U&V) we'd have kept all the types, right?

[radeusgd]

I've added some more scenarios that test my understanding of multi value types with conversions and casts. All seems good.

types-tests-extended.zip

We could consider turning them into tests to serve as illustration + ensure the behaviour stay as we expect it to be.

[radeusgd]

These experiments led me to one concern - the meaning of : is heavily overloaded and I'm worried that it may be a source of confusion for developers and possibly end-users.

I think we tried to do a great job in leveraging the various meanings (argument type check, cast, conversion), but I'm worried if there isn't too much going on at the same time.

Especially in expressions, the type ascription x:T may mean different things - it can either be an instanceof-like 'assertion' that checks if the value of x has type T OR it can actually be a conversion that invokes some T.from (x:?) function. While similar, we have noted above that there are non-trivial differences in behaviour of these two.

IF the x:T was a cast, then the x will keep any additional multi value types it had before (although they become "hidden"). However, if it turned out to need to be a conversion, then any additional multi value types are removed.

Functionally, this seems a good choice - a conversion is applying a new function and its result has not that much to do with the input, so it makes sense to not inherit the inputs unless explicitly determined in the expression. And it prevents the powerset problem as @JaroslavTulach noted above.

However, that means that both the user or the type checker - when they see the type ascription x:T they cannot really tell if the additional multi value types (if there were any) will be kept on x (only hidden) or will be completely removed. That is something that is only decided at runtime because it depends on the actual precise type of x.

While I don't find any critical problems this could cause for type inference - there we are interested mostly in argument type checks and method dispatch - both of which rely on the visible part of the type that is fortunately the same both in a cast and conversion scenario. So we should be okay.

But conceptually - it doesn't feel right that by just looking at the code I cannot really tell if the additional types are kept or removed.

Thus I'm wondering if maybe we should distinguish a cast from a conversion syntactically and make them into two separate constructs. If we want to do this we probably should sooner rather than later.

BUT maybe we are alright after all - because we do have separate constructs:

• we have T.from for 'just conversion'
• and we have case of that allows us to do the instanceof-like check.

So I guess the problem is only with the : ascription used in expressions. Perhaps we should only use it when we have to - when we want to specify multiple types at once - like in x:(A&B). And in case we actually want to perform an instanceof-like check - we should probably prefer the case of statement as it will not trigger conversions accidentally and will ensure that any additional multi value types are always kept.

So to sum up all this experimentation - I think the current state is OK. The : is a bit overloaded so maybe we should prefer to use case of for instanceof checks (it even sounds similar 😀) and be careful when using x:T as expression ascriptions.

[JaroslavTulach]

what I meant by the so called 'variant 1' after all

I am glad you are OK with current behavior, I am fine with it as well.

turning them into tests to serve as illustration + ensure the behaviour stay as we expect

Sure, go on!

Right now I am aware only of following differences from expected behavior:

• Let EnsoMultiValue.to_text delegate to first type to_text #11827 - invoking methods defined on Any may change

Otherwise, whatever behavior works right now is (according to our knowledge) the desired behavior and deserves to be recorded as a test.

[JaroslavTulach]

the problem is only with the : ascription used in expressions. Perhaps we should only use it when we have to - when we want to specify multiple types at once - like in x:(A&B). And in case we actually want to perform an instanceof-like check - we should probably prefer the case of statement as it will not trigger conversions accidentally and will ensure that any additional multi value types are always kept.

In this case we are facing an end (GUI) user problem: We want the IDE to generate human readable code when invoking methods on hidden types of a multi value. So far the IDE can use mv:Hidden_Type . method. Should we allow unrevealing the hidden types via case of only, the generated code would be way more complicated...

[radeusgd]

Yeah I guess for the GUI we need to keep the 'simpler' mv:Hidden_Type approach. Perhaps there the case of losing 'hidden types' when a conversion happens will not be as harmful? Maybe in practical GUI use-cases it won't be a big issue - I guess we need to see how this works in practice.