Ganesh Sittampalam ([info]hsenag) wrote,

Restricted monads in Haskell


I was playing around with restricted monads and came up with the following. It seems really simple, so I was wondering if it's either already known or obvious?

The restricted monad problem is well-known in Haskell. We have some type constructor Foo and some restriction Restr, such that Foo is a monad, but only for contained types that are members of Restr. We can't make Foo an instance of Monad, because in the normal Monad class the types of return and (>>=) are fully polymorphic in the contained type. This in turn blocks us from using do-notation with our "monad". We can get round this using NoImplicitPrelude in GHC, but that's rather messy and means that normal Monads don't work properly in that module.

For concreteness, suppose that Restr is actually Ord, but we could use anything. We'll parameterise over the actual "monad" type, so we don't need to decide on that yet, but I have the usual Set example in mind.

First, let's define a restricted monad class:
class OrdMonad m where
  ordReturn :: Ord a => a -> m a
  ordBind :: (Ord a, Ord b) => m a -> (a -> m b) -> m b

Just to keep things concrete, obviously Set is a member of this:
instance OrdMonad Set where
  ordReturn = Set.singleton
  s `ordBind` f = Set.fold (\v ret -> f v `Set.union` ret) Set.empty s

Now, how can I make a monad from this? Let's start by defining a new type constructor, GADT-style. We intend to apply this type constructor to our OrdMonad instance.
data AsMonad m a where

Now we need some data constructors. Firstly we want to be able to embed "proper" OrdMonads. Here we'll need the full power of the GADTs extension, i.e. restricted return types:
  Embed :: (OrdMonad m, Ord a) => m a -> AsMonad m a

OK so far, but what we're really after is a way to implement return and (>>=). Well, let's take the easy way out:
  Return :: OrdMonad m => a -> AsMonad m a
  Bind :: OrdMonad m => AsMonad m a -> (a -> AsMonad m b) -> AsMonad m b

Now we can implement Monad trivially (I'll ignore fail, but it's not hard to add):
instance OrdMonad m => Monad (AsMonad m) where
  return = Return
  (>>=) = Bind

That was a nice bit of sleight-of-hand, but did it actually help? We've just delayed the problem till later.

Well, actually it does help. "Later", what we'll want to do is get back to our m a type from AsMonad m a. But at this point we can restrict a to being in Ord. What we want is a function unEmbed:
unEmbed :: Ord a => AsMonad m a -> m a

The Embed case of unEmbed is easy:
unEmbed (Embed m) = m

Since we've restricted a, the Return case is easy too:
unEmbed (Return v) = ordReturn v

Now for Bind. Let's split that up into cases based on what the left-hand argument is. Yes, I know this seems like delaying the inevitable, that's how it felt to me too!

If the left-hand argument is Embed, then both a and b are in Ord. So we can call unEmbed recursively and use ordBind:
unEmbed (Bind (Embed m) f) = m `ordBind` (unEmbed . f)

For Return, one of the monad laws applies:
unEmbed (Bind (Return v) f) = unEmbed (f v)

Now for the Bind case. My initial assumption when I was writing this code was that I'd be trapped in a loop, only able to break out the left argument of the inner Bind into yet more cases. Then I realised that actually we can just bring the monad laws to bear again:
unEmbed (Bind (Bind m f) g) = unEmbed (Bind m (\x -> Bind (f x) g)))


And, well, that's it. We can use do-notation on the AsMonad type, and move freely between that and the base type using Embed and unEmbed.
MonadPlus is a simple addition along the same lines:
class OrdMonad m => OrdMonadPlus m where
  ordMZero :: Ord a => m a
  ordMPlus :: Ord a => m a -> m a -> m a

instance OrdMonadPlus Set where
  ordMZero = Set.empty
  ordMPlus = Set.union

data AsMonad m a where
  (...)
  MZero :: OrdMonadPlus m => AsMonad m a
  MPlus :: OrdMonadPlus m => AsMonad m a -> AsMonad m a -> AsMonad m a

instance OrdMonadPlus m => MonadPlus (AsMonad m) where
  mzero = MZero
  mplus = MPlus

