the MPTC Dilemma (please solve)

[Martin Sulzmann]

Manuel M T Chakravarty writes:
 > The big question is: do we really want to do logic programming over
 > types?  I'd say, no!

With ATs you're still doing logic programming if you like or not.

As Ross Paterson writes:
 > I agree that functions on static data are more attractive than logic
 > programming at the type level.  But with associated type synonyms,
 > the type level is not a functional language but a functional-logic one.

The point is here really that you may think you define
a type function, e.g.

type F [a] = [F a]

though, these type definitions behave more like relations,
cause (type) equations behave bi-directionally.


Manuel M T Chakravarty writes:
 > My statement remains:  Why use a relational notation if you can have a
 > functional one?

Because a relational notation is strictly stronger. 

Some time ago I asked the following:

Write the AT "equivalent" of the following FD program.

zip2 :: [a]->[b]->[(a,b)]
zip2 = ... -- standard zip
class Zip a b c | c->a, c->b where
 zip :: [a]->[b]->c
instance Zip a b [(a,b)] where                    -- (Z1)
 zip = zip2
instance Zip (a,b) c e => Zip a b ([c]->e) where  -- (Z2)
 zip as bs cs = zip (zip2 as bs) cs

Specifying the FD improvement conditions via AT type functions
is a highly non-trivial task.
Check out Section 2 in
[October 2005]  Associated Functional Dependencies 
http://www.comp.nus.edu.sg/~sulzmann/
for the answer.

Sure, ATs provide a nice syntax for a specific kind of type class
programs.  Though, as I've pointed out before any AT program can be
encoded with FDs but the other direction does not hold necessarily.
See the above paper for details.


Manuel M T Chakravarty writes:
 > > ------------------------------------------------------------
 > > From: Martin Sulzmann <sulzmann at comp.nus.edu.sg>
 > > Subject: MPTC/FD dilemma 
 > > 
 > > - ATs (associated types) will pose the same challenges.
 > >   That is, type inference relies on dynamic termination checks.
 > 
 > Can you give an example?


There's nothing wrong with ATs as described in the ICFP'05 paper.
The problem is that some "simple" extension easily lead to undecidable
type inference.

Recall the following discussion:
http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html

The point here is really that type inference for ATs and FDs is
an equally hard problem:
http://www.haskell.org//pipermail/haskell-cafe/2006-February/014680.html


Another thing, here's an excerpt of the current summary of the MPTC
dilemma from
http://haskell.galois.com/cgi-bin/haskell-prime/trac.cgi/wiki


Multi Parameter Type Classes Dilemma ¦

    Options for solving the dilemma ¦   
        2. Put AssociatedTypes on the fast-track for sainthood

Associated Types ¦

   Cons ¦   
    * Only a prototype implementation so far 

This is a *inaccurate* and highly *misleading* summary.

Without some formal argument you cannot simply say that ATs are
"better" than FDs. In some situations, ATs may have a better syntax
than FDs. Though, this is a matter of taste. More seriously, ATs
require the programmer to write *all* improvement rules
explicitly. This can be a fairly challenging task. See the above "zip"
example.

I understand that you want to push ATs. It's a good thing to seek
for alternatives. But typing and translating ATs is as challenging
as typing and translating FDs (I've left out the translation issue,
cause this leads to far here).

Martin