here's my take on this (disclaimer: I've got a bit of experience in type-class-level programming, but I'm not an expert in type systems;). Isaac pinned the problem to MPTCs and FDs, because the former are closely connected to when people started noticing the problem, and the latter are intended as a partial solution. the dilemma, as far as standardization is concerned, is that there are several variants of FDs, and their interaction with other features, and that there is no clear optimum in the design space yet (ghc isn't doing too badly in its pragmatic way, but for a standard, one would prefer a consistent story). however, the underlying problem is not limited to MPTCs, and FDs are not the only attempt to tackle the problem. so I agree with Isaac: getting a handle on this issue is imperative for Haskell', because it will be the only way forward when trying to standardize at least those of the many extensions that have been around longer than the previous standard Haskell 98. and if Haskell' fails to do this, it fails. to understand my reason for this strong opinion, it is necessary to understand that the problem underlying this dilemma not limited to some optional extensions one might continue to ignore, but instead is part of almost all advanced type-class programming - I'll try to illustrate with one example. first, here's a stripped down example of (label-type-based) selection of fields from records (as nested tuples): -- | field selection infixl #? class Select label val rec | label rec -> val where (#?) :: rec -> label -> val instance Select label val ((label,val),r) where ((_,val),_) #? label = val instance Select label val r => Select label val (l,r) where (_,r) #? label = r #? label -- examples data A = A deriving Show data B = B deriving Show data C = C deriving Show data D = D deriving Show r1 = ((A,True),((B,'a'),((C,1),((D,"hi there"),((B,["who's calling"]),()))))) the intention is to select the first field with a matching type of label (question: is this intention expressed in the code? how?). this code loads and works, with ghci-6.4.1 (and -fglasgow-exts, -fallow-overlapping-instances), and I can select the first B field like this: *Main> r1 #? B 'a' the same code does *not even load* with Hugs 98 (Nov 2003) +98 (more recent releases seem to have left out the windows platform): Hugs mode: Restart with command line option +98 for Haskell 98 mode ERROR "C:\Documents and Settings\cr3\Desktop\haskell\haskell prime\Dilemma.hs":1 0 - Instances are not consistent with dependencies *** This instance : Select a b (c,d) *** Conflicts with : Select a b ((a,b),c) *** For class : Select a b c *** Under dependency : a c -> b this demonstrates the dilemma, and I hope it also shows why I want these extensions standardized, at the very least as an addendum defining all the options out there in current use. this is not about saying that every implementation has to support FDs, but about clarifying what is supported. we can modify the example a bit, to get to the underlying problem. here's a Select', without the functional dependency: -- | field selection infixl #. class Select' label val rec where (#.) :: rec -> label -> val instance Select' label val ((label,val),r) where ((_,val),_) #. label = val instance Select' label val r => Select' label val (l,r) where (_,r) #. label = r #. label now this loads in both ghci and hugs, but it doesn't quite work to our satisfaction: Main> r1 #. B ERROR - Unresolved overloading *** Type : Select' B a () => a *** Expression : r1 #. B *Main> r1 #. B <interactive>:1:3: Overlapping instances for Select' B val ((B, Char), ((C, Integer), ((D, [Char]), ((B, [[Char]]), ())))) arising from use of `#.' at <interactive>:1:3-4 Matching instances: Dilemma.hs:10:0: instance (Select' label val r) => Select' label val (l, r) Dilemma.hs:7:0: instance Select' label val ((label, val), r) (The choice depends on the instantiation of `val' Use -fallow-incoherent-instances to use the first choice above) In the definition of `it': it = r1 #. B note, btw, that ghci offers a dangerous-sounding workaround, for the adventurous, but this isn't actually going to help, because it only offers to default to the recursive instance, soon running out of record to select from (and no reordering of source-code seems to affect that choice): *Main> :set -fallow-incoherent-instances *Main> r1 #. B <interactive>:1:3: No instance for (Select' B val ()) arising from use of `#.' at <interactive>:1:3-4 Probable fix: add an instance declaration for (Select' B val ()) In the definition of `it': it = r1 #. B back to the problem: there are multiple instances matching the context required to fulfill our selection request, and since the choice of instance might affect the program result, neither implementation is willing to commit to one of the choices (unless explicitly encouraged by a daring option;). so far, so good. we can resolve the ambiguity with a type annotation: Main> r1 #. B ::Char 'a' *Main> r1 #. B::Char 'a' everybody happy? not at all! recall our original FD: we wanted the result to be dependent on the field selected, not the field selection dependent on the result requested! Main> r1 #. B ::[String] ["who's calling"] *Main> r1 #. B::[String] ["who's calling"] oops. if we go back to the original code (and hence ghci only), we get the error message we expected, because the first B field in r1 holds a Char value, not a [String]: *Main> r1 #? B::[String] Top level: Couldn't match `Char' against `[String]' Expected type: Char Inferred type: [String] When using functional dependencies to combine Select label val ((label, val), r), arising from the instance declaration at Dilemma.hs:20:0 Select B [String] ((B, Char), ((C, Integer), ((D, [Char]), ((B, [[Char]]), ())))), arising from use of `#?' at <interactive>:1:3-4 by now, you'll probably have an idea what the problem is (at least, the problem as I see it): selection from ambiguous instances, and committing to one of several choices. to hammer home the point that this is not specific to MPTCs, but inherent in complex type-class level programming, here's the ambiguous version again, without any MPTCs: class Select' t where (#.) :: t instance Select' (((label,val),r)->label->val) where ((_,val),_) #. label = val instance Select' (r->label->val) => Select' ((l,r)->label->val) where (_,r) #. label = r #. label this version loads fine into hugs, but not into ghci: *Main> :r Compiling Main ( Dilemma.hs, interpreted ) Dilemma.hs:10:0: Non-type variables in constraint: Select' (r -> label -> val) (Use -fallow-undecidable-instances to permit this) In the context: (Select' (r -> label -> val)) While checking the context of an instance declaration In the instance declaration for `Select' ((l, r) -> label -> val)' Failed, modules loaded: none. undecidable instances is ghc jargon for "i don't have to care what these instances look like. just don't blame me.". once we've signed that disclaimer, we get the same problems, without any MPTCs in sight: Main> r1 #. B ::Char 'a' Main> r1 #. B ::[String] ["who's calling"] *Main> r1 #. B::Char 'a' *Main> r1 #. B::[String] ["who's calling"] the reason that this problem starts to show up with MPTCs is that, with conventional limitations on instances in place, MPTCs were one of the first extensions that permitted multiple variables to be constrained by one type-class constraint. once those limitations are relaxed (as well they should be), there are other uses of type classes that exhibit the same issue. the reason that FDs are connected with this problem is that they are trying to address part of it, by allowing us to turn type-level relations (type-class constraints involving multiple types) into type-level functions, so that resolving only a subset of type variables in such a constraint will be sufficient to commit to an instance. so, once again, the problem is *selection from possibly ambiguous instances*, and *control over that selection*. and this problem seems to be inherent in type-class-level programming, with or without MPTCs or FDs. the problem is aggravated by the wish to support separate compilation of modules, because it means that the implementation can never know that there won't be another fitting instance just around the corner.. this leads to the slightly ridiculous situation that the implementation will sometimes not even select the one and only instance we ever intended to write. note that I said "possibly ambiguous", because, really, there shouldn't be any ambiguity in this case (and in many other cases). usually, it is just that Haskell (or the Haskell+ implementation at hand) does not give us the means to express our intentions in an unambiguous form. and that is not for not trying, either. to wit, have a look at some of the language features that have tried to address parts of the problem (or that have been proposed): - defaults (remember those?) - functional dependencies - "most-specific" rule in overlapping instances - incoherent instances (is the selection documented anywhere?) - closed classes (yes, dear compiler, you can see *all* instances) it may also be worth pointing out the one language feature that does *not* try to help with the problem: - ignoring contexts when deciding about overlaps because, often, the contexts establish mutually exclusive pre-conditions to those "overlapping" instances. so, this is a lot like ignoring guards when matching patterns.. and if we were able to specify negation of type predicates (the characteristic predicates of those type relations specified by MPTCs), avoiding overlaps by such constraints would be even easier. well, I could go on, but that's probably more than enough for now. thanks for reading with us, we hope you had an enjoyable trip!-) cheers, claus

