0

我正在尝试将少量 PureScript 代码移植到 Idris，在其中可以应用依赖类型，但偶然发现在case依赖类型内部使用不起作用的情况。

由于这是有效的（简化的）：

data ValidInvoice3 : (ft : FeeType) -> Type where
  MkVI3 : ValidInvoice3 ft

为什么以下不进行类型检查？

-- BROKEN
data ValidInvoice4 : (ft : FeeType) -> Type where
  MkVI4 : case ft of
            FeeMarkupHidden => ValidInvoice4 ft -- simplified;
            FeeExplicit     => ValidInvoice4 ft -- more elaborate example below

如果您对我为什么要研究这个感兴趣：这里有一些更详细的示例代码：

module DependentWithCase

data FeeType = FeeMarkupHidden | FeeExplicit

data Fee : (ft : FeeType) -> Type where
  MkFee : Fee ft -- simplified

data ValidArticle : (ft : FeeType) -> Type where
  MkVA : ValidArticle ft -- simplified

现在是如何成功编写“发票”的依赖类型，在 FeeType 上建立索引，使用case表达式来决定是否将费用作为显式参数添加（在实际代码中，在这种情况下，“文章”类型有一个“标记”部分，我在这里省略了；这样我可以确定“标记”只开票一次）：

data ValidInvoice : (ft : FeeType) -> Type where
  MkVI : ValidArticle ft ->
         case ft of FeeMarkupHidden => Unit; FeeExplicit => Fee ft;
         ->
         ValidInvoice ft

因此，您会看到发票数据类型（在实际代码中，文章类型也是如此）取决于费用类型。

但与其在构造函​​数中使用 case 表达式，我更愿意让它看起来像这种类型的同义词（当然没有构造函数；但这本质上是它在 PureScript 代码中的读取方式，而是使用具有单独构造函数的 sum 类型，而不是此处的依赖类型，通过 FeeType 进行索引）。这对我来说更具可读性（尤其是在实际代码中）。

ValidInvoice2 : (ft : FeeType) -> Type
ValidInvoice2 FeeMarkupHidden = ValidArticle FeeMarkupHidden -> Unit            -> ValidInvoice2 FeeMarkupHidden
ValidInvoice2 FeeExplicit     = ValidArticle FeeExplicit     -> Fee FeeExplicit -> ValidInvoice2 FeeExplicit

那么为什么不ValidInvoice4进行类型检查呢？我写错了吗？或者期待一些无法工作的东西？

4

1 回答 1

0

似乎 Idris 没有注意到您的 case 语句的任何一个分支都会导致ValidInvoice4. 它也不评估处于类似位置的函数。你几乎总是可以做一些稍微不同的事情并得到相同的结果。

查看您正在尝试完成的工作，我建议您制作Fee一个FeeType-indexed Maybe- 这可以简化整个事情：

data FeeType = FeeMarkupHidden | FeeExplicit

data Fee : (ft : FeeType) -> Type where
    HidFee : Fee FeeMarkupHidden
    ExFee : Nat {- or w/e -} -> Fee FeeExplicit

data ValidArticle : (ft : FeeType) -> Type where
    MkVA : ValidArticle ft

data ValidInvoice : (ft : FeeType) -> Type where
  MkVI : ValidArticle ft -> Fee ft -> ValidInvoice ft
于 2019-02-08T20:17:34.027 回答