# Difference between revisions of "GHC/AdvancedOverlap"

m (→Notes and variations) |
m (→Notes and variations) |
||

Line 187: | Line 187: | ||

class Print' flag a where |
class Print' flag a where |
||

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

− | instance |
+ | instance Show a => Print' HTrue a where |

print' _ x = putStrLn (show x) |
print' _ x = putStrLn (show x) |
||

instance Print' flag a where |
instance Print' flag a where |

## Revision as of 19:40, 3 October 2013

## Choosing a type-class instance based on the context

Oleg Kiselyov and Simon Peyton-Jones (Apr 2008)

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.

First define an auxiliary class Print':

```
class Print' flag a where
print' :: flag -> a -> IO ()
instance (ShowPred a flag, Print' flag a) => Print a
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:

```
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...
data HTrue -- Just two
data HFalse -- distinct types
-- alternatively use 'True and 'False wth -XDataKinds
```

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>

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

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

```
class Print' flag a where
print' :: a -> IO ()
instance Print' (ShowWorks a) a => Print a
print = print'
-- ShowWorks is a predicate on types, which says
-- which ones are instances of class Show
type family ShowWorks a
type instance ShowWorks a = HFalse
type instance ShowWorks Int = HTrue
type instance ShowWorks 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
print' x = putStrLn (show x)
instance Print' HFalse a where
print' x = putStrLn "No show method"
```

There's a problem: overlap is not generally allowed for type families!! (Thie first ShowPred instance makes all others redundant.) There is a good reason for this, but it's not helpful here. However, as of GHC 7.8, closed type families are available. For more details, see Type families#Closed family simplification which makes the above intent possible with something like:

```
type family ShowWorks a where
ShowWorks Int = HTrue
ShowWorks Bool = HTrue
ShowWorks [a] = ShowWorks a
ShowWorks (a,b) = And (ShowWorks a, ShowWorks b)
ShowWorks a = HFalse
```

Without closed families, a solution is still available which mirrors the original program from section 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.

For the type family based formulation, 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`

.

## 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
```