the MPTC Dilemma (please solve)
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Tue Mar 21 18:56:18 EST 2006
> 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
> for the answer.
Well, this is one of these nice FD puzzles. With ATs it's still a
> > > - 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
> 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.
More information about the Haskell-prime