Skip to content

Commit 9ad3271

Browse files
Docs: Remove discussion on termination: future work
"we should investigate whether..." -> doesn't belong to a spec page. Maybe that text should go into an issue?
1 parent f6057b7 commit 9ad3271

File tree

1 file changed

+1
-51
lines changed

1 file changed

+1
-51
lines changed

docs/docs/reference/new-types/match-types.md

Lines changed: 1 addition & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -143,55 +143,6 @@ The third rule states that a match type conforms to its upper bound
143143

144144
Within a match type `Match(S, Cs) <: B`, all occurrences of type variables count as covariant. By the nature of the cases `Ci` this means that occurrences in pattern position are contravarant (since patterns are represented as function type arguments).
145145

146-
## Handling Termination
147-
148-
Match type definitions can be recursive, which raises the question whether and how to check
149-
that reduction terminates. This is currently an open question. We should investigate whether
150-
there are workable ways to enforce that recursion is primitive.
151-
152-
Note that, since reduction is linked to subtyping, we already have a cycle dectection mechanism in place.
153-
So the following will already give a reasonable error message:
154-
```scala
155-
type L[X] = X match {
156-
case Int => L[X]
157-
}
158-
def g[X]: L[X] = ???
159-
```
160-
161-
```
162-
| val x: Int = g[Int]
163-
| ^^^^^^
164-
| found: Test.L[Int]
165-
| required: Int
166-
```
167-
168-
The subtype cycle test can be circumvented by producing larger types in each recursive invocation, as in the following definitions:
169-
```scala
170-
type LL[X] = X match {
171-
case Int => LL[LL[X]]
172-
}
173-
def gg[X]: LL[X] = ???
174-
```
175-
In this case subtyping enters into an infinite recursion. This is not as bad as it looks, however, because
176-
`dotc` turns selected stack overflows into type errors. If there is a stackoverflow during subtyping,
177-
the exception will be caught and turned into a compile-time error that indicates
178-
a trace of the subtype tests that caused the overflow without showing a full stacktrace.
179-
Concretely:
180-
```
181-
| val xx: Int = gg[Int]
182-
| ^
183-
|Recursion limit exceeded.
184-
|Maybe there is an illegal cyclic reference?
185-
|If that's not the case, you could also try to increase the stacksize using the -Xss JVM option.
186-
|A recurring operation is (inner to outer):
187-
|
188-
| subtype Test.LL[Int] <:< Int
189-
| subtype Test.LL[Int] <:< Int
190-
| ...
191-
| subtype Test.LL[Int] <:< Int
192-
```
193-
(The actual error message shows some additional lines in the stacktrace).
194-
195146
## Related Work
196147

197148
Match types have similarities with [closed type families](https://wiki.haskell.org/GHC/Type_families) in Haskell. Some differences are:
@@ -205,5 +156,4 @@ Match types are also similar to Typescript's [conditional types](https://github.
205156
match types also work for type parameters and abstract types.
206157
- Match types can bind variables in type patterns.
207158
- Match types support direct recursion.
208-
209-
Conditional types in Typescript distribute through union types. We should evaluate whether match types should support this as well.
159+
- Conditional types distribute through union types.

0 commit comments

Comments
 (0)