Personal tools

GHC/AdvancedOverlap

From HaskellWiki

< GHC
Jump to: navigation, search

Contents

1 Choosing a type-class instance based on the context

Oleg Kiselyov and Simon Peyton-Jones (Apr 2008)

1.1 Problem definition

Suppose you have this class:

class Print a where
    print :: a -> IO ()
Now suppose you want to say "if type
a
is in class
Show
, print one way, otherwise print another way". You'd probably try to write this:
instance Show a => Print a where
    print x = putStrLn (show x)
instance           Print a where
    print x = putStrLn "No show method"

But that is illegal in Haskell, because the heads of the two instance declarations are identical. Nevertheless, you can code it up using functional dependencies and overlapping instances, and that's what this note describes.

1.2 Solution 1 (using safer overlapping instances)

First define an auxiliary class
Print'
:
class Print' flag a where
    print' :: flag -> a -> IO ()
 
instance (ShowPred a flag, Print' flag a) => Print a where
    print = print' (undefined::flag)
The main class
Print
has only one instance, and there is no longer any overlapping. The new class
ShowPred
has no methods, but its instances precisely mirror those of
Show
:
-- Just two distinct types
-- alternatively use 'True and 'False with -XDataKinds
data HTrue    
data HFalse   
 
class ShowPred a flag | a->flag where {}
 
                                  -- Used only if the other
                                  -- instances don't apply
-- instance TypeCast flag HFalse => ShowPred a flag -- before -XTypeFamilies
instance (flag ~ HFalse) => ShowPred a flag
 
instance ShowPred Int  HTrue   -- These instances must be
instance ShowPred Bool HTrue   -- the same as Show's
instance ShowPred a flag => ShowPred [a] flag
-- ...etc...
These instances do make use of overlapping instances, but they do not rely on the *context* to distinguish which one to pick, just the instance *head*. Notice that
(ShowPred ty flag)
always succeeds! If
ty
is a type for which there is a Show instance, flag gets unified to
HTrue
; otherwise flag gets unified to
HFalse
. Now we can write the (non-overlapping) instances for
Print'
:
 instance (Show a) => Print' HTrue a where
   print' _ x = putStrLn (show x)
 instance Print' HFalse a where
   print' _ x = putStrLn "No show method"
The trick is to re-write a constraint
(C a)
which succeeds of fails, into a predicate constraint
(C' a flag)
, which always succeeds, but once discharged, unifies flag with either
HTrue
or
HFalse
. The desired invariant is
       C a succeeds <--> C' a flag unifies flag with HTrue
Perhaps the most puzzling is the constraint
(TypeCast flag HFalse)
in the first instance of
ShowPred
. The
TypeCast
constraint and its important role are explained in Section 9 and specifically Appendix D of the full HList paper

<http://homepages.cwi.nl/~ralf/HList/paper.pdf>

1.2.1 Notes and variations

1. A more `closed world' alternative: write
ShowPred
as follows
class ShowPred a flag | a->flag where {}
instance HMember a Showtypes flag => ShowPred a flag
There is only one instance of
ShowPred
and there is no overlapping instances. Here,
Showtypes
are defined as
type Showtypes = Int :+: Bool :+: Char :+: ... :+: HNil
(Polymorphic types like
[a]
take more effort, but they too can be handled). This is the closed list of types, and
HMember
is a
HList
membership checker.
HMember
uses
TypeEq
-- and the latter is the only place that

requires overlapping instances.


2. There is, of course, no check that the instances of
ShowPred
match those of
Show
; you just have to get that right. An alternative, which trades this problem for another, is instead to *replace* by
Show'
, which has the auxiliary flag:
class Show' a flag | a->flag where
    show :: a -> String
 
        -- This instance is used only if the others don't apply
instance TypeCast flag HFalse => Show' a flag where
    show = error "urk"
 
        -- These instances are the regular ones
instance Show' Int HTrue where
    show = showInt
instance Show' Bool HTrue where
    show = showBool
...etc...
Now we can write the instances for
Print'
:
 instance Show' HTrue a => Print' HTrue a where
   print' x = putStrLn (show x)
 instance Print' HFalse a where
   print' x = putStrLn "No show method"
The disadvantage here is, of course, that you have to change the
Show

class.


3. We need a bit of boolean algebra in the more interesting instances

of
ShowPred
:
 instance (ShowPred a flag1, ShowPred b flag2, And flag1 flag2 flag)
       => (ShowPred (a,b) flag
 
 class And a b c | a b -> c
instance And HTrue  b b
instance And HFalse b HFalse

The HList paper shows many examples of such type-level programming.

1.3 Solution 2 (using incoherent instances)

Turn
ShowPred
into a type family:
-- ShowPred is a predicate on types, which says
-- which ones are instances of class Show
type family ShowPred a
 
type instance ShowPred a     = HFalse
type instance ShowPred Int    = HTrue
type instance ShowPred Bool   = HTrue
type instance ShowPred [a]   = ShowPred a
type instance ShowPred (a,b) = And (ShowPred a, ShowPred b)
-- ...etc...
There's a problem: overlap is not generally allowed for type families!! (The first
ShowPred
instance makes all others redundant.) There is a good reason for this, but it's not helpful here.

Without closed families, a solution is still available which mirrors the original program from solution 1. This requires -XIncoherentInstances in addition to the other flags.

class Print a where
    print :: a -> IO ()
instance (ShowPred a ~ flag, Print' flag a) => Print a where
    print = print' (undefined::flag)
 
class Print' flag a where
  print' :: flag -> a -> IO ()
instance Show a => Print' HTrue a where
  print' _ x = putStrLn (show x)
instance Print' flag a where
  print' _ _ = putStrLn "No show method"
 
 
data HTrue
data HFalse
type family ShowPred a 
type instance ShowPred Int = HTrue
type instance ShowPred Bool = HTrue
Here, the original formulation is closely mirrored but with the former
ShowPred
class expressed instead as a type family. The programs look very similar, however the type family based one may be easier to come to understand. For the original, when trying to satisfy the constraint in
instance (ShowPred a flag, Print' flag a) => Print a
, the tough case is when
ShowPred a flag
doesn't result with flag as HTrue. The catch-the-rest instance
instance (flag ~ HFalse) => ShowPred a flag
, requires a further constraint to be satisfied. Needing more information, the other constraint,
Print' flag a
, will be checked. Since the first constraint didn't resolve with flag = HTrue,
Print' HTrue a
will not be satisfied. However,
Print' HFalse a
allows us to unify
(flag ~ HFalse)
in the
ShowPred a
constriaint. Consequently the whole constraint is satisfied.

1.4 Solution 3 (using closed type families)

As of GHC 7.8, closed type families are available. For more details, see Type families#Closed family simplification. It is possible to rewrite
ShowPred
like this:
type family ShowPred a where
  ShowPred Int    = HTrue
  ShowPred Bool   = HTrue
  ShowPred [a]   = ShowPred a
  ShowPred (a,b) = And (ShowPred a, ShowPred b)
  ShowPred a     = HFalse

There are no incoherent instances anymore.

Any unspecified
ShowPred a
resolves to
ShowPred a
making the specific
Print' HTrue a
instance fail and leaving the catch-the-rest
Print' flag a
to succeed with
Print' (ShowPred a) a
.


2 Appendix: the sample code

{-# LANGUAGE EmptyDataDecls,
             MultiParamTypeClasses,
             ScopedTypeVariables,
             FunctionalDependencies,
             OverlappingInstances,
             FlexibleInstances,
             UndecidableInstances #-}
 
module Main where
 
import Prelude hiding (print)
 
class Print a where
    print :: a -> IO ()
 
{- the following does not work:
instance Show a => Print a where
    print x = putStrLn (show x)
instance        Print a where
    print x = putStrLn "No show method"
 
error:
    Duplicate instance declarations:
      instance (Show a) => Print a -- Defined at /tmp/wiki.hs:7:0
      instance Print a -- Defined at /tmp/wiki.hs:9:0
-}
 
class Print' flag a where
    print' :: flag -> a -> IO ()
 
instance (ShowPred a flag, Print' flag a) => Print a where
    print = print' (undefined::flag)
 
 
-- overlapping instances are used only for ShowPred
class ShowPred a flag | a->flag where {}
 
                                  -- Used only if the other
                                  -- instances don't apply
instance TypeCast flag HFalse => ShowPred a flag
 
instance ShowPred Int  HTrue   -- These instances should be
instance ShowPred Bool HTrue   -- the same as Show's
instance ShowPred a flag => ShowPred [a] flag
--  ...etc...
 
 
data HTrue    -- Just two
data HFalse   -- distinct types
 
instance Show a => Print' HTrue a where
   print' _ x = putStrLn (show x)
instance Print' HFalse a where
   print' _ x = putStrLn "No show method"
 
test1 = print [True,False] -- [True,False]
test2 = print id           -- No show method
 
 
 
 
-- see http://okmij.org/ftp/Haskell/typecast.html
class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x  = x