I have to agree with Manuel. I write a lot of Haskell code. People even pay me to do it. I usually stay with Haskell-98, and I don't think it's a great hardship. Sure, there's fancy stuff I can't do then, but I'd much rather have a well understood somewhat less powerful language. I think the right way forward is more along the lines of associated type and type level functions rather than MPTC and FDs. -- Lennart Manuel M T Chakravarty wrote:

Claus Reinke:

...

however, the underlying problem is not limited to MPTCs, and FDs are not the only attempt to tackle the problem. so I agree with Isaac: getting a handle on this issue is imperative for Haskell', because it will be the only way forward when trying to standardize at least those of the many extensions that have been around longer than the previous standard Haskell 98. and if Haskell' fails to do this, it fails.

Please keep things in perspective:

(A) It's not as if every interesting program (or even the majority of interesting programs) use(s) MPTCs.

(B) I don't think the time for which an extension has been around is particularly relevant. One of the big selling points of Haskell is that it's quite well defined, and hence, its semantics is fairly well understood and sane - sure, there are dark corners, but compared to other languages of the same size, we are in good shape. If we include half-baked features, we weaken the standard.

In fact, it's quite worrying that FDs have been around for so long and still resisted a thorough understanding.

Manuel

_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime

Bulat Ziganshin:

Hello Lennart,

Sunday, March 19, 2006, 4:05:03 AM, you wrote:

LA> I have to agree with Manuel. I write a lot of Haskell code. LA> People even pay me to do it. I usually stay with Haskell-98,

when i wrote application code, i also don't used extensions very much, i even don't used Haskell-98 very much and afair don't defined any type classes at all

but when i gone to writing libraries, that can be used by everyone, type classes and requirement in even more extensions is what i need permanently. in particular, i try to write library so what any conception (stream, Binary, reference, array) can be used in any monad and that immediately leads me to using MPTC+FD. moreover, problems with resolving class overloading and other deficiencies of current unofficial Hugs/GHC standard are permanently strikes me

Libraries are a means, not an end. The fact still remains. Most programs don't need MPTCs in an essential way. It's convenient to have them, but they are not essential.

i had a class which defines "default" reference type for monads:

class Ref m r | m->r where newRef :: a -> m (r a) readRef :: r a -> m a writeRef :: r a -> a -> m ()

instance Ref IO IORef where ... instance Ref (ST s) (STRef s) where ...

this class allows to write monad-independent code, for example:

doit = do x <- newRef 0 a <- readRef x writeRef x (a+1) readRef x

can be runned in IO or ST monads, or in any monad derived from IO/ST (with appropriate instance Ref definitions). As you can see, even such small example require using FDs. [..]

this will allow to rewrite my Ref class as:

type Ref IO = IORef Ref (ST s) = STRef s

