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