4 ms·

> One person noodling around for a few weeks Well, I've been trying for about three years, but to be fair I'm a pretty slow programmer so you may have better l

> One person noodling around for a few weeks Well, I've been trying for about three years, but to be fair I'm a pretty slow programmer so you may have better luck. > a language being too obscure to have seen much academic study Doesn't seem too obscure to me. https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=kotlin+acm https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=kotl... > T isn't generic in that code, it's just a class. I think it needs to be a generic type in Kotlin for this to work, because otherwise it will dispatch to a single method. It's tricky to get Kotlin to do much compile time computation. Not saying that it's impossible, but LMK when you've actually tried it. Here's some sample code if you want to try encoding a Boolean logic: https://github.com/breandan/galoisenne/blob/2e465e7a753f634100c40de6f5daa7356ca07b1b/src/commonMain/kotlin/ai/hypergraph/kaliningraph/automata/ECA.kt#L104 https://github.com/breandan/galoisenne/blob/2e465e7a753f6341...

lmm 4y ago
> Well, I've been trying for about three years, but to be fair I'm a pretty slow programmer so you may have better luck. Well, your own link proves it, doesn't it? Kotlin has nominal subtyping, contravariance, and generics, therefore its type system is undecidable. > I think it needs to be a generic type in Kotlin for this to work, because otherwise it will dispatch to a single method. That's the whole point - the type system has to decide which overload to dispatch it to at compile time, which it can only do by performing an arbitrarily complex computation. I ported that code directly to Kotlin and it doesn't compile but it "should", which, well, I don't know what you were expecting or what you'd accept as proof when we've already got an academic paper that proves the point.
- bmc7505 4y ago
  > 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
  - lmm 4y ago
    > 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..." Well, Kotlin has both declaration-site and use-site variance. So surely that result applies. > Can you share your translation of Eric's code? Maybe we can get it to work. Ah I didn't mean that code, I meant the earlier C# one from SO. https://pl.kotl.in/4BrbZAmZG https://pl.kotl.in/4BrbZAmZG

lmm 4y ago

> Well, I've been trying for about three years, but to be fair I'm a pretty slow programmer so you may have better luck. Well, your own link proves it, doesn't it? Kotlin has nominal subtyping, contravariance, and generics, therefore its type system is undecidable. > I think it needs to be a generic type in Kotlin for this to work, because otherwise it will dispatch to a single method. That's the whole point - the type system has to decide which overload to dispatch it to at compile time, which it can only do by performing an arbitrarily complex computation. I ported that code directly to Kotlin and it doesn't compile but it "should", which, well, I don't know what you were expecting or what you'd accept as proof when we've already got an academic paper that proves the point.

bmc7505 4y ago
> 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
- lmm 4y ago
  > 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..." Well, Kotlin has both declaration-site and use-site variance. So surely that result applies. > Can you share your translation of Eric's code? Maybe we can get it to work. Ah I didn't mean that code, I meant the earlier C# one from SO. https://pl.kotl.in/4BrbZAmZG https://pl.kotl.in/4BrbZAmZG