[Haskell-cafe] Re: Associated Type Synonyms question

21 Feb 2006

      Stefan Wehr writes:
...
Martin Sulzmann  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