the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

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_programming03.pdf
    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