Adding some practical tests for intersection types in context of using them for 'refining' types #12144
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,339 @@ | ||
| ## This tests the usage of intersection types as refinement of a value's type. | ||
| These tests rely on a conversion A -> B that is not available in the scope, | ||
| so a type is A & B only if it was 'refined' somewhere else. Then we are | ||
| testing what happens to such instances after various casts, type checks etc. | ||
|
|
||
| from Standard.Base import all | ||
| from Standard.Test import all | ||
| import Standard.Base.Errors.Common.Type_Error | ||
| import Standard.Base.Errors.Common.No_Such_Conversion | ||
| import Standard.Base.Errors.Common.No_Such_Method | ||
| import Standard.Base.Errors.Illegal_State.Illegal_State | ||
|
|
||
| from project.Semantic.Type_Refinement.Types import A, B, make_a_and_b | ||
|
|
||
| id_a (x : A) -> A = x | ||
| id_b (x : B) -> B = x | ||
|
|
||
| type C | ||
| C_Ctor x | ||
|
|
||
| c_method self = "C method" | ||
|
|
||
| C.from (that:B) = C.C_Ctor that | ||
|
|
||
| add_specs suite_builder = | ||
| suite_builder.group "Multi Value as type refinement" group_builder-> | ||
| group_builder.specify "conversion A -> B should not be available" <| | ||
| just_a = A.A_Ctor 1 | ||
| Test.expect_panic Type_Error (just_a:B) | ||
| Test.expect_panic No_Such_Conversion (B.from just_a) | ||
| Test.expect_panic Type_Error (id_b just_a) | ||
|
|
||
| group_builder.specify "make_a_and_b->A&B presents as both A and B" <| | ||
| ab = make_a_and_b | ||
| ab.is_a A . should_be_true | ||
| ab.is_a B . should_be_true | ||
|
|
||
| ab.a_method . should_equal "A method" | ||
| ab.b_method . should_equal "B method" | ||
|
|
||
| (ab:A).to_text . should_equal "(A_Ctor 1)" | ||
| (ab:B).to_text . should_equal "(B_Ctor (A_Ctor 1))" | ||
| (id_a ab).to_text . should_equal "(A_Ctor 1)" | ||
| (id_b ab).to_text . should_equal "(B_Ctor (A_Ctor 1))" | ||
|
|
||
| group_builder.specify "after passing A&B value to a function expecting A argument, B becomes hidden" <| | ||
| ab = make_a_and_b | ||
| a2 = id_a ab | ||
| a2.is_a A . should_be_true | ||
| a2.is_a B . should_be_false | ||
|
|
||
| # Passing a2 to a function expecting B fails because B part was hidden | ||
| Test.expect_panic Type_Error (id_b a2) | ||
| Test.expect_panic No_Such_Method (a2.b_method) | ||
|
|
||
| # But it can be uncovered via explicit cast | ||
| (a2:B).b_method . should_equal "B method" | ||
| (id_b (a2:B)).to_text . should_equal "(B_Ctor (A_Ctor 1))" | ||
|
|
||
| group_builder.specify "after casting A&B to A, B part is again hidden" <| | ||
| ab = make_a_and_b | ||
| a2 = ab:A | ||
| a2.is_a A . should_be_true | ||
| a2.is_a B . should_be_false | ||
|
|
||
| # Passing a2 to a function expecting B fails because B part was hidden | ||
| Test.expect_panic Type_Error (id_b a2) | ||
|
|
||
| # But it can be uncovered via explicit cast | ||
| (a2:B).to_text . should_equal "(B_Ctor (A_Ctor 1))" | ||
| (id_b (a2:B)).to_text . should_equal "(B_Ctor (A_Ctor 1))" | ||
|
|
||
| group_builder.specify "passing A&B to function expecting B, then re-casting to A" <| | ||
| ab = make_a_and_b | ||
| b2 = id_b ab | ||
| a2 = b2:A | ||
| a2.is_a A . should_be_true | ||
| a2.is_a B . should_be_false | ||
|
|
||
| a2.a_method.should_equal "A method" | ||
| Test.expect_panic No_Such_Method (a2.b_method) | ||
|
|
||
| group_builder.specify "passing A&B to function expecting A, then re-casting to B" <| | ||
| ab = make_a_and_b | ||
| a2 = id_a ab | ||
| b2 = a2:B | ||
| b2.is_a A . should_be_false | ||
| b2.is_a B . should_be_true | ||
|
|
||
| Test.expect_panic No_Such_Method (b2.a_method) | ||
| b2.b_method.should_equal "B method" | ||
radeusgd marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| # We can still explicitly cast back to A | ||
| (b2:A).a_method.should_equal "A method" | ||
|
|
||
radeusgd marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| group_builder.specify "unpacking an intersection type via pattern matching" <| | ||
| ab = make_a_and_b | ||
| case ab of | ||
| ab_as_a : A -> | ||
| ab_as_a.a_method . should_equal "A method" | ||
| ab_as_a.is_a A . should_be_true | ||
| ab_as_a.is_a B . should_be_false | ||
| _ -> Test.fail "Expected ab to go to `: A` branch" | ||
|
|
||
| case ab of | ||
| ab_as_b : B -> | ||
| ab_as_b.b_method . should_equal "B method" | ||
| ab_as_b.is_a A . should_be_false | ||
| ab_as_b.is_a B . should_be_true | ||
| _ -> Test.fail "Expected ab to go to `: B` branch" | ||
|
|
||
| group_builder.specify "pattern matching does not apply conversions" <| | ||
| ab = make_a_and_b | ||
| r = case ab of | ||
| _ : C -> "matched C" | ||
| _ -> "was not C" | ||
| r.should_equal "was not C" | ||
|
|
||
| group_builder.specify "using a conversion discards the multi-value structure and we 'start over'" <| | ||
| ab = make_a_and_b | ||
| c = ab:C | ||
|
|
||
| c.is_a C . should_be_true | ||
| c.is_a A . should_be_false | ||
| c.is_a B . should_be_false | ||
|
|
||
| # We cannot convert back to A/B as the mutli-value structure is lost | ||
| Test.expect_panic Type_Error (c:A) | ||
| Test.expect_panic Type_Error (c:B) | ||
|
|
||
| group_builder.specify "conversion can keep the old types if they are listed explicitly in a cast expression" <| | ||
| ab = make_a_and_b | ||
| abc = ab:(A & B & C) | ||
|
|
||
| abc.is_a A . should_be_true | ||
| abc.is_a B . should_be_true | ||
| abc.is_a C . should_be_true | ||
|
|
||
| abc.a_method . should_equal "A method" | ||
| abc.b_method . should_equal "B method" | ||
| abc.c_method . should_equal "C method" | ||
|
|
||
| # We hide A&B parts by casting to C | ||
| c = abc:C | ||
| c.is_a A . should_be_false | ||
| c.is_a B . should_be_false | ||
| c.is_a C . should_be_true | ||
|
|
||
| Test.expect_panic No_Such_Method (c.a_method) | ||
| Test.expect_panic No_Such_Method (c.b_method) | ||
| c.c_method . should_equal "C method" | ||
|
|
||
| # But because the structure was not lost, only hidden, we can cast back to A/B | ||
| (c:A).a_method . should_equal "A method" | ||
| (c:B).b_method . should_equal "B method" | ||
|
|
||
| (c:A&B&C).a_method . should_equal "A method" | ||
| (c:A&B&C).b_method . should_equal "B method" | ||
| (c:A&B&C).c_method . should_equal "C method" | ||
|
|
||
| group_builder.specify "default to_text should delegate to one of values" pending="TODO: https://github.com/enso-org/enso/issues/11827" <| | ||
| ab = make_a_and_b | ||
| ab.to_text . should_equal "(A_Ctor 1)" | ||
|
|
||
| abc = ab:(A & B & C) | ||
| abc.to_text . should_equal "(A_Ctor 1)" | ||
|
|
||
| c = abc:C | ||
| c.to_text . should_equal "(C_Ctor (B_Ctor (A_Ctor 1)))" | ||
|
|
||
| (c:A).to_text . should_equal "(A_Ctor 1)" | ||
| (c:B).to_text . should_equal "(B_Ctor (A_Ctor 1))" | ||
|
|
||
| group_builder.specify "structural pattern matching should be able to match the primary type" pending="TODO: https://github.com/enso-org/enso/issues/12142" <| | ||
| ab = make_a_and_b | ||
| r = case ab of | ||
| A.A_Ctor x -> "matched: "+x.to_text | ||
| _ -> "structural matching of A.A_Ctor failed" | ||
| r.should_equal "matched: 1" | ||
|
|
||
| group_builder.specify "should structural matching match other types?" pending="TODO: decide if we keep this test inhttps://github.com/enso-org/enso/issues/12142" <| | ||
| ab = make_a_and_b | ||
| r = case ab of | ||
| B.B_Ctor x -> "matched: "+x.to_text | ||
| _ -> "structural matching of B.B_Ctor failed" | ||
| r.should_equal "matched: (A_Ctor 1)" | ||
|
|
||
| dispatch_pending="TODO: https://github.com/enso-org/enso/issues/12143" | ||
| group_builder.specify "calling a method on one of the types should not lose the intersection type" pending=dispatch_pending <| | ||
| ab = make_a_and_b | ||
|
|
||
| # Checked variant can hide the B part | ||
| ab.a_id . is_a A . should_be_true | ||
| ab.a_id . is_a B . should_be_false | ||
| # But it can be uncovered via explicit cast | ||
| b = (ab.a_id):B | ||
| b.is_a A . should_be_false | ||
| b.is_a B . should_be_true | ||
|
|
||
| new_ab = (ab.a_id):A&B | ||
| new_ab.is_a A . should_be_true | ||
| new_ab.is_a B . should_be_true | ||
| new_ab.a_method . should_equal "A method" | ||
| new_ab.b_method . should_equal "B method" | ||
|
|
||
| # But unchecked variant should keep both types and not hide anything | ||
| ab.a_id_unchecked . is_a A . should_be_true | ||
| ab.a_id_unchecked . is_a B . should_be_true | ||
| ab.a_id_unchecked.a_method . should_equal "A method" | ||
| ab.a_id_unchecked.b_method . should_equal "B method" | ||
|
|
||
| # The same should apply to the B part | ||
| ab.b_id . is_a A . should_be_false | ||
| ab.b_id . is_a B . should_be_true | ||
| new_ab_2 = (ab.b_id):A&B | ||
| new_ab_2.is_a A . should_be_true | ||
| new_ab_2.is_a B . should_be_true | ||
| ab.b_id_unchecked . is_a A . should_be_true | ||
| ab.b_id_unchecked . is_a B . should_be_true | ||
| ab.b_id_unchecked.a_method . should_equal "A method" | ||
| ab.b_id_unchecked.b_method . should_equal "B method" | ||
|
|
||
| group_builder.specify "calling `.catch` on an intersection type should not lose the refinements" <| | ||
| ab = make_a_and_b | ||
| r = ab.catch Any _->"catched" | ||
| r.is_a A . should_be_true | ||
| r.is_a B . should_be_true | ||
| r.a_method . should_equal "A method" | ||
| r.b_method . should_equal "B method" | ||
|
|
||
| group_builder.specify "calling `.throw_on_warning` on an intersection type should not lose the refinements" <| | ||
| ab = make_a_and_b | ||
| r = ab.throw_on_warning | ||
| r.is_a A . should_be_true | ||
| r.is_a B . should_be_true | ||
| r.a_method . should_equal "A method" | ||
| r.b_method . should_equal "B method" | ||
|
Comment on lines
+230
to
+236
There was a problem hiding this comment. 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. There was a problem hiding this comment. After all I've found a repro: b8407da |
||
|
|
||
| group_builder.specify "attaching warnings to an intersection type should not lose the refinements" <| | ||
| ab = make_a_and_b | ||
| ab_with_warning = Warning.attach (Illegal_State.Error "my warning") ab | ||
| ab_with_warning.is_a A . should_be_true | ||
| ab_with_warning.is_a B . should_be_true | ||
| ab_with_warning.a_method . should_equal "A method" | ||
| ab_with_warning.b_method . should_equal "B method" | ||
| Problems.expect_only_warning Illegal_State ab_with_warning | ||
|
|
||
| group_builder.specify "removing warnings from an intersection type should not lose the refinements" <| | ||
| ab = make_a_and_b | ||
| ab_with_warning = Warning.attach (Illegal_State.Error "my warning") ab | ||
|
|
||
| ab_without_warning = ab_with_warning.remove_warnings | ||
| Problems.assume_no_problems ab_without_warning | ||
| ab_without_warning.is_a A . should_be_true | ||
| ab_without_warning.is_a B . should_be_true | ||
| ab_without_warning.a_method . should_equal "A method" | ||
| ab_without_warning.b_method . should_equal "B method" | ||
|
|
||
| ab2 = ab.remove_warnings | ||
| ab2.is_a A . should_be_true | ||
| ab2.is_a B . should_be_true | ||
| ab2.a_method . should_equal "A method" | ||
| ab2.b_method . should_equal "B method" | ||
|
|
||
| group_builder.specify "calling both `throw_on_warning` and `catch` should not lose the refinements" <| | ||
| ab = make_a_and_b | ||
| r = ab.throw_on_warning Illegal_State . catch Any _->"catched" | ||
| r.is_a A . should_be_true | ||
| r.is_a B . should_be_true | ||
| r.a_method . should_equal "A method" | ||
| r.b_method . should_equal "B method" | ||
|
|
||
| group_builder.specify "calling `.catch` on an intersection type should not lose even the hidden refinements" pending=dispatch_pending <| | ||
| ab = make_a_and_b | ||
| x = ab:A | ||
| r = x.catch Any _->"catched" | ||
| r.a_method . should_equal "A method" | ||
| # After calling catch we should still be able to bring back the B part | ||
| (r:B).b_method . should_equal "B method" | ||
|
|
||
| y = r:(A & B) | ||
| y.is_a A . should_be_true | ||
| y.is_a B . should_be_true | ||
| y.a_method . should_equal "A method" | ||
| y.b_method . should_equal "B method" | ||
|
|
||
| group_builder.specify "calling `.throw_on_warning` on an intersection type should not lose even the hidden refinements" pending=dispatch_pending <| | ||
| ab = make_a_and_b | ||
| x = ab:A | ||
| r = x.throw_on_warning | ||
|
|
||
| y = r:(A & B) | ||
| y.is_a A . should_be_true | ||
| y.is_a B . should_be_true | ||
| y.a_method . should_equal "A method" | ||
| y.b_method . should_equal "B method" | ||
|
|
||
| group_builder.specify "attaching warnings to an intersection type should not lose even the hidden refinements" pending=dispatch_pending <| | ||
| ab = make_a_and_b | ||
| x = ab:A | ||
| x_with_warning = Warning.attach (Illegal_State.Error "my warning") x | ||
|
|
||
| y = x_with_warning:(A & B) | ||
| y.is_a A . should_be_true | ||
| y.is_a B . should_be_true | ||
| y.a_method . should_equal "A method" | ||
| y.b_method . should_equal "B method" | ||
| Problems.expect_only_warning Illegal_State y | ||
|
|
||
| group_builder.specify "removing warnings from an intersection type should not lose even the hidden refinements" pending=dispatch_pending <| | ||
| ab = make_a_and_b | ||
| x1 = Warning.attach (Illegal_State.Error "my warning") (ab:A) | ||
| x2 = (Warning.attach (Illegal_State.Error "my warning") ab):A | ||
|
|
||
| x1_without_warning = x1.remove_warnings | ||
| x2_without_warning = x2.remove_warnings | ||
|
|
||
| r1 = x1_without_warning:(A & B) | ||
| r2 = x2_without_warning:(A & B) | ||
| Problems.assume_no_problems r1 | ||
| r1.is_a A . should_be_true | ||
| r1.is_a B . should_be_true | ||
| r1.a_method . should_equal "A method" | ||
| r2.b_method . should_equal "B method" | ||
| Problems.assume_no_problems r2 | ||
| r2.is_a A . should_be_true | ||
| r2.is_a B . should_be_true | ||
| r2.a_method . should_equal "A method" | ||
| r2.b_method . should_equal "B method" | ||
|
|
||
| r3 = (ab:A).remove_warnings:(A & B) | ||
| r3.is_a A . should_be_true | ||
| r3.is_a B . should_be_true | ||
| r3.a_method . should_equal "A method" | ||
| r3.b_method . should_equal "B method" | ||
|
|
||
| main filter=Nothing = | ||
| suite = Test.build suite_builder-> | ||
| add_specs suite_builder | ||
| suite.run_with_filter filter | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,7 @@ | ||
| private | ||
|
|
||
| from project.Semantic.Type_Refinement.Types import A, B | ||
|
|
||
| ## This conversion should only be imported in `Type_Refinement.Types` and nowhere else. | ||
| B.from (that : A) -> B = | ||
| B.B_Ctor that |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| from project.Semantic.Type_Refinement.Hidden_Conversions import all | ||
AdRiley marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| type A | ||
| A_Ctor x | ||
|
|
||
| a_method self = "A method" | ||
| a_id_unchecked self = self | ||
| a_id self -> A = self | ||
|
|
||
| type B | ||
| B_Ctor x | ||
|
|
||
| b_method self = "B method" | ||
| b_id_unchecked self = self | ||
| b_id self -> B = self | ||
|
|
||
| make_a_and_b -> A & B = | ||
| a = A.A_Ctor 1 | ||
| # Relies on the hidden conversion | ||
| (a : A & B) | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
EnsoMultiValueasselfwhen dispatchingAnyinstance methods #12170 changes the wayAnyinstance methods are dispatcheda2.is_a Bchangesselfto first value which type hasis_a- e.g.AEnsoMultiValueasselfwhen dispatchingAnyinstance methods #12170 theselfremainsEnsoMultiValueis_achecksdispatchas well asextratypes ofEnsoMultiValue.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, I see.
The
is_acase 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_amade sense.If I call
x.is_a Integerit tells me that I can call allIntegermethods 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 Integerbut that does not tell me if I can callx.roundon it? I'm not sure if this is a good step forward.The dispatch change is of course correct, but perhaps
is_ashould rely on a different logic? It is a builtin anyway.We were considering adding a
x.could_be_athat checks theextratypes. But IMHO theis_ashould focus only on thedispatchtypes.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Changed to 34b6a3d as part of #12170
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could x.is_a Integer return true AND you could call x.round on it, be a good solution?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 typeT. 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 callx.fooonxfails becauseTdoes not have methodfoo- I cannot rule out that at runtimexwill have a hidden typeUthat may have the methodfooand 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:Uassertion tells it "The user asserts thatxalso has typeU, if the control flow has continued that means this assertion was correct - so from now on I can infer calls onxas if it had typeU.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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One of the ideas was to use
x : T & Anyas a kind of cast that assertsxis of typeTbut maybe something more too. Then indeed a value like that couldx.is_a Uand allow callingUmethods on it, becausex : T & Anytells us it can be anything.I like this approach because while after
x : T & Anymuch of type inference is not that capable, it is a 'local only' problem - elsewhere in the code where I havex : TI can still infer normally. Not to say thatx : T & Anymay have its downsides too (like users perhaps 'accidentally' cutting off some refined types by casting without the& Anysuffix). I know @JaroslavTulach was not a fan of& Anyapproaches and had some reasons for that.