Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Intersection types & type checks #11600

Merged
merged 43 commits into from
Dec 12, 2024
Merged
Show file tree
Hide file tree
Changes from 39 commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
c0c2fc5
Splitting types in EnsoMultiValue to methodDispatchTypes and the rest
JaroslavTulach Nov 20, 2024
c780c37
Merging with latest chances in develop
JaroslavTulach Nov 22, 2024
515e134
Don't expose EnsoMultiValue methods directly
JaroslavTulach Nov 25, 2024
d0460a4
TypeOf UnresolvedConstructor and UnresolvedSymbol test
JaroslavTulach Nov 25, 2024
a101fe6
Merge branch 'wip/jtulach/UseTypeOfNode11482' into wip/jtulach/Comple…
JaroslavTulach Nov 25, 2024
4e08d8f
UnsupportedMessageException.create accepts only AbstractTruffleException
JaroslavTulach Nov 25, 2024
acebbc1
Unwrap EnsoMultiValue before composing new EnsoMultiValue.create
JaroslavTulach Nov 25, 2024
af85b11
Avoid double wrapping test
JaroslavTulach Nov 25, 2024
ba5953f
Only consider booleans up to methodDispatchTypes
JaroslavTulach Nov 25, 2024
c2d1911
EqualsMultiValueTest
JaroslavTulach Nov 25, 2024
11f8ebc
Two unit tests showing a difference between success and failure
JaroslavTulach Nov 25, 2024
0278257
Special EqualsNode for EnsoMultiValue
JaroslavTulach Nov 25, 2024
720f644
Primitive interop types are mutually exclusive - we need to use one f…
JaroslavTulach Nov 25, 2024
ebaf492
Merge remote-tracking branch 'origin/develop' into wip/jtulach/Comple…
JaroslavTulach Nov 25, 2024
b5fc062
Interop value cannot be both isString and isNumber
JaroslavTulach Nov 25, 2024
02ec775
Handle EnsoMultiValue in a special way
JaroslavTulach Nov 25, 2024
57da6eb
Base EnsoMultiValue.equals on findAllTypesOrNull
JaroslavTulach Nov 26, 2024
3d048be
Documenting the example of Text and extra Integer equality check
JaroslavTulach Nov 26, 2024
be5dbe8
Don't consider extra multi value types in equals
JaroslavTulach Nov 26, 2024
0a81038
Note in the changelog
JaroslavTulach Nov 26, 2024
9fc4bb4
No need for StructsLibrary hack anymore
JaroslavTulach Nov 26, 2024
3a09a8d
No changes in GetFieldNode needed
JaroslavTulach Nov 26, 2024
20973d0
Intersection type and additional conversions tests
JaroslavTulach Nov 26, 2024
ce4c738
Verify dispatch of methods behaves as expected
JaroslavTulach Nov 27, 2024
a6ff51b
Only consider methodDispatchTypes for from conversions
JaroslavTulach Nov 27, 2024
957b3eb
Additional multi value tests
Akirathan Nov 29, 2024
dc490cf
Stream.of.anyMatch
JaroslavTulach Nov 29, 2024
d3102ad
Cleaning up allocated context
JaroslavTulach Nov 29, 2024
57eaf4a
Let converted by the variable name
JaroslavTulach Nov 29, 2024
9929fe8
Finishing documentation sentence
JaroslavTulach Nov 29, 2024
f5fbcf4
Otherwise extract value of type
JaroslavTulach Nov 29, 2024
ca0dd9a
Test also equality with Hi
JaroslavTulach Nov 29, 2024
2f72704
Send multi value as a method argument test
JaroslavTulach Dec 4, 2024
d1172a9
Merge remote-tracking branch 'origin/develop' into wip/jtulach/Comple…
JaroslavTulach Dec 10, 2024
f386c7b
All types state for type check nodes
JaroslavTulach Dec 10, 2024
7db299b
Documenting behavior of intersection types
JaroslavTulach Dec 11, 2024
1167b52
Documenting the converting type check
JaroslavTulach Dec 11, 2024
6b3b4d6
Example of failing conversions
JaroslavTulach Dec 11, 2024
52038f7
Verify case of on multi value
JaroslavTulach Dec 11, 2024
9eaa742
Note about #11600 in CHANGELOG.md belongs to Next Next Release
JaroslavTulach Dec 11, 2024
d1cbc8d
Radek's comments to Intersection Types documentation
radeusgd Dec 12, 2024
77619ab
Open to subclasses
JaroslavTulach Dec 12, 2024
91987ca
Multi value == is not transitive
JaroslavTulach Dec 12, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,10 @@
#### Enso Language & Runtime

