.. 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 inference and 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 by unification 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 for the 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 the declarations 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