termination for FDs and ATs
sulzmann at comp.nus.edu.sg
Fri May 5 01:58:04 EDT 2006
Manuel M T Chakravarty writes:
> 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?)
Superclass implication is reversed when performing type inference.
In the same way that instance reduction is reserved.
Here's the example again.
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
-->_superclass C (T [a]), D [a]
-->_type function C [[[a]]], D [a]
-->_instance D [[a]], D [a]
and so on
Of course, you'll argue that you apply some other inference methods.
Though, I'm a bit doubtful whether you'll achieve any reasonably
strong completeness of inference results.
> > > 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.
More information about the Haskell-prime