Difference between revisions of "GHC/AdvancedOverlap"
(→Solution 2 (using incoherent instances)) 

(10 intermediate revisions by 5 users not shown)  
Line 2:  Line 2:  
Oleg Kiselyov and Simon PeytonJones (Apr 2008) 
Oleg Kiselyov and Simon PeytonJones (Apr 2008) 

+  
+  === Problem definition === 

Suppose you have this class: 
Suppose you have this class: 

<haskell> 
<haskell> 

−  +  class Print a where 

print :: a > IO () 
print :: a > IO () 

</haskell> 
</haskell> 

−  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: 
+  Now suppose you want to say "if type <hask>a</hask> is in class <hask>Show</hask>, print one way, otherwise print another way". You'd probably try to write this: 
<haskell> 
<haskell> 

−  +  instance Show a => Print a where 

print x = putStrLn (show x) 
print x = putStrLn (show x) 

−  +  instance Print a where 

print x = putStrLn "No show method" 
print x = putStrLn "No show method" 

</haskell> 
</haskell> 

+  
But that is illegal in Haskell, because the heads of the two instance 
But that is illegal in Haskell, because the heads of the two instance 

declarations are identical. Nevertheless, you can code it up using 
declarations are identical. Nevertheless, you can code it up using 

Line 21:  Line 24:  
this note describes. 
this note describes. 

−  First define an auxiliary class Print': 

+  === Solution 1 (using safer overlapping instances)=== 

+  
+  First define an auxiliary class <hask>Print'</hask>: 

<haskell> 
<haskell> 

−  +  class Print' flag a where 

print' :: flag > a > IO () 
print' :: flag > a > IO () 

