Difference between revisions of "Data declaration with constraint"

From HaskellWiki
Jump to: navigation, search
(Added use of GADTs to add a context to data constructors.)
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>.
  
E.g.
+
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 [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.
+
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

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