unEmbed :: Ord a => AsMonad m a -> m a
(...)
unEmbed MZero = ordMZero
unEmbed (MPlus m1 m2) = ordMPlus (unEmbed m1) (unEmbed m2)
unEmbed (Bind MZero f) = unEmbed MZero
unEmbed (Bind (MPlus m1 m2) f) = unEmbed (MPlus (Bind m1 f) (Bind m2 f))

Here's some test code:
newtype Wrap a = Wrap { unWrap :: a } -- not an Ord even if a is

test1 = unEmbed $ do x <- Embed $ Set.fromList [6, 2, 3]
                     do y <- return (Wrap x)
                        z <- Embed $ Set.fromList [1..2]
                        guard (unWrap y < 5)
                        return (unWrap y + z)
                      `mplus`
                        return 10


One annoyance is that we can't parametrise over typeclasses (at least not nicely), so we can't make AsMonad fully general, instead we need one for each restriction.

Finally, if we are willing and able to add extra constructors to an existing type, I think it should be possible to directly make that type into a Monad using the same approach.

The closest thing I've seen to this before is something like this: http://www.haskell.org/pipermail/haskell-cafe/2007-January/021086.html. It's the same sort of approach, but I don't think it generalises to arbitrary restricted monads in the same way as this.
Tags: haskell

  • Post a new comment

    Error

    Your reply will be screened

    Your IP address will be recorded 

  • 12 comments

Anonymous

March 23 2008, 18:49:38 UTC 4 years ago

Very Nice, and perplexing

I remember wanting this very badly when I was first learning Haskell, since I wanted to create a quantum computation monad.

I'm still quite perpexed by your implementation. I haven't the slightest idea why code like this:

test = unEmbed $ do
    x <- Embed $ Set.fromList [1..5]
    y <- Embed $ Set.fromList [1..5]
    f <- return (+ (x + y))
    return (f 1)


works. Intuitively, that would require an intermediate Set (Int -> Int).

... time passes ...

After staring at this for a while, I am still not sure how it works. But from some experiments I can say that it is probably no better than an abstract:

    newtype SetM a = SetM [a]
         deriving Monad
    embed = SetM . Set.toList . Set.fromList
    unEmbed (SetM xs) = Set.toList (Set.fromList xs)


On account of the following test:

    import Debug.Trace
    test = unEmbed $ do
        x <- Embed $ Set.fromList [-5..5]
        y <- return (x^2)
        trace (show y) $ return y


Which traces 25,16,9,4,1,0,1,4,9,16,25, then returns [0,1,4,9,16,25].

If you have any more insight into why this works, I'd love if you wrote about it.

[info]hsenag

March 24 2008, 17:11:36 UTC 4 years ago

Re: Very Nice, and perplexing

Intuitively, that would require an intermediate Set (Int -> Int).

All it requires is an intermediate AsMonad Set (Int -> Int), and that is easy to make, by construction. The important part of my trick is to ensure that we don't have to convert it into Set (Int -> Int) in unEmbed - instead we just apply the underlying functions.

But from some experiments I can say that it is probably no better than an abstract [list-based implementation]

Yes, you're right, and thank you for pointing that out with a clear example. Efficiency issues were at the back of my mind but I hadn't got round to thinking them through. I actually had in mind when I designed this some other applications where efficiency isn't a concern, but I thought that Set was the most familiar example to present it with. However, the efficiency issue is actually somewhat subtle, and your question has prompted some ideas that I will explore further to see if I can't do better. I'll make another post once I reach a conclusion.

[info]fredrickegerman

March 26 2008, 12:37:55 UTC 4 years ago

Re: Very Nice, and perplexing

[Here via Haskell-café]

The clever thing that this makes clear is that the restrictions on the carrying type (such as Ord for Set) only apply when you're actually using that type. The rest of the time the monad laws permit us to "compose away" all the bind operations. Let me simplify your first example:
y <- Embed $ Set.fromList [1..5]
f <- return (+ (y + y))
return (f 1)

We can make f just vanish by following the monad laws, and that's exactly what the implementation above does:
Embed(Set.fromList [1..5]) >>= \y ->
return (+(y+y)) >>= \f -> return (f 1)

