How to pattern match on an universally quantified free monad?

user_2659595 0
Viewed 138

I'm wondering if I can write a function isPure :: Free f () -> Bool, which tells you if the given free monad equals Pure () or not. This is easy to do for a simple case, but I can't figure it out for a more complex case where there are constraints on the functor f.

import Control.Monad.Free

-- * This one compiles

isPure :: Free Maybe () -> Bool
isPure (Pure ()) = True
isPure _ = False

-- * This one fails to compile with "Ambiguous type variable ‘context0’ arising from a pattern
-- prevents the constraint ‘(Functor context0)’ from being solved."

{-# LANGUAGE RankNTypes #-}
type ComplexFree = forall context. (Functor context) => Free context ()

isPure' :: ComplexFree -> Bool
isPure' (Pure ()) = True
isPure' _ = False

I can see why specifying the exact type of context0 would be necessary in general, but all I want is to look the coarse-grained structure of the free monad (i.e. is it Pure or not Pure). I don't want to pin down the type because my program relies on passing around some constrained universally quantified free monads and I want this to work with any of them. Is there some way to do this? Thanks!

EDITED to change "existentially quantified" -> "universally quantified"

EDIT: since my ComplexFree type might have been too general, here's a version that more exactly mimics what I'm trying to do.

--* This one actually triggers GHC's warning about impredicative polymorphism...
{-# LANGUAGE GADTs #-}

data MyFunctor context next where
  MyFunctor :: Int -> MyFunctor context next -- arguments not important

type RealisticFree context a = Free (MyFunctor context) a

class HasFoo context where
  getFoo :: context -> Foo

class HasBar context where
  getBar :: context -> Bar

type ConstrainedRealisticFree = forall context. (HasFoo context, HasBar context) => RealisticFree context ()

processRealisticFree :: ConstrainedRealisticFree -> IO ()
processRealisticFree crf = case isPure'' crf of
  True -> putStrLn "It's pure!"
  False -> putStrLn "Not pure!"

isPure'' :: ConstrainedRealisticFree -> Bool
isPure'' = undefined -- ???

(For some more context, this free monad is meant to model an interpreter for a simple language, where a "context" is present. You can think of the context as describing a reader monad that the language is evaluated within, so HasFoo context and HasBar context enforce that a Foo and Bar are available. I use universal quantification so that the exact type of the context can vary. My goal is to be able to identify an "empty program" in this free monad interpreter.)

haskell
2 Answers

First of all, this is not existential quantification. That would look like this:

data ComplexFree = forall context. (Functor context) => ComplexFree (Free context ())

(a syntax I find rather confusing, so I prefer the GADT form

data ComplexFree where
    ComplexFree :: (Functor context) => Free context () -> ComplexFree

, which means the same thing)

You have a universally quantified type here, that is, if you have a value of type ComplexFree (the way you have written it), it can turn into a free monad over any functor you choose. So you can just instantiate it at Identity, for example

isPure' :: ComplexFree -> Bool
isPure' m = case m :: Free Identity () of 
                Pure () -> True
                _       -> False

It must be instantiated at some type in order to inspect it, and the error you see is because the compiler couldn't decide which functor to use by itself.

However, instantiating is not necessary for defining isPure'. Ignoring bottoms1, one of the functors you could instantiate ComplexFree with is Const Void, which means that the recursive case of Free reduces to

f (m a)
  = Const Void (m a)
 ~= Void

that is, it is impossible. By some naturality arguments, we can show that which branch a ComplexFree takes cannot depend on the choice of functor, which means that any fully-defined ComplexFree must be a Pure one. So we can "simplify" to

isPure' :: ComplexFree -> Bool
isPure' _ = True

How boring.

However, I suspect you may have made a mistake defining ComplexFree, and you really do want the existential version?

data ComplexFree where
    ComplexFree :: (Functor context) => Free context () -> ComplexFree

In this case, a ComplexFree "carries" the functor with it. It only works for one functor, and it (and only it) knows what functor that is. This problem is better-formed, and implemented just as you would expect

isPure' :: ComplexFree -> Bool
isPure' (ComplexFree (Pure _)) = True
isPure' _ = False

1 Ignoring bottom is a common practice, and usually not problematic. This reduction strictly increases the information content of the program -- that is, whenever the original version gave a defined answer, the new version will give the same answer. But the new one might "fail to go into an infinite loop" and accidentally give an answer instead. In any case, this reduction can be modified to be completely correct, and the resulting isPure' is just as useless.

user_337960

I'll answer your revamped question here. It turns out that the answer is still basically the same as luqui's: you need to instantiate the polymorphic argument before you can pattern match on it. Thanks to the constraint, you need to use a context type that's an instance of the relevant classes. If it would be inconvenient to use a "real" one, you can easily make a throw-away:

data Gump = Gump Foo Bar

instance HasFoo Gump where
  getFoo (Gump f _) = f

instance HasBar Gump where
  getBar (Gump _ b) = b

That should be fine for this particular case. However, in most similar practical situations, you'll want to instantiate to your real type to get its specialized behavior.

Now you can instantiate the context to Gump and you're good to go:

isPure'' :: ConstrainedRealisticFree -> Bool
isPure'' q = case q :: RealisticFree Gump () of
  Pure _ -> True
  Free _ -> False

The reason you got that error about impredicative types is that you wrote

isPure'' = ...

Higher-rank polymorphic parameters are generally required to be syntactically parameters:

isPure'' q = ...
user_14776670
Related