You are going in the right direction, but what you want here are associated types; i.e., you want type functions that are open and can be extended (in the same way as classes can be extended by adding new instances). Your example reads as follows with associated types: class Monad m => RefMonad m where type Ref m :: * -> * newRef :: a -> m (Ref m a) readRef :: Ref m a -> m a writeRef :: Ref m a -> a -> m () instance RefMonad IO where type Ref IO = IORef ... instance RefMonad (ST s) where type Ref (ST s) = STRef s ... My statement remains: Why use a relational notation if you can have a functional one? (The RefMonad class is btw very similar to a functor of ML's module system.[*]) See http://hackage.haskell.org/trac/haskell-prime/wiki/AssociatedTypes for more details on associated types. Manuel [*] Cf http://www.informatik.uni-freiburg.de/~wehr/diplom/

Bulat Ziganshin:

Sunday, March 19, 2006, 7:25:44 PM, you wrote:

...

...

i had a class which defines "default" reference type for monads:

class Ref m r | m->r where

to be exact,

class Ref m r | m->r, r->m where

...

...

newRef :: a -> m (r a) readRef :: r a -> m a writeRef :: r a -> a -> m ()

or even worser:

class Ref2 m r a | m a->r, r->m instance (Unboxed a) => Ref2 IO IOURef a instance (!Unboxed a) => Ref2 IO IORef a instance (Unboxed a) => Ref2 (ST s) (STURef s) a instance (!Unboxed a) => Ref2 (ST s) (STRef s) a

MMTC> My statement remains: Why use a relational notation if you can have a MMTC> functional one?

how about these examples?

Bidirectional FDs correspond to associated data types. I am not sure what you try to achieve with your Ref2 example. The dependency of r on a seems to be surious as you don't instantiate a in any of your instance declarations.

MMTC> class Monad m => RefMonad m where MMTC> type Ref m :: * -> *

can i use `Ref` as type function? for example:

data StrBuffer m = StrBuffer (Ref m Int) (Ref m String)

Yes, absolutely. Manuel

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

Manuel M T Chakravarty writes:

...

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.

This wasn't meant as a "personal attack". If you (or whoever wrote) feel offended, I'm sorry. Fact is: (risking that I repeat myself here) - When it comes to typing, FDs strictly subsume ATs. (FDs = as defined in the FD-CHR paper) FYI, the next Chameleon release will supports FDs and ATs, ATs are internally represented via FD-CHRs. - All the challenging inference problems encountered for FDs also apply to ATs (see my previous emails) - FD-CHRs describe improvement *and* instance, superclass rules. It's really the subtle interaction between improvement and instances that causes the problem. I also would like to point that none of the FD-CHR results are "recent". The FD-CHR paper was published in ESOP'04, that was two years ago. Since April 2004, there's an extended version available as a TR. Correct, a revised version will somewhen soon appear as a JFP paper. Martin

<Hand-waving-alert> However, the evaluation model is what is known as "residuation" in the FL community, which is essentially functional programming with logic variables and lenient evaluation (a la Id). As long as we only have strongly normalising functions, lenient evaluation and lazy evaluation coincide. So, for Haskell programmers, we are on familiar ground. </Hand-waving-alert>

now that is an interesting difference. but we don't need to change formalizations to achieve that - apart from the difficulty of comparing the different properties of ATS and FDs if the formalisms also differ, there is the issue of implementation. if, instead of requiring completely new tools, ATS can be explained and implemented as a restricted form of FDs, with nicer syntax, then the existing FD implementations can be used - no need to add yet another layer of complexity to the type system implementations. first, syntax. at the level of type-classes, we are dealing with a simple first-order language, so adding nested expressions via function calls does not change expressiveness - we can simply reserve the last class parameter for results, and allow that to be omitted in calls. nested expresssions "F (G x) => C x" can be flattend as "G x r,F r => C x", with an FD for G (x->r). next, semantics. (simplifying slightly,) the difference between narrowing and residuation is that the former may instantiate variables, the latter suspends decisions that depend on variable instantiations, so narrowing subsumes residuation. you do have semantic unification in ATS, so you do have unification as a special case. so if you really avoid variable instantiations in ATS, that means at least: - not having an explicit result parameter (ATS writes the result parameter as an associated type) - not permitting equations involving variable instantiations (ATS has equality constraints, but one must not be able to write G x = r, or else one gets explicit access to a variable to be instantiated with a result, which we could feed back as input into the semantic unification) - not permitting repeated variables in instance heads (otherwise one could define an instance implicitly needing unification, thereby circumventing the second restriction) [I don't recall seeing the last two restrictions in ATS papers; have I missed them? they may be implicit in the restricted subset of the language formalized, but they need to be made explicit if ATS are to be integrated into current Haskell] right so far? the first is the least of our worries: if we flatten nested calls, and do not permit any calls involving the result/ range parameter, there is no way to refer to the result/range parameters explicitly. if we also add the other two restrictions, the narrowing semantics will behave much like the residuation semantics (the only variables ever instantiated are range/result variables, and that only puts a type in place of the call). so it seems that one might use the existing machinery (both formalization/theory and implemenation) for ATS as well, just by adding flattening of nested calls plus restrictions that ensure a single, full FD per class, and no explicit references to result/range variables. does this make any sense?-) cheers, claus

On Mon, Mar 20, 2006 at 10:50:32AM -0000, Claus Reinke wrote:

you reply to a message that is about a month old. since then, every single example of FD "trickyness" presented here has been resolved (or have we missed some example?), and as far as I'm concerned, the remaining problems are due to feature interactions, and need a more systematic approach.

As understand it, you've proposed changes in context reduction to restore confluence: http://www.haskell.org//pipermail/haskell-prime/2006-March/000880.html (with subsequent minor corrections) What is your plan to deal with non-termination (e.g. examples 6 and 16 of the FD-CHR paper)?

Claus Reinke:

...

In fact, it's quite worrying that FDs have been around for so long and still resisted a thorough understanding.

they don't resist. but as long as progress is example-driven and scary stories about FDs supposedly being tricky and inherently non-under- standable are more popular than investigations of the issues, there won't be much progress. please don't contribute to that hype.

When I say hard to understand, I mean difficult to formalise. Maybe I have missed something, but AFAIK the recent Sulzmann et al. paper is the first to thoroughly investigate this. And even this paper doesn't really capture the interaction with all features of H98. For example, AFAIK the CHR formalisation doesn't consider higher kinds (ie, no constructor classes).

it is okay to advertize for your favourite features. in fact, I might agree with you that a functional type-class replacement would be more consistent, and would be a sensible aim for the future.

but current Haskell has type classes, and current practice does use MPTCs and FDs; and you don't do your own case any favours by trying to argue against others advertizing and investigating their's.

I don't care whether I do "my case" a favour. I am not a politician. There is only one reason that ATs exist: FDs have serious problems. Two serious problems have little to do with type theory. They are more like software engineering problems: I. One is nicely documented in http://www.osl.iu.edu/publications/prints/2003/comparing_generic_programming... II. The other one is that if you use FDs to define type-indexed types, you cannot make these abstract (ie, the representations leak into user code). For details, please see the "Lack of abstraction." subsubsection in Section 5 of http://www.cse.unsw.edu.au/~chak/papers/#assoc

you reply to a message that is about a month old.

That's what re-locating around half of the planet does to your email responsiveness...but the topic is still of interest and I got the impression that your position is still the same.

for instance, ATS should just be special syntax for a limited, but possibly sufficient and more tractable form of MPTCs/FDs, and as long as that isn't the case in practice because of limitations in current implementations or theory, we don't understand either feature set sufficiently well to make any decisions.

