.. the translation also needs to account for FD-related information taken from the instance declarations.
actually, since we've already accounted for the two roles of inferenceand FD by splitting the constraints, this might be as simple as merging the instance and instance-improvement CHRs in the original translation (variation A). alternatively, we can make sure that instances generate memo constraints as well (variation B).
this email is somewhat long, but might serve as a synchronisation point for those who feel a bit lost in the flood of emails and information fragments (at least as far as the new subject line is concerned:-).
as some of you seem to be less than enthusiastic about my suggested modifications, I'd like to give you something concrete to attack,-) so here goes the first attempt (cf Fig. 2, p13, in the FD-CHR paper):
============= Tc2CHR alternative, with separated roles
class C => TC a1..an | fd1,..,fdm
where fdi is of the form: ai1..aik -> ai0
-> TC a b <=> infer_TC a b, memo_TC a b. (two roles)
-> memo_TC a1..an, memo_TC th(b1)..th(bn) => ai0=bi0. (fdi)
where th(bij) | j>0 = aij
th(bl) | not (exists j>0. l==ij) = bl
============= Variation A (merge instance inference/propagation):
instance C => TC t1..tn
-> infer_TC th(b1)..th(bn) <=> c1,..,cn, C. (instance
inference/improvement)
where th(bl) | exists i. l==i0 = bl
th(bl) | otherwise = tl
cl | exists i. l==i0 = bl=tl
cl | otherwise = true
-> [only needed for non-full FDs?]
memo_TC th(b1)..th(bn) ==> c1,..,cn. (non-full FDi instance
improvement)
where th(bl) | exists i,j>0. l==ij = tl
th(bl) | otherwise = bl
cl | exists i. l==i0 = (bl=tl)
cl | otherwise = true
============= Variation B (separately record instance FD info):
instance C => TC t1..tn
-> infer_TC t1..tn <=> C. (instance inference)
-> fact ==> memo_TC th(b1)..th(bn). (FDi instance info)
where th(bl) | exists j. l==ij = tl
th(bl) | otherwise = bl
=============================================
in case I messed up the formalization, here are the ideas again:
- each constraint arising during instance inference or given as a goal
needs to be proven (reduced to true). we account for that with the
infer_X constraints and their rules.
- for each constraint used in the instance inference process, each
class FD implies a functional dependency between the concrete
types in that constraint, which has to be consistent accross all
constraints. we account for that with the memo_X constraints
(gathering FD info) and their rules (using FD info).
- the CHR succeeds if there are no infer constraints left. Variation A: - for each instance declaration, each class FDi implies that the type in its range (ti0) is a function of the types in its domain (ti1..tik). we account for that by replacing the range types in the head of the instance inference CHR with variables, which are bound byunification in the body of the CHR.
- for non-full FDs, there may be instances with non-variable types in non-FD positions, in which case the combined inference/ improvement rules won't fully express the FDs. we account for these cases by a separate instance improvement rule. Variation B: - the instance CHRs only account for instance inference - for each instance/FD, we need to generate extra FD-related information (for technical reasons, those propagation rules are triggered by the trivial constraint fact, rather than true, as one might expect; so queries have to be "fact,query", see examples at the end) the main differences to the original translation are: - separating constraint roles should aid confluence, as the memory of constraints remains even after their inference has started (this should also make it easier to relax constraints later, and to focus on their effect on termination rather than confluence)- separating constraint roles allows merging of instance inference and improvement rules, further avoiding conflicts/orderings between these two stages (variation A; this should make it easier to discuss extensions later, such as interaction of FDs with overlapping resolution, where both features have to be taken into account for instance selection)
I'd like to get variation A working, but in case that merging instance inference and propagation should turn out to be impossible for some reason, I include the less adventurous variation B, which still reflects the splitting of roles/improved
confluence aspect. for those who like to experiment, to get a better feeling forthe translation, by-hand translation soon gets tedious, so I attach a TH-based naive implemenation of variation B. it is
naive, so expect problems, but it is also simple, so feel free to suggest patches;-) (*) it is quite likely that I missed something, but I hope this is concrete enough so that you can express your concerns concretely as well (e.g., Ross: which properties do you fear would be lost by this?). cheers, claus (*) load MainTc2CHR into ghci -fglasgow-exts, run: toFile; this creates a file i.chr, representing the translation of thedeclarations in Tc2CHR.i . then start up SWI Prolog, load the i.chr module, and explore the CHRs:
--------------------i = [d| class C a b | a -> b
instance C Int Bool
class D a b c | a -> c where d :: a -> b -> c
instance C a b => D a b c where d a b = undefined
instance D Int Bool Bool where d a b = undefined
|]
--------------------
2 ?- consult('i.chr').
..
3 ?- fact,d(int,int,bool).
No
4 ?- fact,d(int,bool,bool).
fact
memo_c(int, bool)
memo_d(int, bool, bool)
memo_d(int, _G44169, bool)
memo_d(_G43789, _G43790, _G43791)
<-- only fact and memo_ constraints left, indicating success
Yes
5 ?- fact,d(A,B,C).
fact
infer_c(_G43323, _G43324) <---- unresolved infer constraint
memo_c(_G43323, _G43324)
memo_c(int, bool)
memo_d(_G43323, _G43324, _G43325)
memo_d(int, _G44166, bool)
memo_d(_G43786, _G43787, _G43788)
A = _G43323{i = ...}
B = _G43324{i = ...}
C = _G43325{i = ...} ; <--- conditional success, corresponding to
ghc's error messages with
suggested fix:
"add instance for C _G43323
_G43324"
No
6 ?- fact,d(int,B,C).
fact
memo_c(int, bool)
memo_d(int, bool, bool)
memo_d(int, _G44163, bool)
memo_d(_G43783, _G43784, _G43785)
B = bool <-- determined by superclass fd
C = bool ; <-- determined by class fd
No
Tc2CHR.hs
Description: Binary data
MainTc2CHR.hs
Description: Binary data
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
