termination for FDs and ATs

[Martin Sulzmann]

Manuel M T Chakravarty writes:
 > Martin Sulzmann:
 > > A problem with ATs at the moment is that some terminating FD programs
 > > result into non-terminating AT programs.
 > > 
 > > Somebody asked how to write the MonadReader class with ATs:
 > > http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html
 > >
 > > This requires an AT extension which may lead to undecidable type
 > > inference:
 > > http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html
 > 
 > The message that you are citing here has two problems:
 > 
 >      1. You are using non-standard instances with contexts containing
 >         non-variable predicates.  (I am not disputing the potential
 >         merit of these, but we don't know whether they apply to Haskell'
 >         at this point.)
 >      2. You seem to use the super class implication the wrong way around
 >         (ie, as if it were an instance implication).  See Rule (cls) of
 >         Fig 3 of the "Associated Type Synonyms" paper.
 > 

I'm not arguing that the conditions in the published AT papers result
in programs for which inference is non-terminating.

We're discussing here a possible AT extension for which inference
is clearly non-terminating (unless we cut off type inference after n
number of steps). Without these extensions you can't adequately
encode the MonadReader class with ATs.


 > This plus the points that I mentioned in my previous two posts in this
 > thread leave me highly unconvinced of your claims comparing AT and FD
 > termination.
 > 

As argued earlier by others, we can apply the same 'tricks' to make
FD inference terminating (but then we still don't know whether
the constraint store is consistent!).

To obtain termination of type class inference, we'll need to be *very*
careful that there's no 'devious' interaction between instances and
type functions/improvement. 

It would be great if you could come up with an improved analysis which
rejects potentially non-terminating AT programs. Though, note that
I should immediately be able to transfer your results to the FD
setting based on the following observation:

I can turn any AT proof into a FD proof by (roughly)

 - replace the AT equation F a=b with the FD constraint F a b
 - instead of firing type functions, we fire type improvement and
   instances
 - instead of applying transitivity, we apply the FD
   rule F a b, F a c ==> b=c

Similarly, we can turn any FD proof into a AT proof.

Martin