Difference between revisions of "Data declaration with constraint"
(constraint must be in front of the type) |
(Added use of GADTs to add a context to data constructors.) |
||
(One intermediate revision by one other user 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, |
+ | 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> |
||
+ | but its methods require type constraints that depend on the particular type constructor <hask>T</hask>. |
||
+ | |||
+ | E.g. |
||
+ | <haskell> |
||
+ | instance Vector T where |
||
+ | add (Cons x) (Cons y) = Cons (x+y) -- requires Num constraint on type a |
||
+ | </haskell> |
||
=== Answer === |
=== Answer === |
||
− | + | 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. |
||
Line 17: | Line 26: | ||
== Solution == |
== Solution == |
||
+ | You could use ghc's [http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#gadt-style Generalised Algebraic Data Structures (GADTs)] to add an implicit context to the data constructors. |
||
− | But how can one bake type constraints into a type ? ... |
||
+ | |||
+ | 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. |
||
Revision as of 23:07, 4 June 2013
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
.
E.g.
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.
Solution
You could use ghc's Generalised Algebraic Data Structures (GADTs) to add an implicit context to the data constructors.
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....