Warum ist diese wechselseitig rekursive Datendefinition nicht vollständig und wie kann ich sie beheben?

Question

Ich experimentiere viel in letzter Zeit mit Idris und kam mit dem folgenden „Typ-Ebene Definition eines Satzes“ up:

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) 

So ein Satz ist entweder leer oder es besteht aus einem Satz und einem zusätzlichen Element, das ist bewiesen, dass sie nicht schon in diesem Set sind.

Wenn ich diese Gesamtheit prüfen, erhalte ich die Fehler

[...] nicht streng positiv ist

für Insert, Here und There. Ich habe die Dokumentation nach Begriffen wie "strikt positiv" und dem Totalitätsprüfer im Allgemeinen durchsucht, aber ich kann nicht herausfinden, warum dieser Fall insbesondere nicht vollständig (oder streng positiv) ist. Kann jemand das erklären?

Die natürliche nächste Frage ist dann natürlich, wie man es "repariert". Kann ich die Definition irgendwie ändern, indem ich ihre Semantik beibehalte, damit sie vollständig überprüft wird?

Da ich die Definition nicht wirklich brauche (es ist nur ein Experiment), wäre es auch interessant zu wissen, ob es eine andere, irgendwie idiomatische Art gibt, Sets auf der Typ-Ebene darzustellen ist total.

Answer 1

This SO post erklärt, was streng positive Typen sind und warum sie wichtig sind. In Ihrem Fall, da Not (Elem x xs) einfach eine Funktion bedeutet, kommt hier der "Typ, der auf der linken Seite eines Pfeils definiert ist".

Können Sie mit so etwas auskommen?

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)