How can I divide two numbers in ML defined as a datatype?

Question

I'm trying to write a recursive function in SML that receives two natural numbers n1,n2 and returns the result of n1 div n2

The datatype natural is defined as follows:

datatype natural = zero | Succ of natural

I want to write it in terms of the new datatype , or in other words, not by converting them to their regular form and converting back the result.

Any ideas how division is done in this definition?

Answer 1

You could start by defining subtraction:

exception Negative

fun sub (a, zero) = a
  | sub (zero, b) = raise Negative
  | sub (Succ a, Succ b) = sub (a, b)

From here, it should be pretty easy to simply count how many times you can subtract n2 from n1 without going negative. In particular, this equation should help:

n1 div n2 = 1 + (n1 - n2) div n2

I'll leave the rest to you.