Type Classes (20 October 2005)

A Bibliography

How to made ad-hoc polymorphism less ad-hoc

P. Wadler and S. Blott (1988). First type class paper? Simple translation to Hindley-Milner. Principle type problem (in A.7).

Type classes in Haskell

C. Hall, K. Hammond, S. Peyton Jones, and P. Wadler (1994). I expected this to be a somewhat more mature treatment, but it's mostly the same as the above; I think I prefer Wadler and Blott.

Implementing type classes

J. Peterson and M. Jones (1993). I've been led to believe that there's a paper describing how to make type classes more efficient than the naive translation in Wadler and Blott (1988); is that this paper?

Parametric type classes

K. Chen, P. Hudak, and M. Odersky (1992). Introduction of and justification for multiparameter type classes.

Type classes: an exploration of the design space

S. Peyton Jones, M. Jones, E. Meijer (1997). The title is misleading, but the filename on Peyton Jones's site—multi.ps—is less so. Multiparameter type classes are neat.

Type classes with functional dependencies

M. Jones (2000). If multiparameter type classes are (pure) Prolog, then fundeps are modes.

A typed representation for HTML and XML documents in Haskell

P. Thiemann (2002). We know that we can use types to statically guarantee well-formedness. With fundeps, we can also guarantee validity for XML (or pseudo-validity for HTML).

A functional notation for functional dependencies

M. Neuebauer, P. Thiemann, M. Gasbichler, M. Sperber (2000). Predicates with modes are functions, so why not write them that way?

Faking it: simulating dependent types in Haskell

C. McBride (2002). I haven't read this, but it might be interesting (for me).

Sound and decidable type inference for functional dependencies

G. Duck, S. Peyton Jones, P. Stuckey, and M. Sulzmann (2004). Really?

Essential

• Introduction and rationale
• Rationale:
  • Standard ML: eqtypes and weird behavior of +
  • C++: ad-hoc and confusing
  • Miranda: unsafe
  • Ocaml: +.
  These are ugly. (So is print.)
• Typeclasses: Eq, Num, Ord, Show.... Each of these is a set of types that supports certain operations. Example code:

  class Eq a where         -- A type a is in Eq if
    (==) :: a -> a -> Bool -- it has an operation (==)
  
  instance Eq Int where    -- Int is in Eq, and
    a == b  = eqInt a b    -- we supply (==)
  
  -- forall a \in Eq. a -> [a] -> Bool
  find :: Eq a => a -> [a] -> Bool
  find x []     = False
  find x (y:ys)
    | x == y    = True
    | otherwise = find x ys
  
  _ = find 3 [1, 2, 3]
  
  instance Eq a => Eq [a] where
    [] == []         = True
    [] == _          = False
    _  == []         = False
    (x:xs) == (y:ys) = (x == y) and (xs == ys)
  
  _ = find [3] [[], [1], [2, 3]]
  
  class Eq a => Ord a where
    (<)   :: a -> a -> Bool
    (<=)  :: a -> a -> Bool
    a <= b = (a == b) or (a < b)
  
  -- some example using Ord a, (==), ...
  -- binary trees?
  
  data Ord a => Bintree a b = Inner a b (Bintree a b) (Bintree a b)
                            | Leaf a b
  lookup :: Ord a => Bintree a b -> a -> Maybe b
  lookup (Leaf k v) k'
    | k' == k   -> Just v
    | otherwise -> Nothing
  lookup (Inner k v l r)
    | k' == k'  -> Just v
    | k' < k    -> lookup l k'
    | otherwise -> lookup r k'
  

• Translation

  -- class declarations are now record types:
  data Eq a = makeEq {
    eq :: a -> a -> Bool
  }
  
  -- instances are record values:
  eqInt :: Eq Int
  eqInt  = makeEq {
    eq = \a b -> eqInt a b
  }
  
  find :: Eq a -> a -> [a] -> Bool
  find eqDict x []     = False
  find eqDict x (y:ys)
    | eq eqDict x y   = True
    | otherwise       = find eqDict x ys
  
  _ = find eqInt 3 [1, 2, 3]
  
  eqList :: Eq a -> Eq [a]
  eqList eqDict = makeEq {
    eq = eqh where
      eqh [] []         = True
      eqh [] _          = False
      eqh _  []         = False
      eqh (x:xs) (y:ys) = (eq eqDict x y) and (eqh xs ys)
  }
  
  _ = find (eqList eqInt) [3] [[], [1], [2, 3]]
  

  • Contexts

    data Sign = Neg | Zero | Pos
    
    sign x
      | x < 0 = Neg
      | x == 0 = Zero
      | otherwise = Pos
    
    Is the signature:
    - sign :: Num a => a -> Sign
    - sign :: (Eq a, Ord a, Num a) => a -> Sign
    - or something else similar?
    
    Does this affect the number of dictionaries that get passed?
    

  • Optimizations

    -- problem: huge stack frames
    -- problem: fib is a function
    
    fib  :: [Integer]
    fib   = 1 : 1 : [ x + y | x <- fib, y <- tail fib ]
    
    fib  :: Num a -> [a]
    fib d = 1 : 1 : [ x + y | x <- f, y <- tail f ] where f = fib d
    

