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

[brogoff <brogoff@speakeasy.net>]

On Wed, 27 Apr 2005, Andreas Rossberg wrote:
> 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":

It's also possible (and slightly nicer IMO) to use the experimental recursive
module facility to encode polymorphic recursion in OCaml. There are some
restrictions, but they're not horrible.

Speaking of modules, for a while, there was talk of some notion of mixin modules
to address the problems (and more) being addressed by the recursive module
feature. Anyone in the know care to comment on what happened with that?

-- Brian