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@haskell.org http://haskell.org/mailman/listinfo/haskell-prime