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