4 ms·
Could you elaborate on that? It sounds like I may have an overly simplified understanding of the topic here—wouldn't be the first time.
by tehnub 5y ago
Could you elaborate on that? It sounds like I may have an overly simplified understanding of the topic here—wouldn't be the first time.
- native_samples 5y agoStatic type systems don't imply fully dependent types. In Kotlin: sealed class Program class HaltingProgram : Program() class InfiniteProgram : Program() fun checkIsHalting(p: ByteArray) = if (halts(p)) HaltingProgram() else InfiniteProgram() This program will type check just fine. The inferred return type will be Program because that's the nearest shared ancestor type of both possible return types. Good luck implementing the halts() function of course, but that's not the type system's problem.