[Haskell-cafe] forcing a type constraint on data

[Erik Hesselink]

On Sun, Jan 2, 2011 at 01:37, Mathijs Kwik <bluescreen303 at gmail.com> wrote:
> The original package
> http://hackage.haskell.org/packages/archive/reaction-logic/2010.11.17/doc/html/Data-Reactor.html
> has a constructor function (mkReactor) with exactly the constraints
> I'm after. However, the constraint is just on this constructor
> function, not on the data itself.
> All functions I write are inferred as "Reactor (State s) c", while the
> use of that constructor ensures that s == c.

The haskell98 way to do this, is to restate the constraints in every
function where you use your data type. So every function that uses a
"Reactor m c" and needs the fact that it has a "MonadState c m", needs
this in its context: "MonadState c m => Reactor m c -> ..."

Using the GADTs language extension, you can create a constructor that
contains the proof that the type contained is a member of a certain
type class. For example:

data HasShow a where
  HasShow :: (Show a) => a -> HasShow a

newShow :: HasShow a -> String
newShow (HasShow x) = show x

Note that newShow doesn't need a "Show a" constraint.

Erik