termination for FDs and ATs

[Manuel M T Chakravarty]

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 addresses the first point.  You didn't address the second.  let me
re-formuate: I think, you got the derivation wrong.  You use the
superclass implication the wrong way around.  (Or do I misunderstand?)

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

You may be able to encode AT proofs into FD proofs and vice versa, but
that doesn't change the fact that some issues, as for example formation
rules, are more natural, and I argue, more intuitive to the programmer
in the AT setting.  For example, with FDs you have to explain to the
programmer the concept of weak coverage.  With ATs, you don't need to do
this, because the functional notation naturally leads people to write
programs that obey weak coverage.  Again, we want to write functional
programs on the type level - after all FDs are *functional* dependencies
- so, why use a relational notation?  

If, as you say, FDs and ATs are equivalent on some scale of type
theoretic power, let us use a functional notation in a functional
language.  At least, that is more orthogonal language design.

Manuel