> Well, your own link proves it, doesn't it? That code simulates a bounded cellular automaton, which effectively reduces to a regular language, but that's abou

> Well, your own link proves it, doesn't it? That code simulates a bounded cellular automaton, which effectively reduces to a regular language, but that's about as far as I've been able to get. If it's possible to implement general recursion, I'm not quite sure how - yet. > Kotlin has nominal subtyping, contravariance, and generics, therefore its type system is undecidable. They're not using Kennedy and Pierce's system, but it's closely related. See Tate (2013) [1], in particular, "In general, since declaration-site variance can easily be encoded into use-site variance..." > I ported that code directly to Kotlin Can you share your translation of Eric's code? Maybe we can get it to work. [1]: https://fool2013.cs.brown.edu/tate.pdf https://fool2013.cs.brown.edu/tate.pdf