How to pattern match on an universally quantified free monad?

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.


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 = ...

Tags:

Haskell