ATs are not about special syntax. Type checking with ATs doesn't not use "improvement", but rather a rewrite system on type terms interleaved with unification. This leads to similar effects, but seems to have slightly different properties. Actually, I think, much of our disagreement is due to a different idea of the purpose of a language standard. You appear to be happy to standardise a feature that may be replaced in the next standard. (At least, both of the "choices" you propose in your email include deprecating a feature in Haskell''.) I don't see that as an acceptable solution. A standard is about something that stays. That people can rely on. IMHO if we consider deprecating a feature in Haskell'' again, we should not include it in Haskell', but leave it as an optional extra that some systems may experimentally implement and some may not. Manuel

Aaron Denney:

On 2006-03-20, Manuel M T Chakravarty wrote:

...

IMHO if we consider deprecating a feature in Haskell'' again, we should not include it in Haskell', but leave it as an optional extra that some systems may experimentally implement and some may not.

Possibly true, but it still needs to be standardized so that it will work the same on different implementations.

It might be standardised as an add on to the language standard, instead of as part of the language standard. Manuel

For example, AFAIK the CHR formalisation doesn't consider higher kinds (ie, no constructor classes).

you're right about interactions in general. but do you think constructor classes specifically would pose any interaction problems with FDs?

I don't care whether I do "my case" a favour. I am not a politician. There is only one reason that ATs exist: FDs have serious problems.

you don't solve problems by creating new features from scratch, with a different theory/formalization to boot. you try to pinpoint the perceived problems in the old feature, then either transform it to avoid those problems, or demonstrate that such transformation is not possible. otherwise, you have the nasty problem of relating your new feature/theory to the old one to demonstrate that you've really improved matters.

Two serious problems have little to do with type theory. They are more like software engineering problems:

I. One is nicely documented in http://www.osl.iu.edu/publications/prints/2003/comparing_generic_programming...

that paper isn't bad as far as language comparisons go, but it focusses on a rather restricted problem, so I'm surprised that this was part of the motivation to launch ATS: to reduce the number of parameters in combined "concepts", we might as well associate types with each other, instead of types with instances. variant A: I never understood why parameters of a class declaration are limited to variables. the instance parameters just have to match the class parameters, so let's assume we didn't have that variables-only restriction. class Graph (g e v) where src :: e -> g e v -> v tgt :: e -> g e v -> v we associate edge and node types with a graph type by making them parameters, and extract them by matching. variant B: I've often wanted type destructors as well as constructors. would there be any problem with that? type Edge (g e v) = e type Vertex (g e v) = v class Graph g where src :: Edge g -> g -> Vertex g tgt :: Edge g -> g -> Vertex g variant C: the point the paper makes is not so much about the number of class parameters, but that the associations for concepts should not need to be repeated for every combined concept. and, indeed, they need not be class Edge g e | g -> e instance Edge (g e v) e class Vertex g v | g -> v instance Vertex (g e v) v class (Edge g e,Vertex g v) => Graph g where src :: e -> g -> v tgt :: e -> g -> v (this assumes scoped type variables; also, current GHC, contrary to its documentation, does not permit entirely FD-determined variables in superclass contexts) all three seem to offer possible solutions to the problem posed in that paper, don't they?

II. The other one is that if you use FDs to define type-indexed types, you cannot make these abstract (ie, the representations leak into user code). For details, please see the "Lack of abstraction." subsubsection in Section 5 of http://www.cse.unsw.edu.au/~chak/papers/#assoc

do they have to? if variant C above would not run into limitations of current implementations, it would seem to extend to cover ATS: class C a where type CT a instance C t0 where type CT t0 = t1 would translate to something like: class CT a t | a -> t instance CT t0 t1 class CT a t => CT a instance CT t0 t1 => C t0 as Martin pointed out when I first suggested this on haskell-cafe, this might lead to parallel recursions for classes C and their type associations CT, so perhaps one might only want to use this to hide the extra parameter from user code (similar to calling auxiliary functions with an initial value for an accumulator).

...

you reply to a message that is about a month old.

That's what re-locating around half of the planet does to your email responsiveness...but the topic is still of interest and I got the impression that your position is still the same.

definitely. I was just unsure how to react - if you really hadn't seen the messages of the last month, it would be better to let you catch up (perhaps via the mailing list archive). if you just took that message as the natural place to attach your contribution to, there's no need to wait.

ATs are not about special syntax. Type checking with ATs doesn't not use "improvement", but rather a rewrite system on type terms interleaved with unification. This leads to similar effects, but seems to have slightly different properties.

that's what I'm complaining about. if ATs were identified as a subset of FDs with better properties and nicer syntax, it would be easy to compare. unless you claim that the different formalization is essential to achieving the properties of ATs, it is just an unfortunate incidental difference. for instance, what would keep us from reserving the last class parameter as the range, and the rest as the domain of a single FD per class? then we could play the old Prolog game of translating expressions involving predicates of n-1 parameters into flat Prolog code involving predicates with n parameters.

Actually, I think, much of our disagreement is due to a different idea of the purpose of a language standard. You appear to be happy to standardise a feature that may be replaced in the next standard.

I'm pragmatic. Most of us thought the features in questions were well defined, and just needed to be written up. I still don't see why MPTCs or some form of FDs would necessarily be replaced, unless someone did the major overhaul of throwing out type classes and defining a functional replacement. So I'm arguing to standardize features that I think will have staying power. But others don't seem to be so sure, and there's no reason, nor any basis for deciding to disappoint either of us. I've always maintained that Haskell' needs to be modular (core + addenda).

I don't see that as an acceptable solution. A standard is about something that stays. That people can rely on.

the only things that stop changing are the things that are dead. and even those continue to be changed by their environment until they ultimately disintegrate. Haskell is very much alive. it would be a pity if we hadn't learned anything more by the time the next+1 standard gets written. reliability yes, stasis no. noone is still actively supporting Haskell 1.2, and I doubt Haskell 98 will stay on the menu for long if Haskell' is successfull. cheers, claus

...

you're right about interactions in general. but do you think constructor classes specifically would pose any interaction problems with FDs? You have to be more careful with unification in a higher-kinded setting. I am not sure how to do that with CHRs.

to quote from the ATS paper: "just like Jones, we only need first-order unification despite the presence of higher-kinded variables, as we require all applications of associated type synonyms to be saturated".

...

variant A: I never understood why parameters of a class declaration are limited to variables. the instance parameters just have to match the class parameters, so let's assume we didn't have that variables-only restriction.

class Graph (g e v) where src :: e -> g e v -> v tgt :: e -> g e v -> v

we associate edge and node types with a graph type by making them parameters, and extract them by matching.

