なぜこの相互に再帰的なデータ定義は合計ではないのですか？どのように修正できますか？

Question

は、私はたくさん最近イドリースで実験し、以下の「セットのタイプレベルの定義」を思い付いています：

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ため

厳密に正でないエラーを取得します。私は "厳密に肯定的な"と全体的なチェッカーのような用語についてドキュメントを検索してきましたが、なぜこのケースが全体的（または厳密には正の）ではないのか理解できません。誰かがこれを説明できますか？

自然な次の質問はもちろんそれを "修正"する方法です。私は何とか定義を変更して、その意味を維持することができるので、全体のチェックができますか？

私は実際にこのように見えるように定義する必要はないので（それは結局のところ実験でしかありません）、タイプレベルでSetを表現する別の、慣習的な方法があるかどうかを知ることも面白いでしょう。合計です。

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)