Labels and the tentative solution to the MPTC Dilemma

[oleg at pobox.com]

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