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

Question

我最近对 ​​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)

所以一个集合要么是空的，要么由一个集合和一个已被证明不在该集合中的附加元素组成。

当我全面检查这个时，我得到了错误

[...] is not strictly positive

用于Insert、Here 和There。我一直在文档中搜索“严格肯定”和总体检查器之类的术语，但我无法弄清楚为什么这种情况特别不是全部(或严格肯定)。有人可以解释一下吗？

自然而然的下一个问题当然是如何“修复”它。我能否以某种方式更改定义，保留其语义，以便进行完整性检查？

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

Answer 1

This SO post解释什么是严格正类型以及它们为何重要。在您的情况下，由于 Not (Elem x xs) 仅表示函数 Elem x xs -> Void，因此“类型定义出现在左侧箭头的一侧”来自。

你能用这样的东西凑合吗？

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)