Changes between Version 9 and Version 10 of TypeFunctions/ClassFamilies


Ignore:
Timestamp:
May 18, 2007 6:43:46 AM (8 years ago)
Author:
sulzmann
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions/ClassFamilies

    v9 v10  
    7171 * Should an associated class be a (kind of) superclass of its parent.  At least, we may want to add it implicitly to the signature of each method.  Not sure about this, but Roman suggested it, too.
    7272 * Do we allow associated types and classes(?!?) in class-family instances?
     73
     74
     75=== Further Examples ===
     76
     77Here's a sketch of a "modular" extension of Hinze's "Generics for the masses" (GM)
     78approach using indexed classes.  We first explain why in the original
     79GM approach we cannot override generic with specific (ad-hoc) behavior
     80in a modular fashion.
     81
     82The main idea behind the GM approach is to provide
     83a uniform representation of data types in terms of
     84unit, sum and product types.
     85Generic functions are defined in terms of this uniform
     86rather than the concrete structural representation of a data type.
     87The programmer only needs to maintain a type isomorphism between
     88the uniform and concrete representation.
     89Thus, there is no need to extend
     90the (now generic) definition of functions in case we include new data types.
     91
     92Here is a (over-simplified) presentation of the GM approach
     93We only consider the uniform representations "literals" and "plus".
     94
     95{{{
     96data Lit = Lit Int
     97data Plus a b = Plus a b
     98class Generic g where
     99  lit :: g Lit
     100  plus :: g a -> g b -> g (Plus a b)
     101}}}
     102
     103Below is a generic definition of some evaluation function.
     104
     105{{{
     106newtype Ev a = Ev{eval' :: a -> Int}
     107instance Generic Ev where
     108  lit = Ev (\x -> case x of Lit i -> i)
     109  plus a b = 
     110    Ev (\p -> case p of
     111               (Plus x y) -> eval' a x + eval' b y)
     112}}}
     113
     114
     115In order to use the evaluator on its familiar type,
     116we need a ``dispatcher'' function to select the appropriate case of
     117a generic function.
     118The most straightforward approach is to use an ad-hoc polymorphic
     119(therefore extensible) function.
     120{{{
     121class Rep a where
     122  rep :: Generic g => g a
     123instance Rep Lit where
     124  rep = lit
     125instance (Rep a,Rep b) => Rep (Plus a b) where
     126  rep = plus rep rep
     127eval :: Rep t => t -> Int
     128eval = eval' rep
     129}}}
     130The dispatcher function rep will select the
     131appropriate generic case depending on the concrete type context.
     132We can straightforwardly introduce new generic functions (omitted here).
     133
     134Suppose we introduce a new ad-hoc case "minus" which has the
     135same structural representation as "plus".
     136
     137{{{
     138data Minus a b = Minus a b
     139class Generic g => GMinus g where
     140  minus :: g a -> g b -> g (Minus a b)
     141instance GMinus Ev where
     142  minus a b = 
     143    Ev (\p -> case p of
     144               (Minus x y) -> eval' a x - eval' b y)
     145instance (Rep a,Rep b) => Rep (Minus a b) where
     146  rep = minus rep rep
     147}}}
     148
     149The problem is that we cannot access this new case, unless
     150we update the type of the dispatcher function rep. We must
     151change rep's declaration as follows.
     152
     153{{{
     154class Rep a where
     155  rep :: GMinus g => g a
     156-- original code: rep :: Generic g => g a
     157}}}
     158
     159But changing rep's class declaration requires to recompile the entire
     160program. Hence, extending generic definitions with ad-hoc cases
     161cannot be modularly.
     162
     163Such problems go away if we use indexed classes.
     164More precisely, we use a type indexed class in rep's class declaration.
     165
     166The generic cases.
     167{{{
     168class Rep a where
     169  class Generic' g a
     170  -- or class Generic' g :: * -> Class using Tom's suggestion
     171  rep :: Generic' g a => g a
     172instance Rep Lit where
     173  class Generic g => Generic' g Lit
     174  -- better written as? Generic' g Lit = Generic g
     175  rep = lit
     176instance (Rep a,Rep b) => Rep (Plus a b) where
     177  class Generic g => Generic' g (Plus a b)
     178  rep = plus rep rep
     179eval :: Rep t => t -> Int
     180eval = eval' rep
     181}}}
     182
     183The ad-hoc case.
     184{{{
     185class GMinus g where
     186  minus :: g a -> g b -> g (Minus a b)
     187instance GMinus Ev where
     188  minus a b = 
     189    Ev (\p -> case p of
     190               (Minus x y) -> eval' a x - eval' b y)
     191
     192instance (Rep a,Rep b) => Rep (Minus a b) where
     193  class GMinus g => Generic' g (Minus a b)
     194  rep = minus rep rep
     195}}}
     196
     197Notice the use of indexed classes to select appropriate classes
     198for each instance.
     199
     200
     201General insight: It seems that via indexed classes we can encode
     202a type-passing type-class translation scheme.
     203
    73204
    74205=== Type checking ===