Documenting expected behaviour of intersection types #13384

radeusgd · 2025-06-26T14:41:38Z

Pull Request Description

As discussed, we try to summarize our common understanding on expected behaviour of intersection types in various circumstances.

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.

GregoryTravis · 2025-06-26T15:47:57Z

docs/types/intersection-types.md

+- inspecting the type via `case of`, e.g.
+  ```
+  case x of
+      a : A -> ...


What happens in this case?

Suggested change

a : A -> ...

b : B -> ...

a : A -> ...

GregoryTravis · 2025-06-26T15:49:00Z

docs/types/intersection-types.md

+  ```
+  in the first branch, the `a` has visible type `A` but the full type is still
+  `a : A & (hidden B)` - the `B` part is hidden, but not removed.
+- dispatching a method on one of the types, e.g. calling `x.method_defined_on_A`


Is it the same when calling a method defined on a hidden type? x.method_defined_on_B?

GregoryTravis · 2025-06-26T15:49:58Z

docs/types/intersection-types.md

+  will pass the value `x` as `self` to the body of `method_defined_on_A`, the
+  `self` will have a visible type `A`, but the full type is still
+  `self : A & (hidden B)` - so the `self` value can be casted if needed.
+- normally, calling conversions will 'start over' and the value returned from


What happens if there are conversions from both A and B to some other type? Do unhidden ones take precedence over hidden ones?

JaroslavTulach

Thanks for improving the docs, Radek.
I prefer positive tone in the docs
e.g. describe how great Enso design is
and only then warn what would happen if it wasn't as great

JaroslavTulach · 2025-06-27T05:48:41Z

docs/types/intersection-types.md

@@ -198,3 +248,10 @@ _has been cast to_. As a special case any value wrapped into an _intersection
 type_, but _cast down_ to the original type is `==` and has the same `hash` as
 the original value. E.g. `4.2 : Complex&Float : Float` is `==` and has the same
 `hash` as `4.2` (in spite it _can be cast to_ `Complex`).
+
+### TODO


What's the purpose of this TODO? If the functionality is broken, can we link to the appropriate issues?

self preserves intersection types, just hides them

That works, doesn't it?

JaroslavTulach · 2025-06-27T05:49:32Z

docs/types/intersection-types.md

@@ -181,6 +181,56 @@ In short: when a [conversion](../syntax/conversions.md) is needed to satisfy a
 type check a new value is created to satisfy just the types requested in the
 check.

+## Preserving identity of refined types
+
+Intersection types are used to refine a value giving it additional


Suggested change

Intersection types are used to refine a value giving it additional

Intersection types are often used to refine a value with additional

JaroslavTulach · 2025-06-27T05:50:40Z

docs/types/intersection-types.md

+this compound type may get _hidden_ when passing around various methods (e.g.
+`table:Table` will hide the `DB_Table` part), but the value itself still retains
+its identity as a `Table & DB_Table` and can be uncovered via a cast or a case
+expression.


Suggested change

expression.

expression during runtime.

JaroslavTulach · 2025-06-27T05:54:23Z

docs/types/intersection-types.md

+its identity as a `Table & DB_Table` and can be uncovered via a cast or a case
+expression.
+
+It is important to ensure that various operations do not accidentally remove a


I don't like the term various operations

it only spreads FUD

there is no point of being so vague in the documentation

if you have to, move it into a "warning" or "notice" section

e.g. a colloquial knowledge, not part of the spec

JaroslavTulach · 2025-06-27T05:56:57Z

docs/types/intersection-types.md

+It is important to ensure that various operations do not accidentally remove a
+part of the intersection type as then the value completely loses its part of
+functionality. If the `DB_Table` part is not hidden, but completely removed, the
+table can no longer be casted to `DB_Table` and used as such. This is confusing
+for users, as a database table cannot suddenly stop being a database table just
+by passing it around (including method calls) or casting.
+
+Consider a multi value `x : A & B`. We indicate hidden types as `(hidden T)` -
+they are not visible in the actual type, but can be uncovered via casts or
+reflection.
+
+To ensure the above properties, the interpreter ensures that the following
+operations only hide the intersection type, but do not remove it:


