the MPTC Dilemma (please solve)

[Martin Sulzmann]

It's very hard to follow you here. Can you formalize your proposal
below such that we can verify some formal results (e.g. tractable
inference, coherence etc).

Why not be "macho" and use a formal framework in which this all
can be expressed?

In one of your previous emails you said:

 > ...make type classes a syntactic
 > representation of their semantic domain.

What do you mean? Explaining type classes in terms of
type classes? This can't work.

In your previous email, you mentioned the Theory of Qualified
Types (QT) and CHRs as formal type class frameworks but you
seem to be reluctant to use either of these frameworks. Why?

To a large extent, CHRs will do the job. See FDs and my reply
to your other email regarding disequality constraints.

In case, people don't know CHRs. Here's
the type class to CHR translation.

1) For each  class C => TC t
we generate a propagation CHR
rule TC t ==> C
Ex: class Eq a => Ord a translates to
    rule Ord a ==> Eq a

2) For each instance C => TC t
we generate a simplification CHR
rule TC t <==> C
Ex: instance Eq a => Eq [a] translates to
    rule Eq [a] <==> Eq a

Roughly, the CHR semantics is as follows.
Propagation rules add (propagate) the right-hand side
if we find a match to the left-hand side.
Simplification rules reduce (simplifify) the left-hand side
by the right-hand side.

Example:

rule Ord a ==> Eq a   -- (R1)
rule Eq [a] <==> Eq a -- (R2)

  Ord a -->R1 Ord a, Eq a

  Eq [Int] -->R2 Eq Int

This shows that CHRs are *very* close in terms of syntax and semantics
of type classes. 

BTW, 1) shows that the superclass arrow should indeed be the other way
around and 2) shows that instances do NOT correspond to Prolog-style
Horn clauses.

In fact, I don't really care if you're using CHRs, QT or whatever.
As long as there's a (at least semi-) formal description. Otherwise,
we can't start a discussion because we don't know what we're talking
about.

Martin



Claus Reinke writes:
 > [I suggest to keep follow-on discussions to the haskell prime list,
 >  to avoid further copies]
 > 
 > > continuing the list of odd cases in type class handling, here is a
 > > small example where overlap resolution is not taken into account
 > > when looking at FDs. 
 > 
 > actually, one needs to take both into account to arrive at the 
 > interpretation I favour:
 > 
 > - variables in the range of an FD can never influence instance
 >     selection if the variables in the domain of that FD are given
 >     (for, if they did, there'd be two instances with different range
 >     types for the same domain types -> FD violation)
 > 
 > - in other words, FDs not only tell us that some type relations
 >     are functional, they can be seen as roughly similar to what is 
 >     called mode declarations in logic programming: they tell us 
 >     with which input/output combinations a type relation may 
 >     be used
 > 
 > - for each FD a given constraint is subject to, the range types 
 >     should be ignored during instance selection: the domain types
 >     of the FD constitute the inputs and are sufficient to compute 
 >     unique FD range types as outputs of the type relation. the
 >     computed range types may then be compared with the range 
 >     types given in the original constraint to determine whether the
 >     constraint can be fulfilled or not
 > 
 > if we apply these ideas to the example I gave, instance resolution
 > for the "3 parameter, with FD"-version proceeds exactly as it
 > would for the "2 parameter"-version, using best-fit overlap
 > resolution to determine a unique 3rd parameter (range of FD)
 > from the first two (domain of FD).
 > 
 > this would seem similar to what we do at the function level:
 > 
 >     f a b | let res = True, a==b = res
 >     f a b | let res = False, otherwise = res
 > 
 > here, the implementation does not complain that f isn't functional
 > because we could instantiate {a=1,b=1,res=False} as well as 
 > {a=1,b=1,res=True} - instead it treats res as output only, a and b 
 > as input, and lets first-fit pattern matching resolve the overlap in 
 > the patterns. these rules describe a function because we say it does.
 > 
 > whereas, at the type class level, the implementations say "okay,
 > you said this is a type function, with two input and one output 
 > parameters, but if I ignore that for the moment, then overlap 
 > resolution doesn't kick in because of the different 3rd input 
 > parameter, and now there are two instances where there should 
 > only be one {TEQ a a T, TEQ a a F}; and if I now recall
 > that this should be a type function, I have to shout 'foul!'".
 > 
 > am I the only one who thinks this does not makes sense?-)
 > 
 > cheers,
 > claus
 >  
 > >    {- both ghc and hugs accept without 3rd par and FD
 > >       neither accepts with 3rd par and FD -}
 > > 
 > >    data T = T deriving Show
 > >    data F = F deriving Show
 > > 
 > >    class    TEQ a b {- tBool | a b -> tBool -} where teq :: a -> b -> Bool
 > >    instance TEQ a a {- T                    -} where teq _ _ = True
 > >    instance TEQ a b {- F                    -} where teq _ _ = False
 > > 
 > >    test = print (teq True 'c', teq True False)
 > 
 > _______________________________________________
 > Haskell-prime mailing list
 > Haskell-prime at haskell.org
 > http://haskell.org/mailman/listinfo/haskell-prime