Comment by kragen
11 years ago
Sure, I'm pretty sure Turner's original Total Functional Programming proposal https://uf-ias-2012.wikispaces.com/file/view/turner.pdf doesdn't use dependent types, but I'm not sure it has what you mean by "a good runtime [that] does coinduction well".
All I mean by that is that you probably want to be able to evaluate a partiality monad in the runtime if you want to write an interpreter or webserver perhaps.