the MPTC Dilemma (please solve)

[Claus Reinke]

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