type-checking difficulties in recursive functions

type-checking difficulties in recursive functions

[Mike Hamburg]

I'm having trouble with a recursive function which tries to use itself, 
instantiated to a different type, in the recursion.

As a trivial example similar to what I want to do, consider:

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 
by writing

let rec string_foo p : 'string -> 'string = Obj.magic foo p
and foo p x =
	if p then x
	else
		let something = string_foo false "Hello"
		in x;;
val string_foo : bool -> string -> string = <fun>
val foo : bool -> 'a -> 'a = <fun>

but is there a way to avoid magic?

Thanks,
Mike Hamburg
P.S. I couldn't find the bug in my Netcgi program, but by deleting and 
rewriting part of it, I got it working :-)

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

[Andreas Rossberg]

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

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

[brogoff]

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