How are you going to make division total?

[pkoch]

Everyone cheats on that one.

[zesterer]

For reals, division is already total. For integers, there are two options:

• Have the output type of division be Real (there is already precedent for this, negation on a Nat yields an Int)
• Have the output type be (Nat, Nat) (i.e: integer division + remainder)

I think I'd tend towards the former as the more natural option, with the latter as an independent function.

Obviously, this doesn't account for division by zero though: it might be necessary to have some way to express that a value is non-zero in the type system, such as through dependent types.

Ideas are welcome!

[pkoch]

Obviously, this doesn't account for division by zero though: it might be necessary to have some way to express that a value is non-zero in the type system, such as through dependent types.

Yeah, this was more my point. I see you've resisted the common cheat of making Zero - Succ(Zero) == Zero, I was wondering what you have in mind to prevent zero divisions. They do feel like something a dependent type system can tackle. However, I've never seen in implemented, hence the question.

Cheers, and great work! 👏