Re: Re[2]: the MPTC Dilemma (please solve)

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