the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

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?

You have to be more careful with unification in a higher-kinded setting.
I am not sure how to do that with CHRs.
 
> > 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.

The dependency seems to be lost here.

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

> 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).

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

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

The latter.

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

Our formalisation of ATs stays very close to the formalisation of
qualified types, which to me is the state of the art of formalising type
classes.

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

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

Who wants to throw out type classes?

Manuel