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