On 03-Nov-1998, Michael Hanus <[EMAIL PROTECTED]> wrote:
> Fergus Henderson wrote:
> > > Is there any Haskell implementation that supports polymorphic recursion
> > > without the need of annotating the types for defined function by the
> > > programmer?
> >
> > Not as far as I know.
> >
> > However, the current Mercury implementation supports this.
>
> This sounds interesting but how did you implement it?
> As far as I know, the problem of type inference with polymorphic
> recursion is undecidable due to the undecidability of the
> semi-unification problem.
Yes, that's correct. However, theoretical undecidability results often
don't say a lot about whether something is solvable in practice.
In theory, theory is correct, but in practice... ;-)
(Was it Isaac Asimov who said "if a scientist tells you
that something is possible, he is probably right, but if he
tells you that something is impossible, he is probably wrong"?)
The practical solution is quite simple. The fixpoint calculation runs
for a finite but user-selectable number of steps. If it doesn't reach
a fixpoint in that time, it halts with an error message that shows the
types it has inferred so far and that explains how to increase the limit.
In practice, the iteration limit is reached only for type-incorrect
programs. In theory it might be reached for programs with very complicated
types and few type declarations, but programmers tend not to write such
programs. If such situations do occur, it is always possible to recompile
with a higher iteration limit.
For type-incorrect programs which hit the limit, it is generally easy
to tell from the error message what the problem is (well, as easy as it
usually is to tell the cause of a problem from a type error message!).
P.S.
I think Hugs 1.3c and recent versions of ghc both support undecideable
features in their type systems -- but related to typeclasses and
instance declarations rather than to polymorphic recursion.
>From email with Mark Jones, I gather that Hugs does not use an
iteration limit mechanism, instead it just run out of memory if a
fixpoint is not reached. Of course, this must lead to rather poor
quality of diagnostics in such situations. It probably also results
in using up an unnecessarily large amount of memory and compilation time
when compiling some type-incorrect programs -- it's better to keep
the default limit smaller than "all of available memory".
I don't know whether ghc uses an iteration limit mechanism --
my guess is that it probably uses the same technique as Hugs.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
