[Haskell-cafe] Re: Associated Type Synonyms question
Martin Sulzmann
sulzmann at comp.nus.edu.sg
Tue Feb 21 02:43:09 EST 2006
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
More information about the Haskell-Cafe
mailing list