# GHC/AdvancedOverlap

### From HaskellWiki

< GHC(Difference between revisions)

(fix the whitespace issue consistently through the whole document) |
(→Solution 2 (using incoherent instances)) |
||

(7 intermediate revisions by 3 users not shown) | |||

Line 2: | Line 2: | ||

Oleg Kiselyov and Simon Peyton-Jones (Apr 2008) | Oleg Kiselyov and Simon Peyton-Jones (Apr 2008) | ||

+ | |||

+ | === Problem definition === | ||

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

Line 8: | Line 10: | ||

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 | instance Show a => Print a where | ||

Line 16: | Line 18: | ||

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 | class Print' flag a where | ||

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

− | instance (ShowPred a flag, Print' flag a) => Print a | + | 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> | ||

+ | -- Just two distinct types | ||

+ | -- alternatively use 'True and 'False with -XDataKinds | ||

+ | data HTrue | ||

+ | data HFalse | ||

+ | |||

class ShowPred a flag | a->flag where {} | 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 | + | -- 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 Int HTrue -- These instances must be | ||

instance ShowPred Bool HTrue -- the same as Show's | instance ShowPred Bool HTrue -- the same as Show's | ||

instance ShowPred a flag => ShowPred [a] flag | instance ShowPred a flag => ShowPred [a] flag | ||

− | ...etc... | + | -- ...etc... |

− | + | ||

− | + | ||

− | + | ||

− | + | ||

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

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

<haskell> | <haskell> | ||

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

Line 61: | Line 62: | ||

print' _ x = putStrLn "No show method" | print' _ x = putStrLn "No show method" | ||

</haskell> | </haskell> | ||

− | The trick is to re-write a constraint (C a) which succeeds | + | The trick is to re-write 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 | |

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | 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. | + | 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 | class Show' a flag | a->flag where | ||

Line 113: | Line 104: | ||

...etc... | ...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 120: | Line 111: | ||

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 136: | Line 127: | ||

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

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

− | + | ||

− | + | ||

− | + | ||

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

− | + | ||

− | -- | + | <haskell> |

+ | -- ShowPred is a predicate on types, which says | ||

-- which ones are instances of class Show | -- which ones are instances of class Show | ||

− | type family | + | type family ShowPred a |

− | type instance | + | type instance ShowPred a = HFalse |

type instance ShowPred Int = HTrue | type instance ShowPred Int = HTrue | ||

type instance ShowPred Bool = HTrue | type instance ShowPred Bool = HTrue | ||

− | type instance | + | type instance ShowPred [a] = ShowPred a |

− | type instance | + | type instance ShowPred (a,b) = And (ShowPred a, ShowPred b) |

− | ...etc... | + | -- ...etc... |

+ | </haskell> | ||

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

− | + | ||

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

− | + | ||

+ | <haskell> | ||

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

</haskell> | </haskell> | ||

− | |||

− | |||

− | |||

− | ---- | + | 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 catch-the-rest 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 catch-the-rest <hask>Print' flag a</hask> to succeed with <hask>Print' (ShowPred a) a</hask>. | ||

+ | |||

+ | |||

== Appendix: the sample code == | == Appendix: the sample code == | ||

<haskell> | <haskell> |

## Latest revision as of 13:27, 14 January 2015

## Contents |

## [edit] 1 Choosing a type-class instance based on the context

Oleg Kiselyov and Simon Peyton-Jones (Apr 2008)

### [edit] 1.1 Problem definition

Suppose you have this class:

class Print a where print :: a -> IO ()

a

Show

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.

### [edit] 1.2 Solution 1 (using safer overlapping instances)

First define an auxiliary classPrint'

class Print' flag a where print' :: flag -> a -> IO () instance (ShowPred a flag, Print' flag a) => Print a where print = print' (undefined::flag)

Print

ShowPred

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

(ShowPred ty flag)

ty

HTrue

HFalse

Print'

instance (Show a) => Print' HTrue a where print' _ x = putStrLn (show x) instance Print' HFalse a where print' _ x = putStrLn "No show method"

(C a)

(C' a flag)

HTrue

HFalse

C a succeeds <--> C' a flag unifies flag with HTruePerhaps the most puzzling is the constraint

(TypeCast flag HFalse)

ShowPred

TypeCast

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

#### [edit] 1.2.1 Notes and variations

1. A more `closed world' alternative: writeShowPred

class ShowPred a flag | a->flag where {} instance HMember a Showtypes flag => ShowPred a flag

ShowPred

Showtypes

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

[a]

HMember

HList

HMember

TypeEq

requires overlapping instances.

ShowPred

Show

Show'

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

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"

Show

class.

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

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.

### [edit] 1.3 Solution 2 (using incoherent instances)

TurnShowPred

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

ShowPred

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

ShowPred

instance (ShowPred a flag, Print' flag a) => Print a

ShowPred a flag

instance (flag ~ HFalse) => ShowPred a flag

Print' flag a

Print' HTrue a

Print' HFalse a

(flag ~ HFalse)

ShowPred a

### [edit] 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 rewriteShowPred

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 unspecifiedShowPred a

ShowPred a

Print' HTrue a

Print' flag a

Print' (ShowPred a) a

## [edit] 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