[Haskell-cafe] Re: Associated Type Synonyms question

[Martin Sulzmann]

Stefan Wehr writes:
 > Martin Sulzmann <sulzmann at comp.nus.edu.sg> wrote::
 > 
 > > Stefan Wehr writes:
 > > > [...]
 > > > Manuel (Chakravarty) and I agree that it should be possible to
 > > > constrain associated type synonyms in the context of class
 > > > definitions. Your example shows that this feature is actually
 > > > needed. I will integrate it into phrac within the next few days.
 > > > 
 > >
 > > By possible you mean this extension won't break any
 > > of the existing ATS inference results?
 > 
 > Yes, although we didn't go through all the proofs.
 > 
 > > You have to be very careful otherwise you'll loose decidability.
 > 
 > Do you have something concrete in mind or is this a more general
 > advice?
 > 

I'm afraid, I think there's a real issue.
Here's the AT version of Example 15 from "Understanding FDs via CHRs"

  class D a
  class F a where
   type T a
  instance F [a] where
   type T [a] = [[a]]           
  instance (D (T a), F a) => D [a]
            ^^^^^^^
    type function appears in type class

Type inference (i.e. constraint solving) for D [a] will not terminate.
Roughly,

                  D [[a]]
-->_instance      D (T [a]), F [a])
-->_type function D [[a]], F [a]
and so on

Will this also happen if type functions appear in superclasses?
Let's see. Consider

 class C a
 class F a where
   type T a
 instance F [a] where
   type T [a] = [[[a]]]
 class C (T a) => D a
         ^^^^^
    type function appears in superclass context
 instance D [a] => C [[a]] -- satisfies Ross Paterson's Termination Conditions

Consider

                  D [a]
-->_superclass    C (T [a]), D [a]
-->_type function C [[[a]]], D [a]
-->_instance      D [[a]], D [a]
and so on


My point:

- The type functions are obviously terminating, e.g.
  type T [a] = [[a]] clearly terminates.
- It's the devious interaction between instances/superclasss
  and type function which causes the type class program
  not to terminate.


Is there a possible fix? Here's a guess.

For each type definition in the AT case

type T t1 = t2

(or improvement rule in the FD case

rule T1 t1 a ==> a=t2

BTW, any sufficient restriction which applies to the FD
case can be lifted to the AT case and vice versa!)

we demand that the number of constructors in t2
is strictly smaller than the in t1
(plus some of the other usual definitions).
Then,

type T [a] = [[a]]

although terminating, is not legal anymore.

Then, there might be some hope to recover termination
(I've briefly sketched a proof and termination may
indeed hold but I'm not 100% convinced yet).

Martin