解析和使用GADT

Question

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

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

Answer 1

@MathematicalOrchid指出你可能不需要GADT,简单的和类型就足够了.您可能有XY问题但我对您的用例了解不足以作出明确的判断.这个答案是关于如何将无类型数据转换为GADT.

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

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

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和可扩展效果都使用GADT作为其中心数据类型.这有助于编译器检查您在编写的代码中是否正确使用了特定于域的语言(在某些情况下允许某些优化).你不太可能在运行时从真实数据中构建FRP网络或monadic效果.