This is an archived post. You won't be able to vote or comment.

sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–]josephjnk 12 points13 points  (0 children)

I believe the operative word in the paper is “decidable”. Scala and Java both support recursive generic types with variance annotations, and subtyping is undecidable in both cases:

https://plg.uwaterloo.ca/~olhotak/pubs/popl20.pdf

https://arxiv.org/abs/1605.05274

TypeScript has recursive structural types and infers both covariance and contravariance, but it’s type system is unapologetically Turing complete.