the MPTC Dilemma (please solve)

[Claus Reinke]

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

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