Optional

• Clean, Mercury, . . .
• Multiple parameters
• Type programming (examples)
  • Multiparam: extensible sums (Union.hs)

    {-# OPTIONS -fglasgow-exts #-}
    {-# OPTIONS -fallow-overlapping-instances #-}
    {-# OPTIONS -fallow-undecidable-instances #-}
    module Union where
    
    infixr :|:
    data a :|: b = West a | East b
    
    instance (Show a, Show b) => Show (a :|: b) where
        showsPrec p (West a) = showsPrec p a
        showsPrec p (East a) = showsPrec p a
    
    class Union u a where
        inj          :: a -> u
        prj          :: u -> Maybe a
    instance Union (a :|: u) a where
        inj           = West
        prj (West a)  = Just a
        prj _         = Nothing
    instance Union u a => Union (c :|: u) a where
        inj           = East . inj
        prj (East a)  = prj a
        prj _         = Nothing
    
    -- interesting base case -- allowed re-injection from subtypes:
    instance Union (u :|: a) a where
        inj           = East
        prj (East a)  = Just a
        prj _         = Nothing
    
    type Foo = Char :|: String :|: ()
    
    a, b :: Foo
    a     = inj 'a'
    b     = inj "b"
    
    type BoolT a = (Maybe Bool) :|: Bool :|: a
    
    c, d, e :: BoolT Foo
    c        = inj 'c'
    d        = inj True
    e        = inj (Just False)
    
    mapU f l = map f' l where
      f' x = case prj x of
        Nothing -> x
        Just a  -> inj (f a)
    
    l1 = [c, d, e, inj b, inj a]
    l2 = mapU (++"oo") l1
    l3 = mapU not l2
    l4 = mapU (:"oo") l3
    

  • Fundeps: n-ary functions (Multi.hs)

    {-# OPTIONS -fglasgow-exts #-}
    {-# OPTIONS -fallow-undecidable-instances #-}
    {-# GHC_OPTIONS -fcontext-stack400 #-}
    module Multi where
    
    import Prelude hiding (sum)
    
    {-
    Suppose we want to define n-ary sum.
    
    We might define a family of functions:
    
    Sum[0]   = Int
    Sum[n+1] = Int -> Sum[n]
    
    sum[n]  :: Sum[n]
    sum[n]   = sum'[n] 0 where
    
    sum'[n]      :: Integer -> Sum[n]
    sum'[0]   acc = acc
    sum'[n+1] acc = \x -> sum[n] (x + acc)
    
    What are their types?
    
    Sum is a family of types -- even more, it's a function from
    nat -> types in this family:
    -}
    
    -- We need Peano numerals:
    data Z   = Z
    data S n = S n
    
    class Sum nat x | nat -> x where
      sumacc          :: nat -> Integer -> x
    
    instance Sum Z Integer where
      sumacc Z acc     = acc
    
    instance Sum nat x => Sum (S nat) (Integer -> x) where
      sumacc (S n) acc = \x -> sumacc n (acc + x)
    
    sum  :: Sum nat x => nat -> x
    sum n = sumacc n 0
    
    -- we don't even need the values:
    class Sum' nat x | nat -> x where
      sumacc'      :: nat -> Integer -> x
    instance Sum' Z Integer where
      sumacc' _ acc = acc
    instance Sum' nat x => Sum' (S nat) (Integer -> x) where
      sumacc' _ acc = \x -> sumacc' (bot::nat) (acc + x)
    
    sum' (_::t) = sumacc' (bot::t) 0
    bot = bot
    
    {-
    Prolog:
    add(zero, B, B).
    add(succ(A), B, C) :- add(A, succ(B), C).
    
    mul(zero, A, zero).
    mul(succ(A), B, C) :- mul(A, B, D), add(B, D, C).
    
    These are Horn-clause programs.  The class declaration provides
    a declaration and "type" for the predicate, and the fundeps are
    in/out modes.
    -}
    
    class Add a b c | a b -> c where
      (/+/)    :: a -> b -> c
    instance Add Z a a where
      Z /+/ n   = n
    instance Add a b c => Add (S a) b (S c) where
      S a /+/ b = S (a /+/ b)
    
    class Mul a b c | a b -> c where
      (/*/)    :: a -> b -> c
    instance Mul Z a Z where
      Z /*/ _   = Z
    instance (Mul a b ab, Add b ab c) => Mul (S a) b c where
      S a /*/ b =  b /+/ (a /*/ b)
    
    class Reify x f r | f -> r where
      reify      :: f -> r -> x -> r
    instance Reify Z (r -> r) r where
      reify f r _ = r
    instance Reify n (r -> r) r => Reify (S n) (r -> r) r  where
      reify f r _ = f (reify f r (bot::n))
    
    toNum :: (Num a, Reify x (a -> a) a) => x -> a
    toNum  = reify (+1) 0
    
    class Add' a b c | a b -> c where
      (/++/) :: a -> b -> c
      (/++/)  = bot
    instance Add' Z a a where
    instance Add' a b c => Add' (S a) b (S c) where
    
    class Mul' a b c | a b -> c where
      (/**/) :: a -> b -> c
      (/**/)  = bot
    instance Mul' Z a Z where
    instance (Mul' a b ab, Add' b ab c) => Mul' (S a) b c where
    
    class Fact a b | a -> b where
      fact :: a -> b
      fact  = bot
    instance Fact Z (S Z) where
    instance (Fact a c, Mul' (S a) c b) => Fact (S a) b where
    
    p0  = Z
    p1  = S p0
    p2  = S p1
    p3  = S p2
    p4  = S p3
    p5  = S p4
    p20 = p4 /**/ p5
    
    -- Now I can "conveniently" make a nine-place sum:
    sum9'  = sum' (S (S (S Z)) /**/ S (S (S Z)))
    sum9'' = sum' (S (S (S (S (S (S (S (S (S Z)))))))))
    
    class FoldN nat a r x | nat a r -> x where
      foldlN, foldrN :: nat -> (a -> r -> r) -> r -> x
      foldrNk        :: nat -> (a -> r -> r) -> r -> (r -> r) -> x
      foldrN n f z    = foldrNk n f z id
    instance FoldN Z a r r where
      foldlN  _ _  r    = r
      foldrNk _ _  z k  = k z
    instance FoldN nat a r x => FoldN (S nat) a r (a -> x) where
      foldlN  _ f z   a = foldlN  (bot::nat) f (f a z)
      foldrNk _ f z k a = foldrNk (bot::nat) f z (\r -> k (f a r))
    
    sumN n     = foldlN n (+) 0
    prodN n    = foldlN n (*) 1
    reverseN n = foldlN n (:) []
    
    -- How would we write listN?  We need foldrN
    listN n    = foldrN n (:) []
    
    -- Extensible printf -- cool.  Uses accumulator like foldrNk.
    
    -- now zipWithN:
    class ZWH nat a x | nat a -> x where
      zwh         :: nat -> a -> x
    instance ZWH Z [a] [a] where
      zwh _ lst    = lst
    instance ZWH n [b] x => ZWH (S n) [a -> b] ([a] -> x) where
      zwh _ l1 l2  = zwh (bot::n) (zipWith ($) l1 l2)
    
    zipWithN n f = zwh n (repeat f)
    
    n1 = zipWithN p1 (+2) [1,2,3,4]
    n2 = zipWithN p2 (+)  [1,2,3,4] [50,40,30,20]
    n3 = zipWithN p3 (,,) [True, False, False] ['a', 'c', 'e'] [6,7,8]
    n4 = zipWithN p4 (reverseN p4) [1,2,3,4] [5,6,7,8] [9,10,11,12] [13,14,15,16]
    
    -- Do we need N?  Not if we're willing to specify write a type:
    class ZWA a x | x -> a where
      zwa       :: a -> x
    instance ZWA [a] [a] where
      zwa lst    = lst
    instance ZWA [b] (c x) => ZWA [a -> b] ([a] -> c x) where
      zwa l1 l2  = zwa (zipWith ($) l1 l2)
    
    zipWithA f = zwa (repeat f)
    
    a1, a2 :: [Bool]
    a3 :: [(Bool, Char, Ordering)]
    a4 :: [[Integer]]
    a1 = zipWithA not [True, False, False, True]
    a2 = zipWithA (&&) [True, True, False] [True, False, False]
    a3 = zipWithA (,,) [True, False, False] ['a', 'c', 'e'] [EQ, LT, LT]
    a4 = zipWithA (reverseN p4) [1,2,3,4] [5,6,7,8] [9,10,11,12] [13,14,15,16]
    
    a5 = concat (zipWithA (:) "ABCD" ["bcd", "cde", "def", "efg"])