RFC: Loosening the recursive type restriction

[asajeffrey]

No description provided.

[asajeffrey]

Still a draft, as its exploring the design space, not making a concrete proposal yet.

[mheiber]

Interesting work!
Out of curiosity, do you anticipate ensuring types are contractive? If so, how?

Related: racket/typed-racket#1130

[asajeffrey]

Interesting work! Out of curiosity, do you anticipate ensuring types are contractive? If so, how?

Related: racket/typed-racket#1130

There's a separate check for contractiveness, but that's a simple syntactic check that all recursions are inside a function or table type.

[zeux]

One more alternative that I don't think is mentioned: you can either match the generic type list exactly from the declaration, or all types must not include any types from the generic type list from the declaration. Eg they must be "concrete" with a caveat that we treat generics from nested generics as "concrete" because they are expanded lazily. It doesn't seem like this gets us in trouble?

type Foo<T> = { field: Foo<T> } -- ok
type Foo<T> = { field: Foo<number> } -- ok
type Foo<T> = { field: <U>() -> Foo<U> } -- ok
type Foo<T> = { field: Foo<T?> } -- not ok

[asajeffrey]

That proposal would have the advantage of no exponential blowup. There would be cases where the workaround is duplicating the type, though I don't know if they'd come up in practice.

[asajeffrey]

I am inclined towards the "Strict recursive type instantiations with a cache" solution, as any syntactic restriction is likely to have poor ergonomics in terms of difficult-to-understand errors.

[zeux]

I don't fully understand this reasoning, as it seems like "strict recursive instantiation with a cache" generates unpredictable errors when an arbitrary size limit is exceeded. So this yields "recursive type is too complex" unpredictably?

[zeux]

(the strawman I proposed in a comment above would have errors that are completely determined by the code, and the error would say for example "Recursive generic type references are only allowed if instantiation is concrete or fully generic" or therabouts)

[asajeffrey]

I don't fully understand this reasoning, as it seems like "strict recursive instantiation with a cache" generates unpredictable errors when an arbitrary size limit is exceeded. So this yields "recursive type is too complex" unpredictably?

Yes, this would be yet another source of "types too complex" errors, of which we already have a lot. There is no good solution here, either we need to accept a somewhat arbitrary syntactic restriction or live with a restriction on cache size. Most other places in the typechecker we've just lived with limits, but this is user-driven enough we may want not to.

I don't understand what "instantiation is concrete or fully generic" means, I'm not sure many people will!

[zeux]

I don't understand what "instantiation is concrete or fully generic" means, I'm not sure many people will!

"Recursive type references are only allowed if type parameters don't depend on the generic arguments, unless they refer to the generic arguments verbatim".

[zeux]

Alternatively and more simply, includes problematic argument:

"Recursive type reference is not allowed because it refers to generic argument T, as this can result in infinite expansion; use a concrete type or specify all generic arguments verbatim in the same order"

Alternatively and more simply:

"Recursive type reference is not allowed because it refers to generic argument T, as this can result in infinite expansion; use a concrete type or the self-recursive Gen<T1, T2, T3> to fix"

(where Gen / Tn are actual names)

[asajeffrey]

I guess this proposal does deal with the cases we know about, and is the smallest delta that does.

[zeux]

Yeah what I like about it is that it's a subset of the more general behavior; I know that we just went from "anything goes" to "fully restrictive" but I'd rather evolve the rules in backwards-compatible fashion here from this point :) and this still allows us to implement a less restrictive version in the future.

[asajeffrey]

Wrote up the smallest delta proposal. Not a draft any more!

[zeux]

Can we move this to a separate paragraph before the cache description to make it clear that this is the new restriction? The cache then is essentially a description of the mechanics, but from the user perspective the critical part seems to be "either UI = aI for all I, or every UI does not contain any of the aJ/UI for all IJ"

[matthargett]

A note from an internal discussion that we may want to mention default type aliases, and what recursive behavior will be allowed within them, in this RFC.

[asajeffrey]

The issue being types like

  type T<A>  { p : A }
  type U<A, B> { q : T<A>, r : B }

which are not considered mutually recursive, so are fine. But add a default

  type T<A = U<A, number>>  { p : A }
  type U<A, B> { q : T<A>, r : B }

and oh dear these are now mutually recursive and boom.

[ghost]

One possibly relevant use case I have is typechecking and inferring promise parameters.

type promise<a, b, c, d> = {
    chain: <e, f>(((c) -> e)?, ((d) -> f)?) -> (promise<c, d, e, f>),
}
-- ...
promise.chain(function(value)
	return "swim"
end, function(error_message)
	return 1
end).chain(function(action)
	print(action) -- "swim"
end, function(error_count)
	print(error_count) -- 1
end)

[surfbryce]

One possibly relevant use case I have is typechecking and inferring promise parameters.

type promise<a, b, c, d> = {
    chain: <e, f>(((c) -> e)?, ((d) -> f)?) -> (promise<c, d, e, f>),
}
-- ...
promise.chain(function(value)
	return "swim"
end, function(error_message)
	return 1
end).chain(function(action)
	print(action) -- "swim"
end, function(error_count)
	print(error_count) -- 1
end)

I would like to put my support onto a use-case like this; I want to have a type-structure such as this:

type Promise<A...> = {
	Then: <B...>(
		callback: ((A...) -> B...)
	) -> Promise<B...>;
}

Right now we get an issue where recursive types cannot accept different parameters - this type of behavior is very crucial to replicating type awareness for chained-methods.

[zeux]

This PR is closed as part of RFC migration; please see #1074 (comment) for context.

Additional context: we do need to finish this, as it's a notable pain point. I would prefer that we somehow specify the behavior along the lines suggested above that doesn't rely on magical type cache size restrictions, as that represents a useful subset that covers enough user needs.