Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Type signature of parser with existential quantification

In the beginning I had this simple type for a parser:

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


I use the Either for error messages on the left side and the parsed expression with the rest of the tokens on the right side.

This function "unpacks" the parser function.

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

My goal was to make the Parser more general that it does not only take tokens as input. So I used the ExistentialQuantification pragma and changed it to:

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


What I want to know is: What type does the function "parse" have now?


I could not figure it out and it cannot be inferred. GHCi gave this error:

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

Thanks for your help.



EDIT: Thanks a lot for your answers.

The reason I wanted the type to look like "Parser a" because I had seen this in other parsing libraries for example in parsec. But I saw now that this is just a shorthand for parsers that take strings as input.

It makes sense to use "data Parser b a" It was something I also tried earlier, but then I had a strange error in the monad instance for my parser, because I wrote data Parser a b instead:

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)

It gives this error:

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)

Why does it work if you use Parser b a instead of Parser a b? And why do I need this x in Parser x? What does it contain? It would be nice if you could give an example for another monad instance where this variable is used.

like image 585
kindl Avatar asked Sep 12 '14 13:09

kindl


1 Answers

You mean

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

What this actually means becomes clearer if you write the existential in its more rigourous GADT notation:

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

i.e. the constructor Parser is a universally-quantified function taking a ([b] -> ... parser, but returning always a Parser a that knows nothing about what specific b is to be used within. Therefore, this is basically useless: you can't supply a list of b token if you don't know what type that is actually supposed to be!

To make it concrete: parse would be the inverse of Parser; that swaps the quantors so it'd be an existential (duh) function

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

Now, such a type doesn't exist in Haskell, but it's equivalent to having the arguments universal:

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

At this point it's clear you can't use this in any meaningful way: the only inhabitants of forall b. [b] are [] and undefined (and, as Tikhon Jelvis remarks, [undefined], [undefined, undefined], [undefined, undefined, undefined] etc.).


I'm not sure what you actually intend to do with this type, but an existential is definitely not the right approach. Probably you should do

data Parser b a = Parser ([b] -> Either String (a, [b]))
like image 63
leftaroundabout Avatar answered Sep 27 '22 23:09

leftaroundabout