Idris 解析器组合器 GADT答案

【问题标题】：Idris parser combinator GADTIdris 解析器组合器 GADT
【发布时间】：2016-07-06 13:58:40
【问题描述】：

我目前正致力于在 Idris 中实现一个简单的解析器组合器库，以学习该语言并更好地理解一般类型系统，但在理解如何声明和使用 GADT 时遇到了一些麻烦。我试图制定的解析器数据类型看起来像（在 Haskell 中）：type Parser a = String -> [(a,String)]，来自this 论文。基本上，类型是一个接受字符串并返回列表的函数。

在伊德里斯我有：

data Parser : Type -> Type where
    fail : a -> (String -> [])
    pass : a -> (String -> [(a,String)])

fail 实例是一个总是失败的解析器（即 - 将是一个总是返回空列表的函数），pass 实例是一个消耗一些符号的解析器。将上述内容加载到解释器中时，我收到一个错误，指出List elem 和预期类型Type 之间存在类型不匹配。但是，当我使用:t String -> List Type 检查repl 中解析器的返回类型时，我得到Type，这看起来应该可以工作。

如果有人能很好地解释为什么此数据声明不起作用，或者表示解析器数据类型的更好替代方法，我将不胜感激。

【问题讨论】：

标签： parsing types gadt idris

【解决方案1】：

在定义你的数据类型解析器时，第一行是说这个类型接受一个类型并返回一个类型，在这种情况下它接受一个a并返回一个Parser a。

所以，你的构造函数应该返回Parser a。

类似于List，它接受a 并返回List a。

您当前在构造函数中返回的内容不是 Parser 类型 - 很容易看出，Parser 一词不会出现在右侧。

除此之外，我不确定您将如何最好地表达这一点。但是，已经有一些用 Idris 编写的解析器库，看看这些可能会有所帮助吗？例如，看看这个库列表，解析器是第一个提到的：- Idris libraries

【讨论】：

【解决方案2】：

在 Haskell 中，

type Parser a = String -> [(a,String)]

不创建新类型，它只是类型同义词。你可以在 Idris 中做类似的事情

Parser : Type -> Type
Parser a = String -> List (a, String)

然后将您的帮助定义定义为返回 Parser as 的简单函数：

fail : Parser a
fail = const []

pass : a -> Parser a
pass x = \s => [(x, s)]

【讨论】：

谢谢，这正是我想要的。您能否解释或指出不在类型签名中的 -> 的资源？我不知道箭头可以在类型声明之外使用。
=> 只是 lambda 的 Idris 语法：Haskell 中的 \x -> e 在 Idris 中写为 \x => e。
对不起，应该更清楚。我指的是Parser a = String -> List (a, String)。这一行中的-> 基本上是在创建作为函数的类型吗？ -> 是不是出现在类型签名或函数定义中的意思是一样的？
那个和 Haskell 中的type Parser a = String -> LIst (a, String) 完全一样：它没有定义一个新的类型，它只是引入了一个类型同义词。
棘手的部分是Parser 是一个将Type 作为参数的函数，并作为结果返回另一个Type。这就像 Haskell 中的 * -> * 类型构造函数；但在 Idris 中，它不需要以任何不同于函数的方式定义，例如，一个类型为 Int 并返回 Bool 的参数。