4 ms·
Idris is Turing Complete. Total functions are opt-in.
by Dewie 12y ago
Idris is Turing Complete. Total functions are opt-in.
- tel 12y agoIdris' opt-in totality is a weird beast since those opts are extralinguistic. I really consider it to be a downside when a language is turing complete these days—I'd rather Idris just use a partiality monad. So, maybe I'm just using the power of wishful thinking with my characterization above.