-
Notifications
You must be signed in to change notification settings - Fork 324
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Intersection types & type checks (#11600)
Implementation of **type checks** for **intersection types**. The idea is to split the list of `types[]` in `EnsoMultiValue` into two parts: - first `methodDispatchTypes` represent the types the value _"has been cast to"_ - the rest of the types represent the types the value _"can be cast to"_ By performing this separation we address the #10882 requirements. After a type check only methods available on the `methodDispatchTypes` can be invoked. However the value can still be cast to all the possible types.
- Loading branch information
1 parent
ffd0de4
commit 2964457
Showing
30 changed files
with
1,253 additions
and
203 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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)). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,157 @@ | ||
--- | ||
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. | ||
|
||
> [!NOTE] | ||
> Note that if a `Float.from (that:Complex)` conversion were available in the scope, | ||
> any `Complex` instance would be convertible to `Float` regardless of how it was constructed. | ||
> To ensure that such mix-ins are only available on values that opt-in to being | ||
> an intersection type (like in the `Complex` example above where we include | ||
> the `Float` mix-in only if `self.im == 0`), we need to ensure that the conversion | ||
> used to create the intersection type is not available in the default | ||
> conversion resolution scope. Thus it cannot be defined in the same module | ||
> as `Complex` or `Float` types, but instead it should be defined in a separate | ||
> module that is only imported in the place that will be constructing the multi-values. | ||
<!-- | ||
Just as demonstrated at | ||
https://github.com/enso-org/enso/commit/3d8a0e1b90b20cfdfe5da8d2d3950f644a4b45b8#diff-c6ef852899778b52ce6a11ebf9564d102c273021b212a4848b7678e120776287R23 | ||
--> | ||
|
||
## 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 types it represents become _hidden_. | ||
|
||
The following operations consider only the _visible_ part of the type: | ||
- [dynamic dispatch](../types/dynamic-dispatch.md) | ||
- cases when value is passed as an argument | ||
|
||
However the value still keeps internal knowledge of all the types it represents. | ||
|
||
Thus, after casting a value `cf:Complex&Float` to just `Complex`, e.g. `c = cf:Complex`: | ||
- method calls on `c` will only consider methods defined on `Complex` | ||
- the value `c` can only be passed as argument to methods expecting `Complex` type | ||
- a type error is raised when a `Float` parameter is expected | ||
|
||
As such a _static analysis_ knows the type a value _has been cast to_ (the _visible_ part) | ||
and can deduce the set of operations that can be performed with it. Moreover, any | ||
method calls will also only accept the value if it satisfies the type it | ||
_has been cast to_. Any additional remaining _hidden_ types | ||
can only be brought back through an _explicit_ cast. | ||
To perform an explicit cast that can uncover the 'hidden' part of a type write | ||
`f = c:Float`. | ||
|
||
<!-- | ||
When #11828 is fixed. | ||
- or inspect the types in a `case` expression, e.g. | ||
``` | ||
case c of | ||
f : Float -> f.sqrt | ||
_ -> "Not a float" | ||
``` | ||
--> | ||
|
||
> [!WARNING] | ||
> Keep in mind that while both argument type check in method definitions and a | ||
> 'type asserting' expression look similarly, they have slightly different behaviour. | ||
> ``` | ||
> f a:Float = a | ||
> g a = a:Float | ||
> ``` | ||
> These two functions, while very similar, will have different behaviour when | ||
> passed a value like the value `c` above. The function `f` will fail with | ||
> a type error, because the visible type of `c` is just `Complex` (assuming | ||
> the conversion to `Float` is not available in the current scope). | ||
> However, the function `g` will accept the same value and return it as | ||
> a `Float` value, based on the 'hidden' part of its type. | ||
> [!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 **open 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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
79 changes: 79 additions & 0 deletions
79
...tegration-tests/src/test/java/org/enso/interpreter/node/typecheck/TypeCheckValueTest.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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]; | ||
} | ||
} |
Oops, something went wrong.