Re: [Caml-list] type-checking difficulties in recursive functions

["Andreas Rossberg" <AndreasRossberg@web.de>]

Mike Hamburg <hamburg@fas.harvard.edu> wrote:
>
> let rec foo p x =
> if p then x
> else
> let something = foo false "Hello"
> in x;;
> val foo : bool -> string -> string = <fun>
>
> Now, foo is actually safe as a function from bool -> 'a -> 'a, but the
> recursive declaration doesn't generalize and so the checker doesn't
> realize this.  With magic, I can get the right type relatively safely

What you want is "polymorphic recursion". Unfortunately, type inference for
polymorphic recursion is undecidable in general. Haskell allows polymorphic
recursion if you annotate the type, so that it doesn't have to be inferred.
In OCaml, this is not possible directly, but you can achieve the same effect
by going through a record and using the more recent feature of polymorphic
record fields, plus OCaml's let rec "language extension":

  type foo_rec = {foo : 'a.bool->'a->'a}
  let rec foo_rec = {foo = fun p x -> if p then x else let _ = foo_rec.foo
false "" in x}
  let foo = foo_rec.foo

Not particularly nice, but does what you want.

Hope this helps,

  - Andreas