- [Arguments in constructor definitions may now be on their own lines][11374]
- [Intersection types & type checks][11600]

[11374]: https://github.com/enso-org/enso/pull/11374
[11600]: https://github.com/enso-org/enso/pull/11600
- [The `:` type operator can now be chained][11671].

[11374]: https://github.com/enso-org/enso/pull/11374
Expand Down
1 change: 1 addition & 0 deletions docs/syntax/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ The various components of Enso's syntax are described below:
- [**Functions:**](./functions.md) The syntax for writing functions in Enso.
- [**Function Arguments:**](./function-arguments.md) The syntax for function
arguments in Enso.
- [**Conversions:**](./conversions.md) The syntax of special _conversion functions_ in Enso.
- [**Field Access:**](./projections.md) The syntax for working with fields of
data types in Enso.
- [**Comments:**](./comments.md) The syntax for writing comments in Enso.
35 changes: 35 additions & 0 deletions docs/syntax/conversions.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
---
layout: developer-doc
title: Defining Functions
category: syntax
tags: [syntax, functions]
order: 10
---

# Conversions

Conversions are special [functions](./functions.md) associated with a [type](../types/hierarchy.md),
named `from` and taking single `that` argument. Following example:
```ruby
type Complex
Num re:Float im:Float

Complex.from (that:Float) = Complex.Num that 0
```
defines type `Complex` and a **conversion** from `Float` which uses the provided `Float` value as
real part of a complex number while setting the imaginary part to zero.

## Type Checks