Now we can fold away the Bind of f:
Embed(Set.fromList [1..5]) >>= \y ->
return ((+(y+y)) 1)

The key insight (which I'd missed plenty of times in the past myself) is that we don't need Setty behavior unless the thing on the left hand side of
>>=
is actually a set.

[info]pozorvlak

March 24 2008, 22:16:25 UTC 4 years ago

I too have wanted something like this before, so it's good to see that it's possible - though how you do it is currently completely beyond me! :-) Looks like I'd better read up on GADTs and work my way through this post. As for parametrising AsMonad: could you generate the code with Template Haskell? It doesn't look like you actually need to know about the contents of your typeclass to generate the restricted monad for it.

[info]hsenag

March 25 2008, 05:43:48 UTC 4 years ago

Yes, Template Haskell is probably the way to go, but it feels like admitting defeat!

[info]petermarks.openid.org

July 8 2008, 18:35:58 UTC 3 years ago

Two tricks

Looks like you have found a generalised version of an approach I have just come up with for making Set a Monad.

I think it is worth pointing out that there are two tricks used here:

The first is to defer the evaluation of the bind (and return in your case) until you actually need a value, by which time you can restrict on member type because you are not tied by the Monad class definition.

The second trick is to use the monad associativity law to ensure that binds are always evaluated from the right. This allows the type checker to check the constraint in the final values of a bind chain and not worry about the intermediate ones. You do this during evaluation, I did it when building the tree.

The main problem with this approach, as has been pointed out here, is performance. In the Set example this is better than using lists, but you really want to be able to evaluate from the left.

[info]hsenag

July 8 2008, 20:02:07 UTC 3 years ago

Re: Two tricks

Yeah - I did promise above that I'd post more about efficiency once I'd played around with a bit, but I never really got anywhere because I ran into the issue you mention about evaluating from the left.

I then concluded that what I really wanted was an arrow, but ran into problems handling "first" because working with it requires being able to deduce that the restriction is satisfied for a if it is satisfied for (a, b), which is not in general true, and even for Ord it's tricky to convince the typechecker that it is true.

[info]thesz

October 29 2008, 22:00:39 UTC 3 years ago

Elegant and nice. Thank you very much.

[info]migmit.vox.com

November 5 2008, 17:47:35 UTC 3 years ago

Certainly nice, but it can be done in a different way, which seems more elegant for me:
data OrdRest m a where
    OrdReturn :: a -> OrdRest m a
    OrdBind :: Ord a => m a -> (a -> OrdRest m b) -> OrdRest m b
instance Monad (OrdRest m) where
    return = OrdReturn
    OrdReturn x >>= f = f x
    OrdBind mx g >>= f = OrdBind mx $ \x -> g x >>= f
embed mx = OrdBind mx OrdReturn
unembed (OrdReturn x) = ordReturn x
unembed (OrdBind mx g) = ordBind mx $ unembed . g
Anyway, it's kinda pattern, and being such it shows that Haskell isn't powerful enough.

[info]migmit.vox.com

November 5 2008, 17:49:18 UTC 3 years ago

BTW, types derived for "embed" and "unembed" are
embed :: (Ord a) => m a -> OrdRest m a
unembed :: (OrdMonad m, Ord b) => OrdRest m b -> m b

[info]hsenag

November 5 2008, 18:01:16 UTC 3 years ago

I don't see any particular difference (in terms of elegance or otherwise) between doing the collapsing early or late, but obviously that's a matter of personal taste.

It turns out that it is possible to use associated data types (GHC 6.8+) to abstract over this pattern: http://www.haskell.org/pipermail/haskell-cafe/2008-March/041084.html. I merged this with the above idea to make a general restricted monad library: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/rmonad, but didn't get round to blogging about it.

[info]migmit.vox.com

November 5 2008, 18:58:47 UTC 3 years ago

> I don't see any particular difference (in terms of elegance or otherwise) between doing the collapsing early or late, but obviously that's a matter of personal taste.

Me neither, it's only a matter of program length.

> http://www.haskell.org/pipermail/haskell-cafe/2008-March/041084.html

Wow, missed that somehow. Beautiful.
Create an Account
Forgot your login or password?
Facebook Twitter More login options
English • Español • Deutsch • Русский…