I am struggling with existential types in my program. I think I'm trying to do something very reasonable however I cannot get past the typechecker :(
I have a datatype that sort of mimics a Monad
data M o = R o | forall o1. B (o1 -> M o) (M o1)
Now I create a Context for it, similar to that described in Haskell Wiki article on Zipper, however I use a function instead of a data structure for simplicity -
type C o1 o2 = M o1 -> M o2
Now when I try to write a function that splits a data value into its context and subvalue, the typechecker complains -
ctx :: M o -> (M o1 -> M o, M o1)
ctx (B f m) = (B f, m) -- Doesn't typecheck
Error is -
Couldn't match type `o2' with `o1'
`o2' is a rigid type variable bound by
a pattern with constructor
B :: forall o o1. (o1 -> M o) -> M o1 -> M o,
in an equation for `ctx'
at delme1.hs:6:6
`o1' is a rigid type variable bound by
the type signature for ctx :: M o -> (M o1 -> M o, M o1)
at delme1.hs:6:1
Expected type: M o2
Actual type: M o1
In the expression: m
In the expression: (B f, m)
However, I can work around it like so -
ctx (B f m) = let (c,m') = ctx m in ((B f) . c, m') -- OK
Why does this second definition typecheck but not the first one?
Also, if I try to convert ctx
to a complete function by checking for R, I again get a typecheck error -
ctx (R o) = (id, R o) -- Doesn't typecheck
Error -
Couldn't match type `o' with `o1'
`o' is a rigid type variable bound by
the type signature for ctx :: M o -> (M o1 -> M o, M o1)
at delme1.hs:7:1
`o1' is a rigid type variable bound by
the type signature for ctx :: M o -> (M o1 -> M o, M o1)
at delme1.hs:7:1
In the first argument of `R', namely `o'
In the expression: R o
In the expression: (id, R o)
How can I work around this error?
Any help is appreciated!
Let's look at the failing cases first. Both of these fail for the same reason, which is clearer once you add in the implicit
forall
in the type signature:i.e. your function must not only work for a some
o1
, but for anyo1
.In your first case,
we know that
f :: (o2 -> M o)
andm :: M o2
, for some typeo2
, but we have to be able to offer any typeo1
, so we can't assume thato1 ~ o2
.In the second case,
Here, we know that
o :: o
, but again, the function has to be defined for anyo1
, so we can't assume thato ~ o1
.Your workaround only seems to work because it's calling itself, similar to an inductive proof. But without a base case, it's just circular reasoning, and you cannot write the base case for this function, because there is no way to construct an
M o1
from anM o
for any combination ofo
ando1
without using a bottom value.What you'll probably need to do, is to define another existential type for the context, instead of using just a tuple. Not sure if it'll work for your needs, but this compiles1, at least:
1 Try using a
let
instead ofcase
for a funny GHC error :)