Escriba errores con tipos existenciales en Haskell

Question

Estoy luchando con tipos existenciales en mi programa. Creo que estoy tratando de hacer algo muy razonable, sin embargo yo no puedo pasar de la typechecker :(

tengo un tipo de datos de este tipo imita una Mónada

data M o = R o | forall o1. B (o1 -> M o) (M o1) 

Ahora crear un contexto para que, de forma similar al descrito en el Haskell Wiki article on Zipper, sin embargo utilizo una función en lugar de una estructura de datos para la simplicidad -

type C o1 o2 = M o1 -> M o2 

ahora cuando trato de escribir una función que divide un valor de datos en su contexto y subvalue, la typechecker se queja -

ctx :: M o -> (M o1 -> M o, M o1) 
ctx (B f m) = (B f, m) -- Doesn't typecheck 

error es -

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) 

Sin embargo, puedo trabajar alrededor de ella como tal -

ctx (B f m) = let (c,m') = ctx m in ((B f) . c, m') -- OK 

¿Por qué este segundo typecheck definición, pero no el primero?

También, si lo intento de convertir ctx a una función completa mediante la comprobación de R, I nuevamente sale un error typecheck -

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) 

¿Cómo puedo solucionar este ¿error?

¡Se agradece cualquier ayuda!

Answer 1

Primero veamos los casos que fallan. Ambos fracasan por la misma razón, que es más claro una vez que se agrega en la implícita forall en la firma Tipo:

ctx :: forall o o1. M o -> (M o1 -> M o, M o1) 

es decir, su función no sólo debe trabajar por un poco de o1, pero para cualquiero1.

1. En el primer caso,

   ctx (B f m) = (B f, m) 
   

   sabemos que f :: (o2 -> M o) y m :: M o2, por algunos tipo o2, pero tenemos que ser capaces de ofrecer cualquier tipo o1, por lo que podemos supongamos que o1 ~ o2.

2. En el segundo caso,

   ctx (R o) = (id, R o) 
   

   Aquí, sabemos que o :: o, pero de nuevo, la función tiene que ser definido por cualquier o1, por lo que no se puede asumir que o ~ o1.

Su solución solo parece funcionar porque se está llamando a sí misma, similar a una prueba inductiva. Pero sin un caso base, que es sólo un razonamiento circular, y no se puede escribir el caso base para esta función, porque no hay manera de construir un M o1 de un M o para cualquier combinación de o y o1 sin necesidad de utilizar un valor inferior.

Lo que es probable que tengas que hacer, es definir otro tipo existencial para el contexto, en lugar de utilizar sólo una tupla. No estoy seguro si va a trabajar para sus necesidades, pero esto compila , al menos:

data Ctx o = forall o1. Ctx (M o1 -> M o) (M o1) 

ctx :: M o -> Ctx o 
ctx (B f m) = case ctx m of Ctx c m' -> Ctx (B f . c) m' 
ctx (R o) = Ctx id (R o) 

_{Trate de usar un let en lugar de case para a funny GHC error :)}