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 _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