Here is a short version:

Suggested change

It is important to ensure that various operations do not accidentally remove a

part of the intersection type as then the value completely loses its part of

functionality. If the `DB_Table` part is not hidden, but completely removed, the

table can no longer be casted to `DB_Table` and used as such. This is confusing

for users, as a database table cannot suddenly stop being a database table just

by passing it around (including method calls) or casting.

Consider a multi value `x : A & B`. We indicate hidden types as `(hidden T)` -

they are not visible in the actual type, but can be uncovered via casts or

reflection.

To ensure the above properties, the interpreter ensures that the following

operations only hide the intersection type, but do not remove it:

To ensure intersection types properly propagate thru the Enso program the

basic language constructs are designed to handle them properly. Namely:

the actual wording can be different, but I'd prefer the positive focus rather than description of catharsis in the docs.

JaroslavTulach · 2025-06-27T06:03:17Z

docs/types/intersection-types.md

+  - similarly, calling `B.from x` will return a value of type `B & (hidden A)` -
+    the `A` part is still there (only hidden), because no actual conversion code
+    had to be run.
+


Please note the use of these operations rather than various operations ;-)

Suggested change

It is important to ensure these operations do not remove a part of the intersection type.

Otherwise the value loses part of its functionality which would have a detrimental effect

in the GUI, confusing users.

If the `DB_Table` part is not kept as hidden, but completely removed, the

table can no longer be casted to `DB_Table` and used as such.

A little Cassandra's warning at the end may be acceptable...

documenting expected behaviour of intersection types

63a0a6e

radeusgd added the CI: No changelog needed Do not require a changelog entry for this PR. label Jun 26, 2025

radeusgd mentioned this pull request Jun 26, 2025

Explicitly calling T.from x looses type refinement of intersection types #13379

Closed

radeusgd requested review from JaroslavTulach, AdRiley, jdunkerley and GregoryTravis June 26, 2025 15:24

radeusgd assigned AdRiley Jun 26, 2025

GregoryTravis approved these changes Jun 26, 2025

View reviewed changes

JaroslavTulach approved these changes Jun 27, 2025

View reviewed changes

JaroslavTulach mentioned this pull request Jun 27, 2025

Only reordering in Type.from for eligible EnsoMultiValue #13387

Merged

4 tasks

enso-bot bot mentioned this pull request Jun 28, 2025

Less heavyweight jvm-channel by removing dependency on engine-common #13363

Merged

2 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Documenting expected behaviour of intersection types #13384

Documenting expected behaviour of intersection types #13384

Uh oh!

radeusgd commented Jun 26, 2025 •

edited

Loading

Uh oh!

GregoryTravis Jun 26, 2025

Uh oh!

GregoryTravis Jun 26, 2025

Uh oh!

GregoryTravis Jun 26, 2025

Uh oh!

JaroslavTulach left a comment

Uh oh!

JaroslavTulach Jun 27, 2025

Uh oh!

JaroslavTulach Jun 27, 2025

Uh oh!

JaroslavTulach Jun 27, 2025

Uh oh!

JaroslavTulach Jun 27, 2025

Uh oh!

JaroslavTulach Jun 27, 2025

Uh oh!

JaroslavTulach Jun 27, 2025

Uh oh!

Uh oh!

	Intersection types are used to refine a value giving it additional
	Intersection types are often used to refine a value with additional

+It is important to ensure these operations do not remove a part of the intersection type.
+Otherwise the value loses part of its functionality which would have a detrimental effect
+in the GUI, confusing users.
+If the `DB_Table` part is not kept as hidden, but completely removed, the
+table can no longer be casted to `DB_Table` and used as such.

Documenting expected behaviour of intersection types #13384

Are you sure you want to change the base?

Documenting expected behaviour of intersection types #13384

Uh oh!

Conversation

radeusgd commented Jun 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Pull Request Description

Important Notes

Checklist

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JaroslavTulach left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

radeusgd commented Jun 26, 2025 •

edited

Loading