alternative translation of type classes to CHR (was: relaxed
instance rules spec)
Claus Reinke
claus.reinke at talk21.com
Mon Mar 6 08:24:58 EST 2006
>.. 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Tc2CHR.hs
Type: application/octet-stream
Size: 5867 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell-prime/attachments/20060306/00503223/Tc2CHR.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: MainTc2CHR.hs
Type: application/octet-stream
Size: 83 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell-prime/attachments/20060306/00503223/MainTc2CHR.obj
More information about the Haskell-prime
mailing list