为什么这个相互递归的数据定义不完整，我该如何解决？-Java 学习之路

我最近正在尝试使用Idris，并提出了以下“类型级别定义”：

mutual
  data Set : Type -> Type where
    Empty : Set a
    Insert : (x : a) -> (xs : Set a) -> Not (Elem x xs) -> Set a

  data Elem : (x : a) -> Set a -> Type where
    Here : Elem x (Insert x xs p)
    There : Elem x xs -> Elem x (Insert y xs p)

因此，一个集合是空的，或者它由一个集合和一个已证明不在该集合中的附加元素组成 .

当我总体检查这个时，我得到了错误

[...]并非严格正面

对于 Insert ， Here 和 There . 我一直在搜索文档中的"strictly positive"和整体检查器等术语，但我无法弄清楚为什么这个案例特别不完全（或严格来说是正面的） . 有人可以解释一下吗？

那么自然的下一个问题当然是如何“修复”它 . 我可以以某种方式更改定义，保持其语义，以便它进行全面检查吗？

因为我真的不需要这个定义看起来像这样（毕竟它只是一个实验），所以知道是否有另一种，某种更惯用的方式来表示类型级别的集合也是很有趣的 .

1 回答

1
This SO post解释了严格的正面类型及其重要性 . 在你的情况下，因为 Not (Elem x xs) 只是一个函数 Elem x xs -> Void ，这就是"type being defined occurring on the left-hand side of an arrow"来自的地方 .

你能用这样的东西做吗？
```
mutual
  data Set : Type -> Type where
    Empty : Set a
    Insert : (x : a) -> (xs : Set a) -> NotElem x xs -> Set a

  data NotElem : (x : a) -> Set a -> Type where
    NotInEmpty : NotElem x Empty
    NotInInsert : Not (x = y) -> NotElem x ys -> NotElem x (Insert y ys p)
```
回复于 2024-05-15T01:12:40+08:00

为什么这个相互递归的数据定义不完整，我该如何解决？

1 回答

相关问题