Search code examples
sml

SML recursive type error when converting numbers to nat form


I am practicing SML and getting the following recursive type error. Is ML complaining about type recursive and needs some type hints? I am confused.

datatype 'a nat =
    Zero
  | Succ of 'a
  ;

fun to_nat(v) = if v = 0 then Zero else Succ(to_nat(v - 1));

fun plus(n1,n2) =
  case n1 of
    Zero => n2
  | Succ(v) => Succ(plus(v, n2))
    ;

fun multiply(n1,n2) =
  case n1 of
    Zero => Zero
  | Succ(v) => plus(multiply(v, n2), n2)
    ;

val five = to_nat(5);
val six = to_nat(6);
val eleven = plus(five, six);
val thirty = multiply(five, six);

Error:

Standard ML of New Jersey v110.79 [built: Sat Oct 26 12:27:04 2019]
[opening lambda.sml]
datatype 'a num = Succ of 'a | Zero
lambda.sml:6.5-6.60 Error: right-hand-side of clause doesn't agree with function result type [circularity]
  expression:  'Z num
  result type:  'Z
  in declaration:
    to_num = (fn v => if <exp> = <exp> then Zero else Succ <exp>)
/usr/lib/smlnj/bin/sml: Fatal error -- Uncaught exception Error with 0
 raised at ../compiler/TopLevel/interact/evalloop.sml:66.19-66.27

Solution

  • I believe you made a mistake in defining your data type. You want Succ to take a value of type 'a nat rather than 'a.

    datatype 'a nat = Zero | Succ of 'a nat;