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

Question

我最近对 Idris 进行了很多试验，并提出了以下 "type level definition of a set"：

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。我一直在文档中搜索 "strictly positive" 和总体检查器之类的术语，但我无法弄清楚为什么这种情况特别不是全部（或严格为正）。有人可以解释一下吗？

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

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

Answer 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)

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

Why is this mutually recursive data definition not total and how can I fix it?

idris