| > Totality is orthogonal to dependent types. You can absolutely have non-total programs at the type level: Rust has such programs today in fact! Absolutely, the talk I linked to gets at this to some extent. In rust, partiality causes type checking to fail. You could use it on purpose! > You can have an infinite loop in a total language like Agda or Idris: coinduction is the mechanism. For sure, but the totality checker is appeased by sized-types, or at least that's how I know to do it in Agda. I've heard it can be done without them, but I'm not familiar with the approach. This is what I intended w/r/t structural recursion. > This doesn't make a whole lot of sense to me. This is because, as the authors state, to type check the program is to evaluate it, so before it can run you have proof that it is correct. By opting out I'm more talking about the converse, to opt in when you need it. Kind of the opposite of Idris's %partial directive. > You can be total over IO, and effects do not imply non-totality either. That's fair, you're right. This is poorly stated. |