使用存在量化来键入解析器的签名

Question

在开始时,我有一个解析器的简单类型:

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

我在左侧使用Either作为错误消息,在右侧使用其余标记的解析表达式.

此函数"解包"解析器函数.

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

我的目标是使Parser更加通用,它不仅将令牌作为输入.所以我使用了ExistentialQuantification编译指示并将其更改为:

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

我想知道的是:函数"解析"现在有哪些类型？

我无法弄明白,也无法推断出来.GHCi给出了这个错误:

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

谢谢你的帮助.

编辑:非常感谢您的回答.

我之所以希望类型看起来像"Parser a",是因为我在其他解析库中看到过这种情况,例如在parsec中.但我现在看到这只是将字符串作为输入的解析器的简写.

使用"data Parser b a"是有意义的.这也是我之前尝试过的,但后来我的解析器monad实例中出现了一个奇怪的错误,因为我编写了数据Parser ab:

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)

它给出了这个错误:

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)

如果使用Parser ba而不是Parser ab,为什么它可以工作？为什么我需要在Parser x中使用这个x？它包含什么？如果您可以为使用此变量的另一个monad实例提供示例,那将是很好的.

Answer 1

你的意思是

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

如果你用更严格的GADT符号写出存在主义,这实际上意味着什么变得更加清晰:

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

也就是说,构造函数Parser是一个普遍量化的函数,它接受一个([b] -> ...解析器,但总是返回一个对于在其中使用Parser a什么特定b内容一无所知的函数.因此,这基本上是无用的:b如果您不知道实际应该是什么类型,则无法提供令牌列表!

使它具体化:parse将是反过来的Parser; 交换量子因此它是一个存在的(duh)函数

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

现在,Haskell中不存在这样的类型,但它等同于通用的参数:

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

在这一点上很明显,你不能以任何有意义的方式使用:唯一的居民forall b. [b]是[]与undefined(和,因为吉洪Jelvis言论[undefined],[undefined, undefined],[undefined, undefined, undefined]等).

我不确定你真的打算用这种类型做什么,但存在主义肯定不是正确的方法.也许你应该这样做

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