Skip to content

Commit

Permalink
Symetric, transitive and reflexive equality for intersection types (#…
Browse files Browse the repository at this point in the history
…11897)

Fixes #11845 by comparing all the types an `EnsoMultiValue` _has been cast to_.
  • Loading branch information
JaroslavTulach authored Dec 21, 2024
1 parent d87484b commit e8f781a
Show file tree
Hide file tree
Showing 14 changed files with 390 additions and 74 deletions.
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,10 +17,12 @@
- A constructor or type definition with a single inline argument definition was
previously allowed to use spaces in the argument definition without
parentheses. [This is now a syntax error.][11856]
- Symetric, transitive and reflexive [equality for intersection types][11897]

[11777]: https://github.com/enso-org/enso/pull/11777
[11600]: https://github.com/enso-org/enso/pull/11600
[11856]: https://github.com/enso-org/enso/pull/11856
[11897]: https://github.com/enso-org/enso/pull/11897

# Next Release

Expand Down
24 changes: 21 additions & 3 deletions docs/types/intersection-types.md
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ Just as demonstrated at
https://github.com/enso-org/enso/commit/3d8a0e1b90b20cfdfe5da8d2d3950f644a4b45b8#diff-c6ef852899778b52ce6a11ebf9564d102c273021b212a4848b7678e120776287R23
-->

## Narrowing Type Check
### Narrowing Type Check

