Browse thread
type-checking difficulties in recursive functions
-
Mike Hamburg
-
Andreas Rossberg
- brogoff
-
Andreas Rossberg
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | brogoff <brogoff@s...> |
| Subject: | Re: [Caml-list] type-checking difficulties in recursive functions |
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