[mercury-users] literature polymorphic recursive calls
Tom Schrijvers
Tom.Schrijvers at cs.kuleuven.ac.be
Fri Jun 24 07:36:43 AEST 2005
> >> I guess Mercury takes a third
> >> approach: it does multiple iterations to handle some non-problematic
> >> recursive definitions. What happens if the limit is reached? I should
> >> try
> >> it :)
> >
> > Well, even HM checkers can take an exponential amount of time in the
> > worst case! In practice this problem just doesn't arise (at least, not
> > in my experience).
>
> In fact because of adhoc overladoing it is worse for Mercury.
> But in practice problems dont arise.
>
> Still in my opinion Mercury should just use the HM assumption if
> there are no declarations. In any polymorphic recusrive code the
> iterated approach will never infer the polymorphic type
>
> p(X,Y) :- (X == Y -> p(true,false) ; p(1,2))
According to what I have read so far (in particular in a functional
context), iteration is necessary until the bodies of (possibly
polymorphic) recursive functions have the same inferred type as the
assumed types. For well-typed programs iteration should terminate after
some finite number of steps. For ill-typed programs it may not. The
problem is for a well-typed program how many iteration steps are needed.
Some expressions are supposed to have big types that are exponentially
larger than the expressions themselves.
Mercury could enfore the HM monomorphic recursion assumption after the
fixed number of maximum iteration steps. In this way it should be able to
type all programs that are typable by HM and at the same time infer more
principal types. Still, the max. iteration number is a rather arbitrary
way to define the set of typable programs.
Tom
--------------------------------------------------------------------------
mercury-users mailing list
post: mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the users
mailing list