Mutually recursive functions

Type inference for mutually recursive functions is actually quite a bit more complicated than you would think. For example, while thinking through how to implement mutually recursive functions in InforML, I came across something that I was confused about and wondered how we had handled it in AspectML. I spent some time meditating on the AspectML source and found that it didn't really address the issue. In particular, you can naïvely write

  1. % fun f <a:*>(x : a) = 5
  2. > and g <b:*>(y : b) = f y;

which you would think would be two functions »f« and »g« that given anything return 5. However, these functions are not accepted by the type checker

  1. InferenceProcess Error: Error between [interactive]:0.2-[interactive]:1.22
  2. Error between frontend/to-source.sml:170.78-frontend/to-source.sml:170.85
  3. Non-unifiable type variables: b and a
  4. while trying to unify types b and a
  5. while checking that b is subsumed by a
  6. inside (f y)
  7. inside fun f <(a : *)>((x : a)) = 5 and g <(b : *)>((y : b)) = (f y)

The problem is that AspectML rightful decided that »f« could not be used recursively at a polymorphic type, because it didn't initially know the return type. However, this becomes a problem because the type variable a isn't actually in-scope inside of »g«, that is »f« has an invalid type in a sense that should be a »compiler« error, as is illustrated by this slightly more complex example

  1. % fun f <a>(x : a) = 5
  2. > and g <b>(f : b -> Int) : Int = 5
  3. > and h y = g f;
  4. fun f <(a : *)>((x : a)) : Int = 5
  5. and g <(b : *)>((f : ((-> b) Int))) : Int = 5
  6. and h <(b5933 : *)>(y) : Int = (g f)
  7. TranslateProcess Error: Error between [interactive]:1.1-[interactive]:3.13
  8. Error between frontend/to-source.sml:170.78-frontend/to-source.sml:170.85
  9. Error between frontend/to-source.sml:607.85-frontend/to-source.sml:607.92
  10. toTyp: Could not find type variable a. This should be impossible!
  11. %

Of course, diagnosing the problem is the easy part. The difficult part will be figuring out which of the many possible fixes makes the most sense for InforML.

Leave a Comment