FD improvement, variable quantification & generalised propagation

[Claus Reinke]

I've had some interesting off-list discussion with Tom Schrijvers
(one of the guys responsible for the K.U.Leuven CHR System,
which is provided, eg., in SWI Prolog). particularly interesting
was the difference in perspective (logic vs functional programming).

I'd like to share two items from that discussion (haven't thought
either of them through yet, but hope they both provide useful 
food for thought to those of you interested in the type class 
problem).

1. I didn't have to explain to him that FDs may lead to variable 
    instantiation, but I did have to explain why without FDs, there 
    is no variable instantiation, and why we even think about FD 
    consistency without automatically implying unification 
    (improvement).

    the main difference here seems to be that he was thinking of all
    variables as existentially quantified, whereas type variables are 
    mostly universally quantified, so far.

    I hadn't given that much thought before, because FDs are meant
    to determine their range types, and there isn't much difference
    between universal and existential quantification if there is only
    one possible variable value, eg: 

        (forall a in {Char}. T a) vs (exists a in {Char}. T a)

    but perhaps some of the interpretation disagreements we have 
    with FDs could be mitigated if we interpreted FDs differently,
    depending on whether the range type variables are universally
    or existentially quantified.

    given some 'class C a b | a -> b', we could try something like:

    - forall a b. C a b => T a b:
        no improvement for b, the FD is used only for checking
        consistency

    - forall a. exists b. C a b => T a b
        improvement & consistency check for b

2. he suggested that the whole problem may be an instance of
    generalised propagation:
    
    Generalised Constraint Propagation Over the CLP Scheme,
    by Thierry Le Provost and Mark Wallace. Journal of Logic 
    Programming 16, July 1993. Also [ECRC-92-1] 
    http://eclipse.crosscoreop.com:8080/eclipse/reports/ecrc_genprop.ps.gz

    I agree that this might be a useful framework in which to discuss
    further developments (variable instantiation is a lot more limited
    in our context, but we think about why and how to change that; 
    we need to reason in an open world, but at least theoretically, we
    can collect all instances; we don't have multiple solutions, but we
    do sometimes need to look at instances before knowing all variable
    instantiations, leaving us with multiple possible matches, so 
    approximation may be a useful alternative to full search for us, 
    rather than just the optimisation it is in the logic case).

any thoughts?-)

cheers,
claus