[Prev][Next][Index][Thread]

Re: MI: why?

>>>>> "Neel" == Neel Krishnaswami <neelk@brick.cswv.com> writes:

    Neel> Bruce Tobin <btobin@columbus.rr.com> wrote:
    >> > See "Predicate Dispatching: A Unified Theory of Dispatch," by
    >> Michael > D. Ernst, Craig Kaplan, and Craig Chambers, at: > >
    >> http://www.cs.washington.edu/research/projects/cecil/www/Papers/gud.html
    >> 
    >> Darned interesting.
    >> 
    >> > The downside, of course, is that method dispatch becomes
    >> undecidable.
    >> [..]
    Neel> If you added it to something like Python, though, there
    Neel> wouldn't be any performance hit because it doesn't do any
    Neel> optimization to make harder. :) Also, Erik Ernst wrote me in
    Neel> email that there are interesting decidable subsets of
    Neel> predicate dispatch, but I'll let him explain the details.

Here are the details :-)

Actually, it is possible to obey a certain discipline and in return
get a perfectly decidable problem.  The properties that we want to
check for a given generic function is that, for any given set of
argument types and values, there must be 

  - at least one applicable method  (if not: "message-not-understood")
  - at most one most specific applicable method (else: "ambiguous-method")

Assuming that the problem of statically checking ordinary multimethod
dispatch has been solved (which is old hat for methods that do not
depend on type variables, where it actually reduces to the boolean
expression problem anyway), the problem with arbitrary boolean
expressions can be handled in the following special case.  Here, 
a `guard' is a boolean expression associated with a given method M
whose truth value is used to determine whether M is applicable or
not):

  The logical expression which is the disjunction of the boolean
  guards for the methods of a generic function F must be a tautology,
  
and

  Any conjunction of a pair of boolean guards for F must be false.
E.g., if we have two boolean expressions E and F (whose run-time value
is of course in general undecidable), then we can still guarantee
statically that

   (E and F) or (E and not F) or (not E and F) or (not E and not F)

will be true for all values of E and F (i.e., at least one of the
parenthesized expressions will be true), and each of

   (E and F) and (E and not F)
   (E and F) and (not E and F)
   (E and F) and (not E and not F)
   (E and not F) and (not E and F)
   ...

will be false (so at most one of the parenthesized expressions will be
true).  So we can use a set of methods like these and rest
assured that exactly one method will be applicable at run-time, no
matter what the values of the general expressions E and F are:

   method M( ... )  // applicable if (E and F) is true
   method M( ... )  // applicable if (E and not F) is true
   method M( ... )  // applicable if (not E and F) is true
   method M( ... )  // applicable if (not E and not F) is true

It seems that this special case would cover at least a number of
interesting cases in practical programming (in particular because the
ordinary subtype-based dispatch guards considered as boolean
expressions may be analyzed deeper than expressions like x>0, so we
do not have to create full "truth matrices" for that kind of guards).


  regards,

-- 
Erik Ernst                                    eernst@cs.auc.dk
Department of Computer Science, University of Aalborg, Denmark
References: