Errori di tipo con tipi Esistenziali in Haskell

Question

Sono in difficoltà con tipi esistenziali nel mio programma. Penso che sto cercando di fare qualcosa di molto ragionevole comunque non posso andare oltre coontrollore dei tipo :(

Ho un tipo di dati che sorta di imita un Monade

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

Ora io a creare un contesto per esso, simile a quello descritto Haskell Wiki article on Zipper, tuttavia utilizzo una funzione invece di una struttura dati per semplicità -

type C o1 o2 = M o1 -> M o2 

Ora quando provo a scrivere una funzione che divide un valore di dati nel suo contesto e subvalue, controllore dei tipi lamenta -

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

errore è -

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) 

Tuttavia, posso lavorare intorno ad esso in questo modo -

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

Perché questa seconda definizione TYPECHECK ma non il primo?

Inoltre, se cerco di convertire ctx a una funzione completa controllando per R, ho di nuovo un errore di TYPECHECK -

ctx (R o) = (id, R o) -- Doesn't typecheck 

Errore -

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) 

Come posso ovviare a questo errore?

Qualsiasi aiuto è apprezzato!

Answer 1

Esaminiamo prima i casi di errore. Entrambi questi falliscono per la stessa ragione, che è più chiaro una volta che si aggiunge nella implicita forall nella firma tipo:

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

vale a dire la funzione non solo deve lavorare per un po 'o1, ma per qualsiasio1.

1. Nel primo caso,

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

   sappiamo che f :: (o2 -> M o) e m :: M o2, per alcuni tipo o2, ma dobbiamo essere in grado di offrire qualsiasi tipo o1, in modo che possiamo Supponiamo che o1 ~ o2.

2. Nel secondo caso,

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

   Qui, sappiamo che o :: o, ma ancora una volta, la funzione deve essere definita per ogni o1, quindi non si può assumere che o ~ o1.

La tua soluzione sembra funzionare solo perché chiama se stessa, simile a una prova induttiva. Ma senza un caso base, è solo un ragionamento circolare, e non è possibile scrivere il caso base per questa funzione, perché non esiste un modo per costruire un M o1 da un per qualsiasi combinazione di o e o1 senza utilizzare un valore inferiore.

Quello che probabilmente dovrai fare, è definire un altro tipo esistenziale per il contesto, invece di usare solo una tupla. Non sono sicuro se funzionerà per le vostre esigenze, ma questo compila , almeno:

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) 

_{Provare a usare un let invece di case per a funny GHC error :)}