termination for FDs and ATs

[Manuel M T Chakravarty]

Iavor Diatchki:
> On 4/29/06, Manuel M T Chakravarty <chak at cse.unsw.edu.au> wrote:
> >         instance Mul a b => Mul a [b] where
> >                 type Result a [b] = [Result a b]   -- second argument is different
> >                 x .*. ys = map (x .*.) ys
> >
> > The arguments to the ATs, in an instance def, need to coincide with the
> > class parameters.
> >
> > So, in f, we get the context
> >
> >   Mul a [b], Result a [b] = b                       (*)
> >
> > which reduces to
> >
> >   Mul a b, [Result a b] = b
> >
> > at which point type inference *terminates*.
> 
> Perhaps I misunderstand something, but terminating is not always an
> option.  For example, if we are type checking something with a type
> signature, or an expression where the monomorphism restriction kicks
> in, we have to discharge the predicates or reject the program.  (This
> is why the example on the wiki is written with lambdas).

If we require a monomorphic signature at this point, we will reject the
program, as the inferred signature quantifies over two type variables.

> > So, we get the following type for f
> >
> >   f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b]
> >
> > Given the instance definitions of that example, you can never satisfy
> > the equality [Result a b] = b, and hence, never apply the function f.
> 
> What do you think should happen if I add the following definition as well?
> 
> g :: (Mul a b) => Bool -> a -> b -> [Result a b]
> g = f
> 
> It appears that the "right" thing would be to reject this program,
> because we cannot solve the constraint "[Result a b] = b".  However,
> in general this may require some fancy reasoning, which is why naive
> implementations simply loop.

The definition of g will indeed be rejected.  However, no fancy
reasoning is required.  Section 5.4 of the Associated Type Synonyms
paper defines polytype subsumption for signatures including associated
types.  Subsumption is the standard way of determining whether a type
signature is valid.  (To cover this point, the term syntax in the
Associated Type Synonym paper, Figure 1, includes signature
annotations.)

> > So, clearly termination for ATs and FDs is *not* the same.
> I assume (appologies if this is incorrect) that when you are talking
> about termintion of ATs or FDs you mean the terminations of particular
> algorithms for solving predicates arising in both systems.  

You are of course right.  I admit that I am guilty of the same
imprecision as most of the contributions to the AT-FD discussion.  We
are talking of ATs and FDs as if there is only one system each, although
there are two families of systems.

> I am not
> sure if ATs somehow make the problem simpler, but certainly choosing
> to delay predicates rather than solve them is an option available to
> both systems (modulo type signatures, as I mentioned above).

Let's say I have never seen a proposal for FDs that delays predicates in
the way that we proposed for ATs.  One nice property of the system
proposed for ATs is that it arises form a generalisation of the occurs
check that we have to do in Hindley-Milner type inference anyway.  I
suspect that for FDs you have to invoke some extra machinery.

Manuel