The dependency seems to be lost here.

what dependency? the associated types have become parameters to the graph type, so the dependency of association is represented by structural inclusion (type constructors are really constructors, so even phantom types would still be visible in the type construct). any instances of this class would have to be for types matching the form (g e v), fixing the type parameters.

...

variant B: I've often wanted type destructors as well as constructors. would there be any problem with that?

type Edge (g e v) = e type Vertex (g e v) = v

class Graph g where src :: Edge g -> g -> Vertex g tgt :: Edge g -> g -> Vertex g

Also no dependency and you need higher-order matching, which in general is undecidable.

the dependency is still represented by the type parameters, as in the previous case. and is this any more higher-order than what we have with constructor classes anyway? here's an example implementation of the two destructors, using type classes with constructor instances: {-# OPTIONS_GHC -fglasgow-exts #-} import Data.Typeable data Graph e v = Graph e v class Edge g e | g -> e where edge :: g -> String instance Typeable e => Edge (g e v) e where edge g = show (typeOf (undefined::e)) class Vertex g v | g -> v where vertex :: g -> String instance Typeable v => Vertex (g e v) v where vertex g = show (typeOf (undefined::v)) [the Typeable is only there so that we can see at the value level that the type-level selection works] *Main> edge (Graph (1,1) 1) "(Integer,Integer)" *Main> vertex (Graph (1,1) 1) "Integer"

...

variant C: the point the paper makes is not so much about the number of class parameters, but that the associations for concepts should not need to be repeated for every combined concept. and, indeed, they need not be

class Edge g e | g -> e instance Edge (g e v) e class Vertex g v | g -> v instance Vertex (g e v) v

class (Edge g e,Vertex g v) => Graph g where src :: e -> g -> v tgt :: e -> g -> v

(this assumes scoped type variables; also, current GHC, contrary to its documentation, does not permit entirely FD-determined variables in superclass contexts)

You still need to get at the parameter somehow from a graph (for which you need an associated type).

oh, please! are you even reading what I write? as should be clear from running the parts of the code that GHC does accept (see above), FDs are quite capable of associating an edge type parameter with its graph.

...

all three seem to offer possible solutions to the problem posed in that paper, don't they?

Not really.

...

...

...

II. The other one is that if you use FDs to define type-indexed types, you cannot make these abstract (ie, the representations leak into user code). For details, please see the "Lack of abstraction." subsubsection in Section 5 of http://www.cse.unsw.edu.au/~chak/papers/#assoc

do they have to? if variant C above would not run into limitations of current implementations, it would seem to extend to cover ATS:

class C a where type CT a

instance C t0 where type CT t0 = t1

would translate to something like:

class CT a t | a -> t instance CT t0 t1

class CT a t => CT a instance CT t0 t1 => C t0

as Martin pointed out when I first suggested this on haskell-cafe, this might lead to parallel recursions for classes C and their type associations CT, so perhaps one might only want to use this to hide the extra parameter from user code (similar to calling auxiliary functions with an initial value for an accumulator).

That doesn't address that problem at all.

come again? CT expresses the type association for C. all of CT can remain on the library side, so the user only needs to see C, without the representation parameter. unless you do want to expose the representation, in which case you can export CT, too. the only remaining problem would be that the main implementations of FDs still seem to have problems with FD type signatures, so they permit keeping both type and associated type abstract f :: CT t at => at -> t but they don't allow you to pretend that you don't know the associated type when you know the type f :: CT Int at => at -> Int but as you point out yourself, that isn't inherent to FDs, and there are FD versions that permit both, so I see that as a bug/oversight in current implementations. without FDs, all type class inference assumed that types are input only. with FDs, some types (those in range of an FD) have become output of the inference process. the second f-signature above does not claim that f is polymorphic in at, it claims that at is determined by CT's FD. so representing at by a rigid, unconstrained, type variable, and then to complain that at is determined by the FD, is not helpful. it should be quite permissible to use a variable in a functional language, even if we already know its value! the question is how useful that would be to the purpose you state in your papers, as you'd really want the code of f to be independent of the representation type (abstract representation), only using methods of CT. but if the representation type is known via the type association/FD, the type checker will happily accept uses of the concrete type where the type variable at is mentioned.

...

for instance, what would keep us from reserving the last class parameter as the range, and the rest as the domain of a single FD per class? then we could play the old Prolog game of translating expressions involving predicates of n-1 parameters into flat Prolog code involving predicates with n parameters.

That would be a great thing to try if there was a simple formalisation of functional dependencies.

I thought the modified CHR translation we arrived at was rather simple (see thread "alternative translation of type classes to CHR"). any particular problems with that?

Who wants to throw out type classes?

anyone who argues against relational programming via characteristic predicates - type classes are all about predicate entailment, and we don't want that in a functional language. or don't you listen to your own propaganda?-) you have since relented a bit, and functional logic programming at the type level may now be acceptable to you. but you started out with rather extreme views;-) cheers, claus

...

class Graph (g e v) where src :: e -> g e v -> v tgt :: e -> g e v -> v

we associate edge and node types with a graph type by making them parameters, and extract them by matching.

If I understand correctly, this requires all graphs to be polymorphic in the types of edges and vertices. Thus, you cannot (easily) define a graph which provides, say, only boolean edges. Moreover, doesn't this require higher-order matching?

I've already answered the last question. as for polymorphism, all this requires is for a graph type parameterized by an edge and vertex type (just as the SML solution, which got full marks in this category, requires instantiations of the edge and vertex types in the graph structure). I already gave an example of a graph instantiated with (Int,Int) edges and Int vertices. see below for a translation of the ATC paper examples

...

variant B: I've often wanted type destructors as well as constructors. would there be any problem with that?

type Edge (g e v) = e type Vertex (g e v) = v

class Graph g where src :: Edge g -> g -> Vertex g tgt :: Edge g -> g -> Vertex g

This suffers from the same problems as the previous variant. It also looks a lot like a special form of associated types. Could the AT framework be extended to support a similar form of type synonyms (in effect, partial type functions outside of classes)?

it suffers as little as the previous variant. and it was meant to be a special form, showing that the full generality of ATs as a separate type class extension is not required to solve that paper's issue. and the translation from type functions to FDs or ATs is entirely syntactic, I think, so it would be nice to have in Haskell', as long as at least one of the two is included.

Would

instance Graph Int -- methods left undefined