When an _intersection type_ value is being downcast to _some of the types it
already represents_, these types become its _visible_ types. Any additional
Expand Down Expand Up @@ -160,9 +160,9 @@ 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`.
explicitly cast by the visual environment to `Column`.

## Converting Type Check
### 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
Expand All @@ -180,3 +180,21 @@ 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.

## Equality & Hash Code

A value of an intersection type is equal with other value, if all values _it has
been cast to_ are equal to the other value. E.g. a value of `Complex&Float` is
equal to some other value only if its `Complex` part and `Float` part are equal
to the other value. The _hidden_ types of a value (e.g. those that it _can be
cast to_, if any) aren't considered in the equality check.

The order of types isn't important for equality. E.g. `Complex&Float` value can
be equal to `Float&Complex` if the individual components (values _it has been
cast to_) match. As implied by (custom)
[equality rules](../syntax/functions.md#custom-equality) the `hash` of a value
of _intersection type_ must thus be a sum of `hash` values of all the values it
_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`).
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,9 @@ private static void registerValue(
if (!polyValue.isNull()) {
assertTrue("Type of " + polyValue + " is " + t, t.isMetaObject());
var rawValue = ContextUtils.unwrapValue(ctx(), polyValue);
if (rawValue instanceof EnsoMultiValue) {
return;
}
var rawType = ContextUtils.unwrapValue(ctx(), t);
if (rawType instanceof Type type) {
var singleMultiValue = EnsoMultiValue.create(new Type[] {type}, 1, new Object[] {rawValue});
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,120 @@
package org.enso.interpreter.test;

import static org.junit.Assert.assertTrue;

import java.io.ByteArrayOutputStream;
import java.nio.charset.StandardCharsets;
import org.enso.interpreter.runtime.data.EnsoMultiValue;
import org.enso.interpreter.runtime.data.Type;
import org.enso.interpreter.runtime.data.text.Text;
import org.enso.test.utils.ContextUtils;
import org.graalvm.polyglot.Context;
import org.graalvm.polyglot.Source;
import org.junit.AfterClass;
import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Ignore;
import org.junit.Test;

public class AnyToTest {
private static Context ctx;

private static final ByteArrayOutputStream out = new ByteArrayOutputStream();

@BeforeClass
public static void initCtx() {
ctx = ContextUtils.createDefaultContext(out);
}

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

@Before
public void resetOutput() {
out.reset();
}

private String getStdOut() {
return out.toString(StandardCharsets.UTF_8);
}

@Test
public void multiValueToInteger() throws Exception {
var ensoCtx = ContextUtils.leakContext(ctx);
var types =
new Type[] {ensoCtx.getBuiltins().number().getInteger(), ensoCtx.getBuiltins().text()};
var code =
"""
from Standard.Base import all
private eq a b = a == b
conv style v = case style of
0 -> v.to Integer
1 -> v:Integer
99 -> eq
""";
var conv =
ContextUtils.evalModule(ctx, Source.newBuilder("enso", code, "conv.enso").build(), "conv");
var both = EnsoMultiValue.create(types, types.length, new Object[] {2L, Text.create("Two")});
var eq =
ContextUtils.executeInContext(
ctx,
() -> {
var bothValue = ctx.asValue(both);
var asIntegerTo = conv.execute(0, bothValue);
var asIntegerCast = conv.execute(1, bothValue);
var equals = conv.execute(99, null);
return equals.execute(asIntegerTo, asIntegerCast);
});
assertTrue("Any.to and : give the same result", eq.asBoolean());
}

@Test
@Ignore
public void multiValueToText() throws Exception {
multiValueToText(2);
}

@Test
@Ignore
public void multiValueToTextHidden() throws Exception {
multiValueToText(1);
}

private void multiValueToText(int dispatchLength) throws Exception {
var ensoCtx = ContextUtils.leakContext(ctx);
var types =
new Type[] {ensoCtx.getBuiltins().number().getInteger(), ensoCtx.getBuiltins().text()};
var code =
"""
from Standard.Base import all
private eq a b = a == b
conv style:Integer v = case style of
2 -> v.to Text
3 -> v:Text
99 -> eq
""";
var conv =
ContextUtils.evalModule(ctx, Source.newBuilder("enso", code, "conv.enso").build(), "conv");
var both = EnsoMultiValue.create(types, dispatchLength, new Object[] {2L, Text.create("Two")});
var eq =
ContextUtils.executeInContext(
ctx,
() -> {
var bothValue = ctx.asValue(both);
var asIntegerCast = conv.execute(3, bothValue);
var asIntegerTo = conv.execute(2, bothValue);
var equals = conv.execute(99, null);
return equals.execute(asIntegerTo, asIntegerCast);
});
assertTrue("Any.to and : give the same result", eq.asBoolean());
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,13 @@ private static void registerValue(
var rawT2 = ContextUtils.unwrapValue(ctx(), t2);
if (rawT1 instanceof Type typ1 && rawT2 instanceof Type typ2) {
var r1 = ContextUtils.unwrapValue(ctx, v1);
if (r1 instanceof EnsoMultiValue) {
return;
}
var r2 = ContextUtils.unwrapValue(ctx, v2);
if (r2 instanceof EnsoMultiValue) {
return;
}
var both = EnsoMultiValue.create(new Type[] {typ1, typ2}, 2, new Object[] {r1, r2});
data.add(new Object[] {both});
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -111,15 +111,24 @@ public void testEqualityIntegerAndMultiValueWithBoth() {
var intType = builtins.number().getInteger();
var textText = builtins.text();
var hi = Text.create("Hi");
var fourExtraText =
var textFour =
EnsoMultiValue.create(new Type[] {textText, intType}, 2, new Object[] {hi, 4L});

assertTrue("4 == 4t", equalityCheck(4L, fourExtraText));
assertFalse("5 != 4t", equalityCheck(5L, fourExtraText));
assertTrue("4t == 4", equalityCheck(fourExtraText, 4L));
assertFalse("4t != 5", equalityCheck(fourExtraText, 5L));
assertTrue("4t == 'Hi'", equalityCheck(fourExtraText, hi));
assertTrue("'Hi' == 4t", equalityCheck(hi, fourExtraText));
var textFive =
EnsoMultiValue.create(new Type[] {textText, intType}, 2, new Object[] {hi, 5L});
var fourText =
EnsoMultiValue.create(new Type[] {intType, textText}, 2, new Object[] {4L, hi});

assertFalse("4 != t", equalityCheck(4L, hi));
assertFalse("4 != 4t", equalityCheck(4L, textFour));
assertFalse("5 != 4t", equalityCheck(5L, textFour));
assertFalse("5t != 4t", equalityCheck(textFive, textFour));
assertFalse("4t != 4", equalityCheck(textFour, 4L));
assertFalse("4t != 5", equalityCheck(textFour, 5L));
assertFalse("4t != 'Hi'", equalityCheck(textFour, hi));
assertFalse("'Hi' != 4t", equalityCheck(hi, textFour));

assertTrue("t4 == 4t", equalityCheck(textFour, fourText));
assertTrue("4t == t4", equalityCheck(fourText, textFour));

return null;
});
Expand All @@ -137,9 +146,9 @@ public void testEqualityIntegerAndMultiValueWithIntText() {
EnsoMultiValue.create(
new Type[] {intType, textText}, 2, new Object[] {4L, Text.create("Hi")});

assertTrue("4 == 4t", equalityCheck(4L, fourExtraText));
assertFalse("4 != 4t", equalityCheck(4L, fourExtraText));
assertFalse("5 != 4t", equalityCheck(5L, fourExtraText));
assertTrue("4t == 4", equalityCheck(fourExtraText, 4L));
assertFalse("4t != 4", equalityCheck(fourExtraText, 4L));
assertFalse("4t != 5", equalityCheck(fourExtraText, 5L));

return null;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,11 @@
import java.util.TimeZone;
import org.enso.common.MethodNames;
import org.enso.common.MethodNames.Module;
import org.enso.interpreter.node.expression.foreign.HostValueToEnsoNode;
import org.enso.interpreter.runtime.data.EnsoMultiValue;
import org.enso.interpreter.runtime.data.EnsoObject;
import org.enso.interpreter.runtime.data.Type;
import org.enso.test.utils.ContextUtils;
import org.graalvm.polyglot.Context;
import org.graalvm.polyglot.PolyglotException;
import org.graalvm.polyglot.Value;
Expand Down Expand Up @@ -865,6 +870,41 @@ public List<Value> problemBehaviors() {
return collect;
}

public List<Value> numbersMultiText() {
var leak = ContextUtils.leakContext(ctx);
var numberTextTypes =
new Type[] {
leak.getBuiltins().number().getInteger(), leak.getBuiltins().text(),
};
var textNumberTypes =
new Type[] {
leak.getBuiltins().text(), leak.getBuiltins().number().getInteger(),
};
var collect = new ArrayList<Value>();
var toEnso = HostValueToEnsoNode.getUncached();
for (var n : numbers()) {
for (var t : textual()) {
var rawN = toEnso.execute(ContextUtils.unwrapValue(ctx, n));
var rawT = ContextUtils.unwrapValue(ctx, t);
if (!(rawT instanceof EnsoObject)) {
continue;
}
addMultiToCollect(collect, numberTextTypes, 2, rawN, rawT);
addMultiToCollect(collect, numberTextTypes, 1, rawN, rawT);
addMultiToCollect(collect, textNumberTypes, 2, rawT, rawN);
addMultiToCollect(collect, textNumberTypes, 1, rawT, rawN);
}
}
return collect;
}

private void addMultiToCollect(
List<Value> collect, Type[] types, int dispatchTypes, Object... values) {
var raw = EnsoMultiValue.create(types, dispatchTypes, values);
var wrap = ctx.asValue(raw);
collect.add(wrap);
}

public List<Value> noWrap() {
var collect = new ArrayList<Value>();
if (languages.contains(Language.ENSO)) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ private static Object[] fetchAllUnwrappedValues() {
values.addAll(valGenerator.numbers());
values.addAll(valGenerator.booleans());
values.addAll(valGenerator.textual());
values.addAll(valGenerator.numbersMultiText());
values.addAll(valGenerator.arrayLike());
values.addAll(valGenerator.vectors());
values.addAll(valGenerator.maps());
Expand Down
Loading

0 comments on commit e8f781a

Please sign in to comment.