Haskell type constraint

Question

I'm struggling with the haskell type system. Basically what I'm trying to do is define a data structure (cf Ast data type in the code sample) that represents a monad (it could be something else). This type is parameterized by a and there is no constraint on it. My issue is when I want to introspect this type, I might need some constraints on the type parameter, for instance:

{-# LANGUAGE GADTs #-}

import Control.Monad

data Ast a where
    Bind :: Ast a -> (a -> Ast b) -> Ast b
    Return :: a -> Ast a

instance Functor Ast where
    fmap = liftM

instance Applicative Ast where
    pure = Return
    (<*>) = ap

instance Monad Ast where
    (>>=) = Bind

instance Show a => Show (Ast a) where
    show (Bind x y) = "bind " ++ {- begin error -} show x {- end error -} 
    show (Return y) = "return " ++ show y

This yields the following error:

Could not deduce (Show a1) arising from a use of ‘show’
from the context (Show a)
  bound by the instance declaration at src/Main.hs:21:10-31
Possible fix:
  add (Show a1) to the context of the data constructor ‘Bind’
In the second argument of ‘(++)’, namely ‘show x’
In the expression: "bind " ++ show x
In an equation for ‘show’: show (Bind x y) = "bind " ++ show x

And that makes sense, the compiler doesn't know that x is an instance of Show. My question is could I express this constraint? Ideally I'd like to have the constraint only on my Show instance but I also tried to add the Show constraint in the Ast constructor:

data Ast a where
    Bind :: (Show a, Show b) => Ast a -> (a -> Ast b) -> Ast b
    Return :: a -> Ast a

And I get this error:

No instance for (Show a) arising from a use of ‘Bind’
Possible fix:
  add (Show a) to the context of
    the type signature for (>>=) :: Ast a -> (a -> Ast b) -> Ast b
In the expression: Bind
In an equation for ‘>>=’: (>>=) = Bind
In the instance declaration for ‘Monad Ast’

I understand the Show constraint should be added at the monad class type definition level.

Any idea how to manage that?

Thanks.

If you really want to make a monad with restrictions, package rmonad could help. — Petr

dfeuer dfeuer · Accepted Answer · 2016-01-01T20:10:52

You can't have it both ways.

The Functor class, of which Monad is a subclass, insists on full polymorphism (fmap can be applied to functions with arbitrary return types). So you can't restrict things on that end. You also can't restrict them within Bind because >>= must accept arbitrary left operands.

An alternative is to use different notions of functor and monad (look up "indexed monad"). The following code is completely untested.

{-# Language DataKinds, Gadts, KindSignatures #-}

-- (type-level) free magma
data FM a = Leaf | Bin (FM a) a (FM a)

data Ast :: FM * -> * -> * where
  Return :: a -> Ast 'Leaf a
  Bind :: Ast ts a -> (a -> Ast us b) -> Ast ('Bin ts a us) b

class Showy (mag :: FM *) where
  showy :: Show a => Ast mag a -> String

instance Showy 'Nil where
  showy (Return a) = "Return " ++ show a

instance (Showy as, Show b) => Showy ('Bin as b cs) where
  showy (Bind m f) = "Bind " ++ showy m

instance (Showy as, Show b) => Show (Ast as b) where
  show = showy

Haskell type constraint

1 Answers