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
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