be a type error here?

yes, of course. instances still have to be instances of classes. in variation A, the type error would be in the instance head, in variation B, it would be in the method types (although it could backpropagate to the head).

...

class Edge g e | g -> e instance Edge (g e v) e class Vertex g v | g -> v instance Vertex (g e v) v

class (Edge g e,Vertex g v) => Graph g where src :: e -> g -> v tgt :: e -> g -> v

(this assumes scoped type variables; also, current GHC, contrary to its documentation, does not permit entirely FD-determined variables in superclass contexts)

What are the types of src and tgt here? Is it

src, tgt :: (Edge g e, Vertex g v, Graph g) => e -> g -> v

yes.

This does not seem to be a real improvement to me and, in fact, seems quite counterintuitive.

Roman

you're free to your own opinions, of course!-) it is, however, probably as close as we can come within current Haskell, and the shifting of Edge/Vertex to the right of the '=>' is a purely syntactic transformation, even if it is a nice one. and as you can see from the implementation below (I had to move the class methods out of the class to circumvent GHC's current typing problem, so no method implementations, only the types), it is sufficient to address the problem in that survey paper, and accounting for graphs with specific types is no problem (direct translation from ATC paper examples): *Main> :t \e->src e (undefined::NbmGraph) \e->src e (undefined::NbmGraph) :: GE2 -> GV2 *Main> :t \e->src e (undefined::AdjGraph) \e->src e (undefined::AdjGraph) :: GE1 -> GV1 cheers, claus {-# OPTIONS_GHC -fglasgow-exts #-} class Edge g e | g -> e instance Edge (g e v) e class Vertex g v | g -> v instance Vertex (g e v) v class Graph g -- these should be class methods of Graph.. src, tgt :: (Edge g e,Vertex g v,Graph g) => e -> g -> v src = undefined tgt = undefined -- adjacency matrix data G1 e v = G1 [[v]] data GV1 = GV1 Int data GE1 = GE1 GV1 GV1 type AdjGraph = G1 GE1 GV1 -- type associations instance Graph AdjGraph -- neighbor map data FiniteMap a b data G2 e v = G2 (FiniteMap v v) data GV2 = GV2 Int data GE2 = GE2 GV2 GV2 type NbmGraph = G2 GE2 GV2 -- type associations instance Graph NbmGraph

Ah, I see. You are suggesting to introduce phantom type parameters to fake polymorphism for types which aren't really polymorphic. This might be acceptable as a temporary workaround but I don't think it is a good long-term solution. The ML implementation is not really comparable to this as instantiating structures is quite different from instantiating types.

if we could actually write the instance implementations, it would be easier to say whether this is an adequate approach. once the phantom types are connected to the actual types used in the implementation, I suspect this would be very similar to the use of structure sharing and signature inclusion in the ML implementation.

...

it is, however, probably as close as we can come within current Haskell, In what sense is this current Haskell?

ignoring accidental limitations in current implementations.

For this to work, you need at the very least to

a) allow FD-determined variables to appear only in the superclass contexts but not in the head of class declarations (not supported by GHC at the moment),

also in data declarations. reported as #714.

b) rely on scoped type variables (in a way which GHC doesn't support at the moment) and

GHC does scope type variables over classes and instances, amongst other things (as demonstrated in the version of Edge/Vertex with methods edge/ vertex). what do you suspect is missing?

c) provide a way to keep FD outputs abstract even when the inputs are known (not supported by GHC).

accidental limitation, as far as rejecting the type signatures is concerned, I think. but perhaps I'm missing something deep? (that would still not really be abstract, as I mentioned in my previous email; does the ATS implementation really manage to keep the result of the type function unknown, and how?)

do. This is not meant as a criticism of your (very interesting, IMO) approach - I agree that this is probably the best you can do with FDs. It's just that FDs simply seem to be a less than optimal mechanism for this kind of programming.

thanks. I'm not saying that ATS are a bad thing, either, just that once we have a proper basis on which to rid current FD implemenations of accidental limitations, we should be able to implement ATS as a syntax transformation. so, if something works with ATS, but not with FDs, that points to a weak area in our current understanding or implementation of FDs. I'd prefer to see the FD story cleaned up, rather than introducing a new alternative, but I do want the type functions one can build on top of either.

Also, it might be worth pointing out that even if all of the above worked, you still couldn't do

data VertexPair g = VP (Vertex g) (Vertex g) fstVertex :: Graph g => VertexPair g -> Vertex g fstVertex (VP v1 v2) = v1

fstVertex :: Graph g => VertexPair g -> Vertex g fstVertex (VP v1 v2) = v1

a variation of problem (a) above: contexts can introduce new, FD-bound variables only in type signatures at the moment, not in class or data declarations. data Vertex g v => VertexPair g v = VP v v fstVertex :: (Vertex g v, Graph g) => VertexPair g v -> v fstVertex (VP v1 v2) = v1 otherwise, we could omit the spurious v parameter, as we'd like to.

type Vertices g = [Vertex g]

a variation of problem (c) above type Vertices g = Vertex g v => [v] *Main> :t (undefined::Vertices g) (undefined::Vertices g) :: forall t g. (Vertex g t) => [t] is accepted, but leads to the 'rigid vs FD-range' error if used with a concrete graph type. cheers, claus

On Sat, Feb 18, 2006 at 12:26:36AM +0000, Ross Paterson wrote:

Martin Sulzmann writes:

...

Result2: Assuming we can guarantee termination, then type inference is complete if we can satisfy - the Bound Variable Condition, - the Weak Coverage Condition, - the Consistency Condition, and - and FDs are full. Effectively, the above says that type inference is sound, complete but semi-decidable. That is, we're complete if each each inference goal terminates.

I think that this is a little stronger than Theorem 2 from the paper, which assumes that the CHR derived from the instances is terminating. If termination is obtained via a depth limit (as in hugs -98 and ghc -fallow-undecidable-instances), it is conceivable that for a particular goal, one strategy might run into the limit and fail, while a different strategy might reach success in fewer steps.

Rereading, I see you mentioned dynamic termination checks, but not depth limits. Can you say a bit more about termination? It seems to be crucial for your proofs of confluence.

On Tue, Feb 21, 2006 at 03:50:52PM +0800, Martin Sulzmann wrote:

A depth limit is not enough. For confluence we need that *all* derivations for a particular goal terminate. Once we have confluence we get completeness of the inference checks.

