haskell - 解析和使用 GADT

我在编写解析器时遇到了问题。具体来说，我想成为不同类型的返回值。例如，我有两种不同的数据类型 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 。我希望能够解析 FA 或 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

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

最佳答案

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

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

因此，从运行时数据构建 GADT 时的标准技巧 - 当您事先不知道索引的类型时 - 是使用 existential quantification 。

data AParsedLipid = forall a. AParsedLipid (ParsedLipid a)

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

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

您可以解压 AParsedLipid 以获取您的 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 也不能出现在采用 AParsedLipid 的函数的返回类型中，原因如上所述。编译器必须知道返回类型；此技术不允许您定义“具有不同返回类型的函数”。

当您构建 AParsedLipid 时，您必须生成足够的证据来说服编译器包装的 ParsedLipid 格式良好。在您的示例中，这归结为解析类型良好的 PA 或 FA 然后将其包装起来。

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

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

关于haskell - 解析和使用 GADT，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/33408943/