Conversions are integral part of [type checking](../types/inference-and-checking.md#type-checking-algorithm)
during runtime. Having the right conversion in scope one can write:
```ruby
complex_pi = 3.14:Complex
```
to create a new instance of type `Complex`. The Enso runtime represents
the `3.14` literal as `Float` value and that would fail the `Complex` type check if there was no
conversion method available. However as there is one, the runtime uses `Complex.from` behind the
scene and `complex_pi` then becomes `Complex.Num 3.14 0` value.

Type checks may perform no, one or multiple conversions (like in case of
[intersection types](../types/intersection-types.md)).
1 change: 1 addition & 0 deletions docs/types/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ Information on the type system is broken up into the following sections:
- [**Goals for the Type System:**](./goals.md) The goals for the Enso type
system, particularly around usability and user experience.
- [**The Type Hierarchy:**](./hierarchy.md) The type hierarchy in Enso.
- [**Intersection Types:**](./intersection-types.md) intersection types in Enso.
- [**Function Types:**](./function-types.md) Function types in Enso.
- [**Access Modification:**](./access-modifiers.md) Access modifiers in Enso
(e.g. `private` and `unsafe`),
Expand Down
2 changes: 1 addition & 1 deletion docs/types/hierarchy.md
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ They are as follows:
- **Union - `|`:** This operator creates a typeset that contains the members in
the union of its operands.
- **Intersection - `&`:** This operator creates a typeset that contains the
members in the intersection of its operands.
members in the [intersection of its operands](./intersection-types.md).

> [!WARNING]
> These operators _don't seem to be supported_. There is no plan to
Expand Down
104 changes: 104 additions & 0 deletions docs/types/intersection-types.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
---
layout: developer-doc
title: The Enso Type Hierarchy
category: types
tags: [types, hierarchy, typeset]
order: 2
---

# Intersection Types

Intersection types play an important role in Enso [type hierarchy](./hierarchy.md)
and its visual representation. Having a value that can play _multiple roles_
at once is essential for smooth _live programming_ manipulation of such a value.

Intersections types are created with the use of [`&` operator](./hierarchy.md#typeset-operators).
In an attempt to represent `Complex` numbers (with real and imaginary component)
one may decide to create a type that is both `Complex` and `Float` when the
imaginary part is `0`:
```ruby
type Complex
Num re:Float im:Float

plain_or_both self =
if self.im != 0 then self else
both = self.re : Complex&Float
both # value with both types: Complex and Float
```
Having a value with such _intersection type_ allows the IDE to offer operations
available on all individual types.

## Creating

Creating a value of _intersection types_ is as simple as performing a type check:
```ruby
self : Complex&Float
```
However such a _type check_ is closely associated with [conversions](../syntax/conversions.md).
If the value doesn't represent all the desired types yet, then the system looks
for [conversion methods](../syntax/conversions.md) being available in the scope like:
```
Complex.from (that:Float) = Complex.Num that 0
```
and uses them to create all the values the _intersection type_ represents.

## Narrowing Type Check

When an _intersection type_ value is being downcast to _one of the types it already represents_,
such a check is:
- recorded for purposes of [dynamic dispatch](../types/dynamic-dispatch.md)
- recorded for cases when the value is passed as an argument
- however the value still keeps (internal) knowledge of all the types it represents

As such a _static analysis_ knows the type a value _has been cast to_ and
can deduce the set of operations that can be performed with it. However, the value
_can be cast to_ explicitly.

> [!NOTE]
> In the **object oriented terminology** we can think of
> a type `Complex&Float` as being a subclass of `Complex` and subclass of `Float` types.
> As such a value of type `Complex&Float` may be used wherever `Complex` or `Float` types
> are used. Let there, for example, be a function:
> ```ruby
> use_complex c:Complex callback:(Any -> Any) = callback c
> ```
> that accepts `Complex` value and passes it back to a provided callback function.
> It is possible to pass a value of `Complex&Float` type to such a function. Only
> operations available on type `Complex` can be performed on value in variable `c`.
>
> However the `callback` function may still explicitly cast the value to `Float`.
> E.g. the following is valid:
> ```ruby
> both = v : Complex&Float
> use_complex both (v-> v:Float . sqrt)
> ```
> This behavior is often described as being **openness to subclasses**. E.g. the `c:Complex`
> check allows values with _intersection types_ that include `Complex` to pass thru with
> all their runtime information available,
> but one has to perform an explicit cast to extract the other types associated with
> such a value.

This behavior allows creation of values with types like `Table&Column` to represent a table
with a single column - something the users of visual _live programming_ environment of Enso find
very useful.
```ruby
Table.join self right:Table -> Table = ...
```
Such a `Table&Column` value can be returned from the above `Table.join` function and while
having only `Table` behavior by default, still being able to be explicitly casted by the visual environment
to `Column`.

## Converting Type Check

When an _intersection type_ is being checked against a type it doesn't represent,
any of its component types can be used for [conversion](../syntax/conversions.md).
Should there be a `Float` to `Text` conversion:
```ruby
Text.from (that:Float) = Float.to_text
```
then `Complex&Float` value `cf` can be typed as `cf:Text`. The value can also
be converted to another _intersection type_ like `ct = cf:Complex&Text`. In such case
it looses its `Float` type and `ct:Float` would fail.

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.
Original file line number Diff line number Diff line change
Expand Up @@ -89,15 +89,15 @@ private static void registerValue(
var rawValue = ContextUtils.unwrapValue(ctx(), polyValue);
var rawType = ContextUtils.unwrapValue(ctx(), t);
if (rawType instanceof Type type) {
var singleMultiValue = EnsoMultiValue.create(new Type[] {type}, new Object[] {rawValue});
var singleMultiValue = EnsoMultiValue.create(new Type[] {type}, 1, new Object[] {rawValue});
var n = t.getMetaSimpleName();
data.add(new Object[] {singleMultiValue, n, 0});
var rawInt = (Type) ContextUtils.unwrapValue(ctx(), g.typeInteger());
var secondMultiValue =
EnsoMultiValue.create(new Type[] {rawInt, type}, new Object[] {5L, rawValue});
EnsoMultiValue.create(new Type[] {rawInt, type}, 2, new Object[] {5L, rawValue});
data.add(new Object[] {secondMultiValue, n, 1});
var firstMultiValue =
EnsoMultiValue.create(new Type[] {type, rawInt}, new Object[] {rawValue, 6L});
EnsoMultiValue.create(new Type[] {type, rawInt}, 2, new Object[] {rawValue, 6L});
data.add(new Object[] {firstMultiValue, n, 0});
} else {
if (!t.isHostObject()) {
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
package org.enso.interpreter.node.typecheck;

import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertTrue;

import com.oracle.truffle.api.CallTarget;
import org.enso.interpreter.runtime.data.EnsoMultiValue;
import org.enso.interpreter.runtime.data.Type;
import org.enso.test.utils.ContextUtils;
import org.enso.test.utils.TestRootNode;
import org.graalvm.polyglot.Context;
import org.junit.AfterClass;
import org.junit.Test;

public class TypeCheckValueTest {
private static Context ctx;

private static Context ctx() {
if (ctx == null) {
ctx = ContextUtils.defaultContextBuilder().build();
}
return ctx;
}

@AfterClass
public static void closeCtx() {
if (ctx != null) {
ctx.close();
}
ctx = null;
}

@Test
public void avoidDoubleWrappingOfEnsoMultiValue() {
var convert = allOfIntegerAndText();

ContextUtils.executeInContext(
ctx(),
() -> {
var builtins = ContextUtils.leakContext(ctx).getBuiltins();
var m1 =
EnsoMultiValue.create(
new Type[] {builtins.text(), builtins.number().getInteger()},
2,
new Object[] {"Hi", 42});
assertEquals("Text & Integer", m1.toDisplayString(true));

var res = convert.call(m1);
assertTrue("Got multivalue again", res instanceof EnsoMultiValue);
var emv = (EnsoMultiValue) res;

assertEquals("Integer & Text", emv.toDisplayString(true));
return null;
});
}

private static CallTarget allOfIntegerAndText() {
var call = new CallTarget[1];
ContextUtils.executeInContext(
ctx(),
() -> {
var builtins = ContextUtils.leakContext(ctx).getBuiltins();
var intNode = TypeCheckValueNode.single("int", builtins.number().getInteger());
var textNode = TypeCheckValueNode.single("text", builtins.text());
var bothNode = TypeCheckValueNode.allOf("int&text", intNode, textNode);
var root =
new TestRootNode(
(frame) -> {
var arg = frame.getArguments()[0];
var res = bothNode.handleCheckOrConversion(frame, arg, null);
return res;
});
root.insertChildren(bothNode);
call[0] = root.getCallTarget();
return null;
});
return call[0];
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
package org.enso.interpreter.test;

import com.oracle.truffle.api.interop.InteropLibrary;
import java.util.ArrayList;
import org.enso.interpreter.runtime.data.EnsoMultiValue;
import org.enso.interpreter.runtime.data.Type;
import org.enso.test.utils.ContextUtils;
import org.graalvm.polyglot.Context;
import org.graalvm.polyglot.Value;
import org.junit.AfterClass;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;

@RunWith(Parameterized.class)
public class EnsoMultiValueInteropTest {

@Parameterized.Parameter(0)
public Object value;

private static Context ctx;

private static Context ctx() {
if (ctx == null) {
ctx = ContextUtils.defaultContextBuilder().build();
}
return ctx;
}

@Parameterized.Parameters
public static Object[][] allEnsoMultiValuePairs() throws Exception {
var g = ValuesGenerator.create(ctx());
var typeOf =
ContextUtils.evalModule(
ctx(),
"""
from Standard.Base import all

typ obj = Meta.type_of obj
main = typ
""");
var data = new ArrayList<Object[]>();
for (var v1 : g.allValues()) {
for (var v2 : g.allValues()) {
registerValue(g, typeOf, v1, v2, data);
}
}
return data.toArray(new Object[0][]);
}

private static void registerValue(
ValuesGenerator g, Value typeOf, Value v1, Value v2, ArrayList<Object[]> data) {
var t1 = typeOf.execute(v1);
var t2 = typeOf.execute(v2);
if (!t1.isNull() && !t2.isNull()) {
var rawT1 = ContextUtils.unwrapValue(ctx(), t1);
var rawT2 = ContextUtils.unwrapValue(ctx(), t2);
if (rawT1 instanceof Type typ1 && rawT2 instanceof Type typ2) {
var r1 = ContextUtils.unwrapValue(ctx, v1);
var r2 = ContextUtils.unwrapValue(ctx, v2);
var both = EnsoMultiValue.create(new Type[] {typ1, typ2}, 2, new Object[] {r1, r2});
data.add(new Object[] {both});
}
}
}

@AfterClass
public static void disposeCtx() throws Exception {
if (ctx != null) {
ctx.close();
ctx = null;
}
}

@Test
public void isStringDoesntFail() {
ContextUtils.executeInContext(
ctx,
() -> {
return InteropLibrary.getUncached().isString(value);
});
}
}
Loading
Loading