So without a static test for termination (though just for this goal), we're still in the no-man's land between proof and counterexample. Reduction might be confluent, but we have no proof.

When I said "type class acrobats" I didn't mean to make fun of people like you who use type classes in a very skillfull way. Though, I tried (successfully :) ) to be provocactive. I agree with you there's a real need for unrestricted type class programming. After all, the Hindley/Milner subset of Haskell already allows us to write non-terminating, "buggy" programs. So, what's the differences if we allow for the same on the level of types!? The trouble I have with the current practice of type class programming is that it's not very principled (yes, I'm provocactive again). People learn how to write type class programs by observing the behavior of a specific implementation and sometimes the results are quite unexpected. I have been mentioning CHRs before as a very useful tool to study FDs. In fact, CHRs go way beyond FDs see "A Theory of Overloading". I claim that when it comes to unrestricted type class programming CHRs are the way to go. CHRs have a clean semantic meaning and precisely explain the meaning of type class programs. Martin Claus Reinke writes:

...

I'm forwarding an email that Martin Sulzmann asked me to post on his behalf.

thanks. well, that is one view of things. but it is certainly not the only one.

first, about those "acrobatics": my type-class-level programs tend to start out as straightforward logic programs over types - no acrobatics involved, easy to understand. the acrobatics start when I'm trying to fit those straightforward programs into the straightjackets imposed by current systems - be they explicit restrictions or accidental limitations. wrestling them leads to the need to introduce complex work-arounds and implementation-specific tricks into the formerly clean logic programs.

the restrictions tend to be artificial and full of odd corners, rather than smooth or natural, and the limitations tend to be the result of not thinking the problem through. so one could say that neither of the levels proposed by Martin is ready for standardization. or, one could be pragmatic and standardize both levels, well knowing that neither is going to be the final word.

second, about the proposal to "ignore overlapping instances for the moment": that moment has long passed - iirc, undecidable and overlapping instances have been around for longer than the current standard Haskell 98. they provide recursion and conditionals (via best-match pattern-matching) for logic programming over types. they are overdue for inclusion in the standard, and it is time to stop closing our eyes to this fact.

third, understanding FDs via CHRs is very nice, and a good start that I hope to see expanded on rather sooner than later. but (a) there is a big discrepancy between the language studied there and current practice, so this work will have to catch on before it can be applied; and (b) the main issue with unconstrained type-class- level programming is not that it tackles a semi-decidable problem.

in fact, the usual Prolog system only provides an _incomplete_ implementation of almost the same semi-decidable problem. but it provides a well-defined and predictable implementation, so programmers can live with that (with a few well-known exceptions).

the two problems are not quite the same, because we extract programs from type-class-level proofs. so not only do we need the result to be uniquely determined (coherence), we also need the proof to be un-ambiguous (or we might get different programs depending on the proof variant chosen).

but, and this is an important "but": trying to restrict the permissable programs so that neither incoherence nor ambiguity can arise in the first place is only _one_ way to tackle the issue; the other direction that needs to be explored is to give programmers control enough to disambiguate and to restore coherence where needed.

so, I am quite happy with splitting the bigger problem into two levels: restrictive programs corresponding to the current state of art in formal studies of the problem, and unconstrained programs catering for the current state of art in programming practice. just as long as both levels are included in the standard, and both levels receive the further attention they need.

as far as I understand, this should not pose a problem for implementors, as they usually implement the simpler unconstrained variant first, then add restrictions to conform to the standard.

cheers, claus

...

- There's a class of MPTC/FD programs which enjoy sound, complete and decidable type inference. See Result 1 below. I believe that hugs and ghc faithfully implement this class. Unfortunately, for advanced type class acrobats this class of programs is too restrictive.

- There's a more expressive class of MPTC/FD programs which enjoy sound and complete type inference if we can guarantee termination by for example imposing a dynamic check. See Result 2 below. Again, I believe that hugs and ghc faithfully implement this class if they additionally implement a dynamic termination check. Most type class acrobats should be happy with this class I believe.

Let's take a look at the combination of FDs and "well-behaved" instances. By well-behaved instances I mean instances which are non-overlapping and terminating. From now on I will assume that instances must be well-behaved. The (maybe) surprising observation is that the combination of FDs and well-behaved instances easily breaks completeness and decidability of type inference. Well, all this is well-studied. Check out [February 2006] Understanding Functional Dependencies via Constraint Handling Rules by Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones and Peter J. Stuckey which is available via my home-page.

Here's a short summary of the results in the paper:

Result 1: To obtain sound (we always have that), complete and decidable type inference we need to impose - the Basic Conditions (see Sect4) (we can replace the Basic Conditions by any conditions which guarantees that instances are well-behaved. I'm ignoring here super classes for simplicity) - Jones's FD restrictions and the Bound Variable Condition (see Sect4.1)

The trouble is that these restrictions are quite "severe". In fact, there's not much hope to improve on these results. See the discussion in Sect5.1-5.3.

Let's take a look at a simple example to understand the gist of the problem.

Ex: Consider

class F a b | a->b instance F a b => F [a] [b] -- (F)

Assume some program text generates the constraint F [a] a. Type inference will improve a to [b] (because of the functional dependency in connection with the instance). Though, then we'll find the constraint F [[b]] [b] which can be resolved by the instance to F [b] b. But this is a renamed copy of the original constraint hence, type inference will not terminate here.

If we translate the instance and improvement conditions of the above program to CHRs the problem becomes obvious.

rule F a b, F a c ==> b=c -- the FD rule rule F [a] [a] <==> F a b -- the instance rule rule F [a] c ==> c=[b] -- the improvement rule

The rules should be read from left to right where "==>" stands for propagation and "<==>" for simplification.

My point: The above improvement rule is (potentially) dangerous cause we introduce a fresh variable b. And that's why type inference may not terminate. Using the terminology from the paper. The instance (F) violates one of Jones' FD restriction (the Coverage Condition).

So, is all lost? Not quite. A second major result in the paper says that if we can guarantee termination then we can guarantee completeness. Of course, we need to find some appropriate replacement for Jones' FD restrictions.

Result2: Assuming we can guarantee termination, then type inference is complete if we can satisfy - the Bound Variable Condition, - the Weak Coverage Condition, - the Consistency Condition, and - and FDs are full. Effectively, the above says that type inference is sound, complete but semi-decidable. That is, we're complete if each each inference goal terminates.

Here's a short explanation of the conditions. The Bound Variable Condition says that all variables which appear in the instance head must appear in the instance body. Weak Coverage says that any of the "unbound" variables (see b in the above example) must be captured by a FD in the instance context. This sounds complicated but is fairly simple. Please see the paper. Consistency says that for any FD and any two instances the improvement rules generated must be consistent. In fact, because we assume that FDs are full and instances are well-behaved (i.e. instances are non-overlapping) the Consistency Condition is always satisfied here. So, why did I mention Consistency then? Well, Theorem 2 in the paper from which Result2 is derived is stated in very general terms. We only assume that instances are terminating and confluent. Hence, we could (eventually) extend Result2 to overlapping instances and *then* Consistency becomes important (But PLEASE let's ignore overlapping instances for the moment). Okay, let's consider the last condition. We say a FD is full if all class parameters either appear in the domain or range of a FD. For example, class F a b c | a -> b is not full but class F a b c | a b -> c is full

Again, if we leave out any of the above conditions, we loose completeness.

Result2 covers in my opinion a rich class of FD programs. In my experience, the fullness condition is not a problem. (In some situations, we can transform a non-full into a full program but I'd rather reject non-full FDs). We could even drop the Bound Variable Condition and check for this condition "locally", similar to the way we check for termination now locally.

Somebody might ask, will ATs (associated types) behave any better? Unfortunately not, they share the same problem as FDs. AT type inference has the potential to become undecidable and incomplete.

Here's the above example re-casted in AT terms.

class F a where type T a instance F a => F [a] type T [a] = [T a]

Assume some program text generates the constraint T [b] = b. Naively, we could apply the above type definition which results in [T [b]] = b etc (T [b] = [T b] and T [b] = b leads to [T b] = b which leads to [T [T b]] = b) Though, the current AT description rejects the constraint T [b] = b right away. AT applies the occurs check rule. Clearly, b in fv(T [b]).

Important point to note: The occurs check is a "dynamic" check. We could impose a similar check on FDs. E.g. the type class constraint F [a] a contains a cycle. Hence, we should immediately reject this constraint. Of course, cycles may span across several constraints/type equations. For example, consider F [a] b, F [b] a and T [a]=b, T [b]=a.

Probably, more could be said but I'll stop here.

Martin

_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime

---

Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime

Claus Reinke:

...

I'm forwarding an email that Martin Sulzmann asked me to post on his behalf.

thanks. well, that is one view of things. but it is certainly not the only one.

first, about those "acrobatics": my type-class-level programs tend to start out as straightforward logic programs over types - no acrobatics involved, easy to understand. the acrobatics start when I'm trying to fit those straightforward programs into the straightjackets imposed by current systems - be they explicit restrictions or accidental limitations. wrestling them leads to the need to introduce complex work-arounds and implementation-specific tricks into the formerly clean logic programs.

The big question is: do we really want to do logic programming over types? I'd say, no! We are not doing logic programming over values either, are we? I have done my share of Prolog programming and what I repeatedly found is that I write functional programs using a horrible syntax (because you can't nest expressions) and with lots of cuts to prevent backtracking to kick in. If we want to express computations over types, we'll see the same advantages when using a functional style as we do see on values. Let's look at an example. Here addition and multiplication on Peano numerals using MPTCs and FDs: data Z data S a class Add a b c | a b -> c instance Add Z b b instance Add a b c => Add (S a) b (S c) class Mul a b c | a b -> c instance Mul Z b Z instance (Mul a b c, Add c b d) => Mul (S a) b d It's a mess, isn't it. Besides, this is really untyped programming. You can add instances with arguments of types other than Z and S without the compiler complaining. So, we are not simply using type classes for logic programming, we use them for untyped logic programming. Not very Haskell-ish if you ask me. I'd rather write the following: kind Nat = Z | S Nat type Add Z (b :: Nat) = b Add (S a) (b :: Nat) = S (Add a b) type Mul Z (b :: Nat) = Z Mul (S a) (b :: Nat) = Add (Mul a b) b Well, actually, I'd like infix type constructors and some other syntactic improvements, but you get the idea. It's functional and typesafe. Much nicer. Manuel

Jean-Philippe Bernardy:

On 3/18/06, Manuel M T Chakravarty wrote:

...

Here addition and multiplication on Peano numerals using MPTCs and FDs:

data Z data S a

class Add a b c | a b -> c instance Add Z b b instance Add a b c => Add (S a) b (S c)

class Mul a b c | a b -> c instance Mul Z b Z instance (Mul a b c, Add c b d) => Mul (S a) b d

It's a mess, isn't it. Besides, this is really untyped programming. You can add instances with arguments of types other than Z and S without the compiler complaining. So, we are not simply using type classes for logic programming, we use them for untyped logic programming. Not very Haskell-ish if you ask me.

I'd rather write the following:

kind Nat = Z | S Nat

type Add Z (b :: Nat) = b Add (S a) (b :: Nat) = S (Add a b)

type Mul Z (b :: Nat) = Z Mul (S a) (b :: Nat) = Add (Mul a b) b

Well, actually, I'd like infix type constructors and some other syntactic improvements, but you get the idea. It's functional and typesafe. Much nicer.

Indeed, this looks all very good and I truly believe this is the direction we should move in.

Still, a question: do you propose to go as far as to replace the "traditional" single parameter type-classes with /partial/ type constructors?

No. Type classes are fine as they are. However, if you want to associate types with classes, where the definition of these types varies on an instance by instance basis, I argue that associated types (ie, type definitions in classes) are more appropriate than MPTCs with FDs[*]: http://hackage.haskell.org/trac/haskell-prime/wiki/AssociatedTypes Associated types are *open* definitions of type functions (ie, you can always extend them by adding more instances). In some situations *closed* definitions of type functions are preferable (as in the Peano arithmetic example above, which can for example be nicely combined with GADTs to define bounded lists). AFAIK nobody has a worked out a proposal for how to add closed type functions to Haskell, but Tim Sheard has argued for their usefulness in his language Omega: http://www.cs.pdx.edu/~sheard/papers/LangOfTheFuture.ps Manuel [*] I am unsure whether we want MPTCs if we have associated types. It seems that the typical uses of MPTCs become single parameter classes when associated types are used instead of FDs.