Support runtime checks of intersection types

[JaroslavTulach]

Pull Request Description

Fixes #6165 by removing support for \ and providing support for &. As a result of that we can now request multiple type classes for a single value.

Checklist

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

• The documentation has been updated, if necessary.
• All code follows the
  Scala,
  Java,
• All code has been tested:
  • Unit tests have been written where possible.
  • Remove support for \
  • Check benchmarks for slowdowns & another.
  • Check for duplicates

[Akirathan]

Seems OK and useful. Minor nitpicks.

[radeusgd]

I'm worried that such a big semantics change was merged so quickly.

I did not have a chance to review it properly before merging, but I feel like the PR is not tested enough. For example, this case is failing:

from Standard.Base import all

type Foo
    Value foo

    to_text : Text
    to_text self = "{FOO " ++ self.foo.to_text ++ "}"

Foo.from (that : Integer) = Foo.Value that

do_stuff (x : Integer & Foo) =
    IO.println x.foo
    IO.println (x==x)
    IO.println (x==42)
    IO.println (42==x)
    IO.println (100+x)

main =
    do_stuff 42

yields:

42
False
True
False
Execution finished with an error: Type error: expected `that` to be Integer, but got Integer.
        at <enso> intersections.do_stuff<arg-1>(intersections.enso:16:17-21)
        at <enso> intersections.do_stuff(intersections.enso:16:5-22)
        at <enso> intersections.main(intersections.enso:19:5-16)

It seems like our builtin nodes are not prepared to handle EnsoMultiValue - + panics, but even worse - equality loses symmetry and reflexivity!

[radeusgd]

Aren't we afraid that this kind of method resolution will introduce confusion?

If both Foo and Not_Foo have methods with the same name, which one is resolved will depend on the ordering of types there. IMO that will be confusing and not that easy to track down.

I'd rather detect ambiguity and require to narrow down to a single type, so that the reference is unambiguous.

I.e.

type A
    Value x
    foo self = self.x+100
    only_a self = self.x+1000
type B
    Value x
    foo self = self.x+200
    only_b self = self.x+2000

foo (v : A & B) =
    IO.println v.only_a # OK
    IO.println v.only_b # OK
    IO.println v.foo # IMO this should be an Ambiguous_Method_Resolution.Error saying that implementations from both A and B are available
    IO.println (v.to A . foo) # now it's unambiguous again

What do you think?

I'm not sure if what I'm proposing is better, but the current approach definitely introduces possible confusion. This is a big semantics change and I'm not aware of any discussions about it.

[Akirathan]

This is a big semantics change and I'm not aware of any discussions about it.

This PR only adds a runtime type checks for methods with intersection or union types. It does not define what intersection or union types are. Therefore, I'd say that there is in fact no semantic change at all. Moreover, this behavior is opt-in by specifying a particular method ascription.

Your observation with builtin nodes failing with EnsoMultiValue input is interesting, though. And worth further investigation.

[radeusgd]

This PR only adds a runtime type checks for methods with intersection or union types. It does not define what intersection or union types are. Therefore, I'd say that there is in fact no semantic change at all. Moreover, this behavior is opt-in by specifying a particular method ascription.

It introduces a new kind of value EnsoMultiValue which introduces a new style of method resolution (first type from types of the intersection type that contains a given method is chosen).

Yes, this is an opt-in change, that is true.

But it is available now. And once users start using it, it will be hard to change the semantics. And I feel like we did not have a chance to discuss the implications of e.g. the new method resolution style.

[JaroslavTulach]

this should be an Ambiguous_Method_Resolution.Error saying that implementations from both A and B are available

Such an approach could lead to CharSequence.isEmpty() situation - e.g. a situation where two independent and correct on each own changes adding something into two types could break their usage at intersection. We haven't yet tried to evolve Enso libraries in a 99% compatible way, so it is hard to predict what is going to be optimal for that - in general I am not fan of throwing errors in production when a viable, deterministic resolution exists. However yes, the check for ambiguities can be implemented with no slowdown with some work.

Btw. even the sample test contains such ambiguities as both types define dict. Based on such experience I started work on (x : Plus) syntax that should make the exact resolution natural for programmers.

[JaroslavTulach]

This PR only adds a runtime type checks for methods with intersection or union types.
It does not define what intersection or union types are.

A program that did run before and for some reason used & types, may no longer finish, but yield an error. E.g. yes, this changes semantics, but that's what we want: either support & checks or remove & altogether just like \.

Yes, this is an opt-in change, that is true.

There was no code using & yet - e.g. yes, it is an opt-in. I suggest to wait with widespread usage until (x : Text) destiny is set as the x : Plus syntax would make the usage far more easy.

It introduces a new kind of value EnsoMultiValue

Many engine PRs introduce new kind of value (for example #4023) and then we deal with consequences (like in #7348). There is nothing special on that and honestly, there is probably no other way to support & types in a dynamic language like Enso.

which introduces a new style of method resolution:

Right. One has to resolve the methods somehow. Either:

• first type containing a given method is chosen
• last type ...
• random type ...
• error is raised when there are two types containing a method
• no method can be called on such multi value

Enough reviewers of this PR approved the "first type" approach. However, as there are no usages yet, there is time for change.

[JaroslavTulach]

equality loses symmetry and reflexivity!

With https://github.com/enso-org/enso/pull/7796/files#r1324206886 the equality has reflexivity back.

GitHub

Checking ascribed expression types for existence by JaroslavTulach · Pull Request #7796 · enso-org/enso

Pull Request Description Fixes #6848 by:

making sure type in a:Xyz exists or yielding an error otherwise
making sure type in a:Integer is checked at runtime
simplifies conversions by using these i...