Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Symetric, transitive and reflexive equality for intersection types #11897

Merged
merged 11 commits into from
Dec 21, 2024
Merged
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);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems like you forgot to test style 2 and 3, i.e.:

              var asTextTo = conv.execute(2, bothValue);
              var asTextCast = conv.execute(3, bothValue);
assertTrue(equals.execute(asTextTo, asTextCast).asBoolean());

Copy link
Member Author

@JaroslavTulach JaroslavTulach Dec 20, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good catch, not only it is not called, but it is also broken. These two new tests added in d30da41 are failing on CI

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
Loading