the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

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.

If you insist, we are doing functional logic programming, but using a
model that is extremely close to what Haskell does on the value level
already.  (See Ross Paterson's email and my response.)

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

I disagree.  Associated type synonyms are similar to uni-directional
functional dependencies.  (Associated data types are similar to
bi-directional FDs.)  If you are familiar with the evaluation models of
functional logic programming languages, associated type synonyms do not
behave like functions under a narrowing strategy, but like functions
under a residuation strategy.

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

That's the same argument that the logic programming community has used
for ages to convince us that we should do logic programming, not
functional programming.  I don't buy it.  It doesn't even hold on a
theoretical level, relations can be seen as Boolean-valued functions.
And as far as the pragmatics of programming goes, well, we are
discussing the standardisation of a functional language, don't we.

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

Well, this is one of these nice FD puzzles.  With ATs it's still a
puzzle.  Fine.

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

I am happy to hear that.

> The problem is that some "simple" extension easily lead to undecidable
> type inference.

That's true for about anything in Haskell's type system these days.


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

I didn't write that wiki page plus you are citing individual sentences
out of a larger text.

Manuel