Tipo firma del parser con quantificazione esistenziale

Question

All'inizio ho avuto questo semplice tipo per un parser:

data Parser a = Parser ([Token] -> Either String (a, [Token])) 

uso l'entrambi i messaggi di errore sul lato sinistro e l'espressione analizzato con il resto del i token sul lato destro.

Questa funzione "decomprime" la funzione parser.

parse :: Parser a -> [Token] -> Either String (a, [Token]) 
parse (Parser p) = p 

Il mio obiettivo era rendere il parser più generale che non solo prendesse i token come input. Così ho usato l'ExistentialQuantification pragma e cambiato a:

data Parser a = forall b. ([b] -> Either String (a, [b])) 

Quello che voglio sapere è: Che fa la funzione di "analizzare" ho adesso?

Non riuscivo a capirlo e non si può dedurre. GHCi ha fornito questo errore:

Couldn't match type `t' with `[b] -> Either String (t1, [b])' 
    `t' is a rigid type variable bound by 
    the inferred type of parse :: Parser t1 -> t 
    at ParserCombinator.hs:9:1 
In the expression: p 
In an equation for `parse': parse (Parser p) = p 

Grazie per il vostro aiuto.

EDIT: Grazie mille per le vostre risposte.

Il motivo per cui desideravo che il tipo assomigliasse a "Parser a" perché l'avevo visto in altre librerie di analisi, ad esempio in parsec. Ma ora ho visto che questa è solo una scorciatoia per i parser che accettano le stringhe come input.

ha senso utilizzare "BA dati Parser" E 'stato qualcosa che ho provato anche in precedenza, ma poi ho avuto uno strano errore nel caso Monade per il mio parser, perché ho scritto i dati Parser ab invece:

import Control.Monad.Error 

data Parser a b = Parser ([b] -> Either String (a, [b])) 
parse (Parser p) = p 

instance Monad (Parser x) where 
    p >>= f = Parser (\tokens -> do 
     (parsed, rest) <- parse p tokens 
     parse (f parsed) rest) 
    return a = Parser (\ts -> Right (a, ts)) 
    fail b  = Parser (\_ -> Left b) 

si dà questo errore:

ParserCombinator.hs:12:18: 
    Couldn't match type `x' with `b' 
     `x' is a rigid type variable bound by 
      the instance declaration at ParserCombinator.hs:9:24 
     `b' is a rigid type variable bound by 
      the type signature for 
      >>= :: Parser x a -> (a -> Parser x b) -> Parser x b 
      at ParserCombinator.hs:10:5 
    Expected type: a 
     Actual type: x 
    In the first argument of `f', namely `parsed' 
    In the first argument of `parse', namely `(f parsed)' 
    In a stmt of a 'do' block: parse (f parsed) rest 

ParserCombinator.hs:12:26: 
    Couldn't match type `a' with `b' 
     `a' is a rigid type variable bound by 
      the type signature for 
      >>= :: Parser x a -> (a -> Parser x b) -> Parser x b 
      at ParserCombinator.hs:10:5 
     `b' is a rigid type variable bound by 
      the type signature for 
      >>= :: Parser x a -> (a -> Parser x b) -> Parser x b 
      at ParserCombinator.hs:10:5 
    Expected type: [b] 
     Actual type: [a] 
    In the second argument of `parse', namely `rest' 
    In a stmt of a 'do' block: parse (f parsed) rest 

ParserCombinator.hs:13:38: 
    Couldn't match type `a' with `x' 
     `a' is a rigid type variable bound by 
      the type signature for return :: a -> Parser x a 
      at ParserCombinator.hs:13:5 
     `x' is a rigid type variable bound by 
      the instance declaration at ParserCombinator.hs:9:24 
    In the expression: a 
    In the first argument of `Right', namely `(a, ts)' 
    In the expression: Right (a, ts) 

Perché funziona se si utilizza Parser ba invece di Parser ab? E perché ho bisogno di questa x in Parser x? Cosa contiene? Sarebbe bello se potessi dare un esempio per un'altra istanza di monad dove viene usata questa variabile.

Answer 1

Vuoi dire

data Parser a = forall b. Parser ([b] -> Either String (a, [b])) 

Che cosa questo significa in realtà diventa più chiara se si scrive la esistenziale nella sua più rigorosa GADT notazione:

data Parser a where 
    Parser :: forall b. ([b] -> Either String (a, [b])) -> Parser a 

cioè il costruttore Parser è una funzione universalmente quantificata prendendo un ([b] -> ... parser, ma restituendo sempre un Parser a che non sa nulla su quale specifico b deve essere utilizzato all'interno. Pertanto, questo è sostanzialmente inutile: non è possibile fornire un elenco di token b se non si conosce il tipo che in realtà dovrebbe essere!

Per concretizzare: parse sarebbe l'inverso di Parser; che scambia i quantors quindi sarebbe una funzione esistenziale (duh)

parse :: exists b . Parser a -> ([b] -> Either String (a, [b])) 

Ora, un tale tipo non esiste in Haskell, ma è equivalente ad avere gli argomenti universali:

parse :: Parser a -> ((forall b . [b]) -> Either String (a, exists b . [b])) 

A questo punto è chiaro che non è possibile utilizzarlo in alcun modo significativo: gli unici abitanti di forall b. [b] sono [] e undefined (e, come osserva Tikhon Jelvis, [undefined], [undefined, undefined], [undefined, undefined, undefined] ecc.).

---

Non sono sicuro di cosa si intende effettivamente fare con questo tipo, ma un approccio esistenziale non è sicuramente l'approccio giusto. Probabilmente dovresti fare

data Parser b a = Parser ([b] -> Either String (a, [b]))