GADT的解析和使用



我在编写解析器时遇到了一个问题。具体来说,我想成为不同类型的返回值。例如,我有两种不同的数据类型FAPA来表示两个不同的脂质类别-

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,我构建了解析器来解析脂质简写符号。对于上面的数据类型,我有解析器faParserpaParser。我希望能够解析FAPA。然而,由于FAPA是不同的数据类型,我无法执行以下操作-

inputParser =  faParser
           <|> paParser

我最近了解了GADT,我认为这会解决我的问题。因此,我去做了一个GADT和一个eval函数,并更改了解析器faParserpaParser

data ParsedLipid a where
  ParsedFA :: FA -> ParsedLipid FA
  ParsedPA :: PA -> ParsedLipid PA
eval :: ParsedLipid a -> a
eval (ParsedFA val) = val
eval (ParsedPA val) = val

这让我很接近,但似乎ParsedFAParsedPA是不同的数据类型?例如,解析"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,这是没有意义的;CCD_ 20实际上是由输入数据确定的。并且不能返回ParsedLipid FAParsedLipid PA,因为输入数据可能是任意一种类型。

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

data AParsedLipid = forall a. AParsedLipid (ParsedLipid a)

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

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

您可以解压缩AParsedLipid以取回ParsedLipid,并在此基础上进行模式匹配以在运行时确定a是什么——它将是FAPA

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是良好的形式。在您的示例中,这归结为解析一个类型良好的PAFA,然后对其进行封装。

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

GADT在与运行时数据一起使用时有点尴尬。存在包装器有效地擦除了ParsedLipid中的额外编译时信息——AParsedLipid同构于Either FA PA。(证明代码中的同构是一个很好的练习。例如,Yampa和可扩展效果都使用GADT作为它们的中心数据类型。这有助于编译器检查您在编写的代码中是否正确使用了特定于领域的语言(在某些情况下允许进行某些优化)。你不太可能在运行时根据真实世界的数据构建FRP网络或单元效应。

您到底想要什么?

如果您在编译时知道是想要FA还是PA,那么GADT是一个很好的方法。

如果您想在运行时决定解析FAPA,可以使用。。。Either FA PA

最新更新