the MPTC Dilemma (please solve)

[Claus Reinke]

> When I said "type class acrobats" I didn't mean to make fun
> of people like you who use type classes in a very skillfull way.
> Though, I tried (successfully :) ) to be provocactive.

thought so:) but there are others listening, and I didn't want them
to go away with the idea that this does only concern some "others",
not mainstream Haskellers.

I think this is at the heart of Haskell's contribution to language
design and programming practice, which has evolved since the 
first reports. type classes ceased to be just about "overloading" 
a long time ago, and anyone trying to understand current practice 
from that original background will have a hard time. whereas, 
with a slight change of perspective, things become a lot clearer 
and easier to understand.
 
> I agree with you there's a real need for unrestricted type class
> programming. 

thanks. I would go so far to say that, independent of which 
"extensions" will go into the language, the Haskell' report should
replace the old story about "less ad-hoc overloading" with the
new story about extracting programs from proofs over types
(or logic meta-programming over typed functional programs).

> The trouble I have with the current practice of type class programming
> is that it's not very principled (yes, I'm provocactive again).
> People learn how to write type class programs by observing the
> behavior of a specific implementation and sometimes the results
> are quite unexpected.

how is current practice ever to become more principled and
less implementation-dependent when the recorders of principles 
and definers of language avoid dealing with the issues?!

that is exactly the part I'm campaigning against, and I believe that
it has its source in the lack of acknowledgement in the language 
definition. in my view, the restrictions in the language definition are
artificial, and complicate the situation (yes, they do so for a purpose,
but I can be provocative, too;). moreover, implementations dealing
in "extensions" know that they are outside the standard anyway, so
why even try to lay down any common rules?

in the unconstrained view of type class programming, those 
"extensions" are just relaxations of constraints that are often, but 
not always useful. and there is a coherent picture behind it that 
should be reflected in the language, and in its definition. I always 
thought that qualified types were a lot more elegant than the 
systems they were trying to give a semantics to, and what I'd 
like to see is a language that better represents that semantic 
domain.

> I have been mentioning CHRs before as a very useful tool to study
> FDs. In fact, CHRs go way beyond FDs see "A Theory of Overloading".
> I claim that when it comes to unrestricted type class programming
> CHRs are the way to go. CHRs have a clean semantic meaning and
> precisely explain the meaning of type class programs.

as far as I can see, replacing qualified types with CHRs become 
necessary/convenient only once one tries to account for things like
FDs, because their non-local interactions are not mediated by
variables (and adding constraints to the global store can capture
that easily). but I see you feel about CHRs almost the way I do 
about QTs. I don't much mind which one you choose for semantics
of type classes, but I'd like to go a step further than just explaining
type classes in CHRs or QTs, and make type classes a syntactic
representation of their semantic domain.

it is this *two-way* connection between syntax and semantics that
has made the greatest impact in semantics-based language design.

and I think the way forward is to capture the unconstrained picture
first, because it is simpler and so that we understand what we are 
talking about. sort out the current differences in view about that
unconstrained picture, and then to add restrictions in order to 
achieve additional properties. but the language definition should 
describe both the unconstrained and the restricted version, in 
order to cater for what you describe as a real need to get away 
from current unprincipled practice.

cheers,
claus