4

我在编写解析器时遇到了问题。具体来说，我想成为不同类型的返回值。例如，我有两种不同的数据类型FA并PA代表两种不同的脂质类 -

data FA = ClassLevelFA IntegerMass
        | FA           CarbonChain
        deriving (Show, Eq, Ord)

data PA   = ClassLevelPA       IntegerMass
          | CombinedRadylsPA   TwoCombinedRadyls
          | UnknownSnPA        Radyl Radyl
          | KnownSnPA          Radyl Radyl
          deriving (Show, Eq, Ord)

使用 attoparsec，我构建了解析器来解析脂质速记符号。对于上面的数据类型，我有解析器faParser和paParser. 我希望能够解析 anFA或PA. 但是，由于FA和PA是不同的数据类型，我不能执行以下操作 -

inputParser =  faParser
           <|> paParser

我最近了解了 GADT，我认为这可以解决我的问题。因此，我制作了一个 GADT 和一个eval函数，并更改了解析器faParser和paParser. -

data ParsedLipid a where
  ParsedFA :: FA -> ParsedLipid FA
  ParsedPA :: PA -> ParsedLipid PA

eval :: ParsedLipid a -> a
eval (ParsedFA val) = val
eval (ParsedPA val) = val

这让我很接近，但它看起来好像ParsedFA并且ParsedPA是不同的数据类型？例如，解析"PA 17:1_18:1"给了我一个类型的值ParsedLipid PA（不只是ParsedLipid我所期望的）。因此，解析器inputParser仍然不进行类型检查。

let lipid = use "PA 17:1_18:1"
*Main> :t lipid
lipid :: ParsedLipid PA

关于如何解决这个问题的任何建议？

4

2 回答 2

6

@MathematicalOrchid 指出您可能不需要 GADT，简单的 sum 类型可能就足够了。您可能有XY 问题，但我对您的用例了解不足，无法做出坚定的判断。这个答案是关于如何将无类型数据转换为 GADT。

正如您所注意到的，您的解析函数不能返回 a ParsedLipid a，因为这使调用上下文可以自由选择a没有意义的；a实际上是由输入数据决定的。而且您不能返回 aParsedLipid FA或 a ParsedLipid PA，因为输入数据可能是任何一种类型。

因此，从运行时数据构建 GADT 时的标准技巧（当您事先不知道索引的类型时）是使用存在量化。

data AParsedLipid = forall a. AParsedLipid (ParsedLipid a)

类型参数a出现在右侧AParsedLipid而不是左侧。的值AParsedLipid保证包含格式良好的ParsedLipid，但其精确类型是保密的。存在类型是一个包装器，它帮助我们将杂乱的、无类型的现实世界转换为干净的、强类型的 GADT。

将存在量化的包装器推到系统边缘是一个好主意，您必须与外部世界进行通信。您可以像在核心模型中那样编写带有签名的函数，ParsedLipid a -> a并将它们应用于边缘存在包装器下的数据。您验证您的输入，将其包装在一个存在类型中，然后使用您的强类型模型安全地处理它 - 这不必担心错误，因为您已经检查了您的输入。

您可以解压缩 anAParsedLipid以获取ParsedLipid支持，并对其进行模式匹配以确定在运行时是什么a- 它将是FA或PA.

showFA :: FA -> String
showFA = ...
showPA :: PA -> String
showPA = ...

showLipid :: AParsedLipid -> String
showLipid (AParsedLipid (ParsedFA x)) = "AParsedLipid (ParsedFA "++ showFA x ++")"
showLipid (AParsedLipid (ParsedPA x)) = "AParsedLipid (ParsedPA "++ showPA x ++")"

您会注意到，由于上述原因，a它不能出现在采用 any 的函数的返回类型中。AParsedLipid编译器必须知道返回类型；这种技术不允许您定义“具有不同返回类型的函数”。

当您构建AParsedLipid一个ParsedLipid. 在您的示例中，这归结为解析一个类型良好的PAorFA然后将其包装起来。

parser :: Parser AParsedLipid
parser = AParsedLipid <$> (fmap ParsedFA faParser <|> fmap ParsedPA paParser)

与运行时数据一起使用时，GADT 有点尴尬。ParsedLipid存在包装器有效地擦除了 a - AParsedLipidis isomorphic to中的额外编译时信息Either FA PA。（证明代码中的同构是一个很好的练习。）根据我的经验，GADT 在构建程序方面比在构建数据方面要好得多——它们擅长实现强类型的嵌入式领域特定语言，其类型的索引可以在编译时知道时间。例如，Yampa和extensible-effects两者都使用 GADT 作为其中心数据类型。这有助于编译器检查您在编写的代码中是否正确使用了特定于域的语言（并且在某些情况下允许某些优化）。您不太可能在运行时根据真实数据构建 FRP 网络或单子效应。

于 2015-10-29T09:58:05.863 回答
4

你到底想要什么？

如果你在编译时就知道你想要的是 aFA还是 a PA，那么 GADT 是一个很好的方法。

如果您想在运行时决定解析 anFA或 a PA，您可以使用Either FA PA...

于 2015-10-29T09:04:49.333 回答