GADT 的解析和使用

我在编写解析器时遇到了问题。具体来说，我想要不同类型的返回值。例如，我有两种不同的数据类型FA and 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 and paParser。我希望能够解析FA or PA。然而，自从FA and PA是不同的数据类型，我不能执行以下操作 -

inputParser =  faParser
           <|> paParser

我最近了解了 GADT，我认为这可以解决我的问题。因此我做了一个 GADT 和一个eval函数并更改了解析器faParser and 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 and ParsedPA是不同的数据类型吗？例如，解析"PA 17:1_18:1"给我一个类型的值ParsedLipid PA（不只是ParsedLipid正如我所期待的那样）。因此，解析器inputParser仍然不进行类型检查。

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

关于如何解决这个问题有什么建议吗？

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

正如您所注意到的，您的解析函数无法返回ParsedLipid a因为这使得调用上下文可以自由选择a这没有道理；a实际上是由输入数据决定的。并且你不能返回ParsedLipid FA or a ParsedLipid PA，因为输入数据可以是任一类型。

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

data AParsedLipid = forall a. AParsedLipid (ParsedLipid a)

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

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

您可以解压一个AParsedLipid得到你的ParsedLipid返回，并对其进行模式匹配以确定运行时的内容a是 - 要么是FA or 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不能出现在采用 a 的函数的返回类型中AParsedLipid要么出于上述原因。返回类型必须为编译器所知；该技术不允许您定义“具有不同返回类型的函数”。

当你构建一个AParsedLipid，你必须生成足够的证据来说服编译器包装的ParsedLipid是格式良好的。在你的例子中，这归结为解析一个类型良好的PA or FA然后把它包起来。

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

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