Labels and the tentative solution to the MPTC Dilemma
This message shows the (extensible polymorphic) record selection code that requires neither overlapping instances and not even undecidable instances. Therefore, it works both in GHC and Hugs. This constructively shows that it is possible to write less-trivial code using functional dependencies and multi-parameter type classes as had been specified by Mark P. Jones -- that is, abiding by his syntactic decidability constraints. Therefore, if Haskell' standardized the current practice -- which is implemented _both_ by GHC and Hugs (with no overlapping instances, no undecidable instances), the result can still be useful. I do admit that writing the code below required jumping through more hoops than I would like, but I was prepared to suffer for the principle. The code highlights the benefits of the type equality predicate. With the type equality predicate, many common (albeit not all) uses of overlapping instances can be eliminated. It seems that overlapping instances is one of the more objectionable extensions, and not likely to be adopted in Haskell''. I have the feeling the remaining uses of overlapping instances can be eliminated likewise. That has the implication for the label proposal: it seems that introducing labels _without_ the total label equality predicate is not useful, as any serious use of labels in type-class programming would require overlapping instances (which are unlikely to be standardized). I personally find introducing labels via 'data' declaration isn't that big of an inconvenience, and I found the fact that these 'labels' behave exactly like nullary data/type constructors beneficial and elegant. {-# OPTIONS -fglasgow-exts #-} -- Records with very few extensions (no overelapping instances! -- and even no undecidable instances!) -- See the HList paper for additional explanations and details module SRec where -- Labels data L1 = L1 data L2 = L2 -- Equality predicate on labels data HTrue ; data HFalse class TypeEq a b c | a b -> c class EqL1 a c | a -> c instance EqL1 L1 HTrue instance EqL1 L2 HFalse class EqL2 a c | a -> c instance EqL2 L1 HFalse instance EqL2 L2 HTrue instance EqL1 b c => TypeEq L1 b c instance EqL2 b c => TypeEq L2 b c typeEq :: TypeEq a b c => a -> b -> c typeEq = typeEq -- Records are type-level associative lists -- Following Claus Reinke's notation infixl #? (#?) :: Select () label val rec => rec -> label -> val (#?) = lookp () class Select dummy label val rec | label rec -> val where lookp :: dummy -> rec -> label -> val instance (TypeEq label l tr, ProjLabel r l, Select' tr label val r) => Select () label val r where lookp () r label = lookup' (typeEq label (proj'label r)) r label class Select' tr label val rec | tr label rec -> val where lookup' :: tr -> rec -> label -> val instance Select' HTrue label val ((label,val),rest) where lookup' _ ((_,v),_) _ = v instance (TypeEq label l tr, ProjLabel rest l, Select' tr label val rest) => Select' HFalse label val (a,rest) where lookup' _ (_,r) label = lookup' (typeEq label (proj'label r)) r label class ProjLabel r l | r -> l where proj'label :: r -> l instance ProjLabel ((l,v),r) l where proj'label ((l,v),r) = l r1 = ((L1,True),((L2,'a'),((L1,["who's calling"]),()))) test1 = r1 #? L1 test2 = r1 #? L2
On 2/16/06, oleg@pobox.com
class EqL1 a c | a -> c instance EqL1 L1 HTrue instance EqL1 L2 HFalse
class EqL2 a c | a -> c instance EqL2 L1 HFalse instance EqL2 L2 HTrue [...]
Doesn't this spell quadratic blow-up on the number of labels in scope? It also seems tangled, considering the cost of adding a new label to the set. -- Cheers, Dinko
On Wed, Feb 15, 2006 at 08:29:48PM -0800, oleg@pobox.com wrote:
This message shows the (extensible polymorphic) record selection code that requires neither overlapping instances and not even undecidable instances. Therefore, it works both in GHC and Hugs. This constructively shows that it is possible to write less-trivial code using functional dependencies and multi-parameter type classes as had been specified by Mark P. Jones -- that is, abiding by his syntactic decidability constraints. Therefore, if Haskell' standardized the current practice -- which is implemented _both_ by GHC and Hugs (with no overlapping instances, no undecidable instances), the result can still be useful.
I'm afraid it's worse than that: current practice lacks a foundation, and attempts to provide one have exposed flaws (see the FunctionalDependencies page). FDs as specified by Mark are significantly weaker than what is implemented by GHC and Hugs. Even so, the original specification needs an additional restriction to prevent some non-terminating instances. In line with recent studies of FDs by Sulzmann et al, the CVS version of GHC has much tighter rules (closer to the original specification). It also has a more liberal termination condition for instances (see the end of FlexibleInstances), but this is only partial compensation. For example,
class TypeEq a b c | a b -> c class EqL1 a c | a -> c class EqL2 a c | a -> c instance EqL1 b c => TypeEq L1 b c instance EqL2 b c => TypeEq L2 b c
These instances are not permitted by the original restrictions: the third (range) argument contains a variable (c) that does not occur in the first two (domain) arguments. A safe relaxation has been proposed (see end of FunctionalDependencies) and Simon favours adding it to GHC. It is quite complex, though.
class Select dummy label val rec | label rec -> val where lookp :: dummy -> rec -> label -> val
instance (TypeEq label l tr, ProjLabel r l, Select' tr label val r) => Select () label val r where lookp () r label = lookup' (typeEq label (proj'label r)) r label
This instance (and the similar one for Select') were permitted by the original rules, under a relaxation that has since been shown to produce non-termination in some cases (CHR paper, ex. 15). No replacement has been proposed, so the relaxation has been removed from the CVS version of GHC, which thus rejects this.
participants (3)
-
Dinko Tenev -
oleg＠pobox.com -
Ross Paterson