−  +  instance (ShowPred a flag, Print' flag a) => Print a where 

print = print' (undefined::flag) 
print = print' (undefined::flag) 

</haskell> 
</haskell> 

−  The main class Print has only one instance, and there is no longer any 
+  The main class <hask>Print</hask> has only one instance, and there is no longer any overlapping. The new class <hask>ShowPred</hask> has no methods, but its instances precisely mirror those of <hask>Show</hask>: 
−  overlapping. The new class ShowPred has no methods, but its instances 

−  precisely mirror those of Show: 

<haskell> 
<haskell> 

−  class ShowPred a flag  a>flag where {} 

+   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 
 Used only if the other 

 instances don't apply 
 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... 

−  
−  
−  data HTrue  Just two 

−  data HFalse  distinct types 

</haskell> 
</haskell> 

−  These instances do make use of overlapping instances, but they do not 

+  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 <hask>(ShowPred ty flag)</hask> always succeeds! If <hask>ty</hask> is a type for which there is a Show instance, flag gets unified to <hask>HTrue</hask>; otherwise flag gets unified to <hask>HFalse</hask>. 

−  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 (nonoverlapping) instances for Print': 
+  Now we can write the (nonoverlapping) instances for <hask>Print'</hask>: 
<haskell> 
<haskell> 

instance (Show a) => Print' HTrue a where 
instance (Show a) => Print' HTrue a where 

Line 55:  Line 61:  
print' _ x = putStrLn "No show method" 
print' _ x = putStrLn "No show method" 

</haskell> 
</haskell> 

−  The trick is to rewrite a constraint (C a) which succeeds 
+  The trick is to rewrite a constraint <hask>(C a)</hask> which succeeds 
−  of fails, into a predicate constraint (C' a flag), which always 
+  of fails, into a predicate constraint <hask>(C' a flag)</hask>, which always 
−  succeeds, but once discharged, unifies flag with either HTrue or 
+  succeeds, but once discharged, unifies flag with either <hask>HTrue</hask> or 
−  HFalse. The desired invariant is 
+  <hask>HFalse</hask>. The desired invariant is 
C a succeeds <> C' a flag unifies flag with HTrue 
C a succeeds <> C' a flag unifies flag with HTrue 

−  Perhaps the most puzzling is the constraint (TypeCast flag HFalse) in 
+  Perhaps the most puzzling is the constraint <hask>(TypeCast flag HFalse)</hask> in the first instance of <hask>ShowPred</hask>. The <hask>TypeCast</hask> constraint and its important role are explained in Section 9 and specifically Appendix D of the full HList paper 
−  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> 
<http://homepages.cwi.nl/~ralf/HList/paper.pdf> 

+  ==== Notes and variations ==== 

−   

+  1. A more `closed world' alternative: write <hask>ShowPred</hask> as follows 

−  == Notes and variations == 

−  
−  
−  1. A more `closed world' alternative: write ShowPred as follows 

<haskell> 
<haskell> 

−  +  class ShowPred a flag  a>flag where {} 

−  +  instance HMember a Showtypes flag => ShowPred a flag 

</haskell> 
</haskell> 

−  There is only one instance of ShowPred and there is no overlapping 
+  There is only one instance of <hask>ShowPred</hask> and there is no overlapping 
−  instances. Here, Showtypes are defined as 
+  instances. Here, <hask>Showtypes</hask> are defined as 
<haskell> 
<haskell> 

−  +  type Showtypes = Int :+: Bool :+: Char :+: ... :+: HNil 

</haskell> 
</haskell> 

−  (Polymorphic types like [a] take more effort, but they too can be handled). 
+  (Polymorphic types like <hask>[a]</hask> take more effort, but they too can be handled). 
−  This is the closed list of types, and HMember is a HList membership 
+  This is the closed list of types, and <hask>HMember</hask> is a <hask>HList</hask> membership checker. <hask>HMember</hask> uses <hask>TypeEq</hask>  and the latter is the only place that 
−  checker. HMember uses TypeEq  and the latter is the only place that 

requires overlapping instances. 
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 

+  2. There is, of course, no check that the instances of <hask>ShowPred</hask> match those of <hask>Show</hask>; you just have to get that right. An alternative, which trades this problem for another, is instead to *replace* by <hask>Show'</hask>, which has the auxiliary flag: 

−  trades this problem for another, is instead to *replace* by Show', 

−  which has the auxiliary flag: 

<haskell> 
<haskell> 

−  +  class Show' a flag  a>flag where 

show :: a > String 
show :: a > String 

 This instance is used only if the others don't apply 
 This instance is used only if the others don't apply 

−  +  instance TypeCast flag HFalse => Show' a flag where 

show = error "urk" 
show = error "urk" 

 These instances are the regular ones 
 These instances are the regular ones 

−  +  instance Show' Int HTrue where 

show = showInt 
show = showInt 

−  +  instance Show' Bool HTrue where 

show = showBool 
show = showBool 

−  +  ...etc... 

</haskell> 
</haskell> 

−  Now we can write the instances for Print': 
+  Now we can write the instances for <hask>Print'</hask>: 
<haskell> 
<haskell> 

instance Show' HTrue a => Print' HTrue a where 
instance Show' HTrue a => Print' HTrue a where 

Line 109:  Line 110:  
print' x = putStrLn "No show method" 
print' x = putStrLn "No show method" 

</haskell> 
</haskell> 

−  The disadvantage here is, of course, that you have to change the Show 
+  The disadvantage here is, of course, that you have to change the <hask>Show</hask> 
class. 
class. 

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

−  of ShowPred: 
+  of <hask>ShowPred</hask>: 
<haskell> 
<haskell> 

instance (ShowPred a flag1, ShowPred b flag2, And flag1 flag2 flag) 
instance (ShowPred a flag1, ShowPred b flag2, And flag1 flag2 flag) 

Line 120:  Line 121:  
class And a b c  a b > c 
class And a b c  a b > c 

−  +  instance And HTrue b b 

−  +  instance And HFalse b HFalse 

</haskell> 
</haskell> 

The HList paper shows many examples of such typelevel programming. 
The HList paper shows many examples of such typelevel programming. 

−  4. Using type families, we'd like to express it like this: 

+  === Solution 2 (using incoherent instances) === 

+  
+  Turn <hask>ShowPred</hask> into a type family: 

+  
<haskell> 
<haskell> 

−  class Print' flag a where 

+   ShowPred is a predicate on types, which says 

−  print' :: a > IO () 

+   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... 

+  </haskell> 

−   ShowWorks is a predicate on types, which says 

+  There's a problem: overlap is not generally allowed for type families!! (The first <hask>ShowPred</hask> instance makes all others redundant.) There is a good reason for this, but it's not helpful here. 

−   which ones are instances of class Show 

−  type family ShowWorks a 

−  type instance ShowWorks a = HFalse 

+  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. 

−  type instance ShowPred Int = HTrue 

−  type instance ShowPred Bool = HTrue 

−  type instance ShowWorks [a] = ShowWorks a 

−  type instance ShowWorks (a,b) = And (ShowWorks a, ShowWorks b) 

−  ...etc... 

−  instance (Show a) => Print' HTrue a where 

+  <haskell> 

−  print' x = putStrLn (show x) 

+  class Print a where 

−  instance Print' HFalse a where 

+  print :: a > IO () 

−  print' x = putStrLn "No show method" 

+  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 

</haskell> 
</haskell> 

−  However, there's a problem: overlap is not allowed at all for type 

−  families!! There is a good reason for this, but it's not helpful 

−  here. 

−   

+  Here, the original formulation is closely mirrored but with the former <hask>ShowPred</hask> 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 <hask>instance (ShowPred a flag, Print' flag a) => Print a</hask>, the tough case is when <hask>ShowPred a flag</hask> doesn't result with flag as HTrue. The catchtherest instance <hask>instance (flag ~ HFalse) => ShowPred a flag</hask>, requires a further constraint to be satisfied. Needing more information, the other constraint, <hask>Print' flag a</hask>, will be checked. Since the first constraint didn't resolve with flag = HTrue, <hask>Print' HTrue a</hask> will not be satisfied. However, <hask>Print' HFalse a</hask> allows us to unify <hask>(flag ~ HFalse)</hask> in the <hask>ShowPred a</hask> constriaint. Consequently the whole constraint is satisfied. 

+  
+  === 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 <hask>ShowPred</hask> like this: 

+  
+  <haskell> 

+  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 

+  </haskell> 

+  
+  There are no incoherent instances anymore. 

+  Any unspecified <hask>ShowPred a</hask> resolves to <hask>ShowPred a</hask> making the specific <hask>Print' HTrue a</hask> instance fail and leaving the catchtherest <hask>Print' flag a</hask> to succeed with <hask>Print' (ShowPred a) a</hask>. 

+  
+  
== Appendix: the sample code == 
== Appendix: the sample code == 

<haskell> 
<haskell> 

−  {# OPTIONS fglasgowexts #} 

+  {# LANGUAGE EmptyDataDecls, 

−  {# OPTIONS fallowundecidableinstances #} 

+  MultiParamTypeClasses, 

−  {# OPTIONS fallowoverlappinginstances #} 

+  ScopedTypeVariables, 

+  FunctionalDependencies, 

+  OverlappingInstances, 

+  FlexibleInstances, 

+  UndecidableInstances #} 

module Main where 
module Main where 
Latest revision as of 13:27, 14 January 2015
Contents
Choosing a typeclass instance based on the context
Oleg Kiselyov and Simon PeytonJones (Apr 2008)
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.
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 (nonoverlapping) 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 rewrite 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>
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 typelevel programming.
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 catchtherest 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.
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 catchtherest Print' flag a
to succeed with Print' (ShowPred a) a
.
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