# Difference between revisions of "Data declaration with constraint"

(Added use of GADTs to add a context to data constructors.) |
Artyom Kazak (talk | contribs) m (→Solution: Change the link again) |
||

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

Line 7: | Line 7: | ||

data C a => T a = Cons a | data C a => T a = Cons a | ||

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

− | and I hoped that now the type checker knows | + | |

− | that every value of type <hask>T a</hask> satisfies the type constraint on <hask>a</hask>. | + | and I hoped that now the type checker knows that every value of type <hask>T a</hask> satisfies the type constraint on <hask>a</hask>. |

I like to declare an instance for an type constructor class for the type constructor <hask>T</hask> | I like to declare an instance for an type constructor class for the type constructor <hask>T</hask> | ||

but its methods require type constraints that depend on the particular type constructor <hask>T</hask>. | but its methods require type constraints that depend on the particular type constructor <hask>T</hask>. | ||

− | + | For example: | |

<haskell> | <haskell> | ||

instance Vector T where | instance Vector T where | ||

Line 22: | Line 22: | ||

In Haskell 98, only functions can have type constraints. | In Haskell 98, only functions can have type constraints. | ||

The type constraint of a <hask>data</hask> only refers to the constructors. | The type constraint of a <hask>data</hask> only refers to the constructors. | ||

− | The designers of Haskell 98 do now think, that it was a bad decision to allow constraints on constructors. | + | The designers of Haskell 98 do now think, that it was a bad decision to allow constraints on constructors. GHC as of version 7.2 disallows them by default (turn back on with <code>-XDatatypeContexts</code>). |

== Solution == | == Solution == | ||

− | You could use ghc's [ | + | You could use ghc's [https://wiki.haskell.org/GADTs_for_dummies Generalised Algebraic Data Structures (GADTs)] to add an implicit context to the data constructors: |

+ | |||

+ | <haskell> | ||

+ | data T a where | ||

+ | Cons :: C a => a -> T a | ||

+ | </haskell> | ||

+ | |||

+ | This way, functions using <hask>T</hask> no longer need a constraint. Instead, constructing a <hask>T a</hask> using <hask>Cons</hask> needs a <hask>C a</hask> context, and when something pattern matches a <hask>Cons x</hask>, the context comes with it. | ||

There has been some discussion about whether it is sensible to want this. | There has been some discussion about whether it is sensible to want this. | ||

A Haskell 98 workaround is to use [[multi-parameter type class]]es, where <hask>T a</hask> and <hask>a</hask> are separate arguments. | A Haskell 98 workaround is to use [[multi-parameter type class]]es, where <hask>T a</hask> and <hask>a</hask> are separate arguments. | ||

− | |||

== See also == | == See also == |

## Latest revision as of 23:26, 19 September 2016

## Contents

## Problem

### Question

I have declared

```
data C a => T a = Cons a
```

and I hoped that now the type checker knows that every value of type `T a`

satisfies the type constraint on `a`

.
I like to declare an instance for an type constructor class for the type constructor `T`

but its methods require type constraints that depend on the particular type constructor `T`

.

For example:

```
instance Vector T where
add (Cons x) (Cons y) = Cons (x+y) -- requires Num constraint on type a
```

### Answer

In Haskell 98, only functions can have type constraints.
The type constraint of a `data`

only refers to the constructors.
The designers of Haskell 98 do now think, that it was a bad decision to allow constraints on constructors. GHC as of version 7.2 disallows them by default (turn back on with `-XDatatypeContexts`

).

## Solution

You could use ghc's Generalised Algebraic Data Structures (GADTs) to add an implicit context to the data constructors:

```
data T a where
Cons :: C a => a -> T a
```

This way, functions using `T`

no longer need a constraint. Instead, constructing a `T a`

using `Cons`

needs a `C a`

context, and when something pattern matches a `Cons x`

, the context comes with it.

There has been some discussion about whether it is sensible to want this.

A Haskell 98 workaround is to use multi-parameter type classes, where `T a`

and `a`

are separate arguments.

## See also

- Henning Thielemann in Haskell-Cafe: Context for type parameters of type constructors
- Mark Nicholls in Haskell-Cafe: nice simple problem for someone struggling....