alternative translation of type classes to CHR (was: relaxed instance rules spec)

[Claus Reinke]

>.. 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