在 Idris 的接口内定义数据类型

Question

我希望创建一类可以证明某个元素是正数或负数或零的类型。我已经创建了一个界面：

interface Signed t where
    data Positive : t -> Type
    data Negative : t -> type
    data IsZero : t -> Type

现在我想为Nat 创建一个实现，但我不知道它的语法。例如，这不起作用：

Signed Nat where
    data Positive : Nat -> Type where
        PosNat : (n : Nat) -> Positive (S n)
    data Negative : Nat -> Type where
        NegNat : Void -> Negative Nat
    data IsZero : Nat -> Type 
        ZZero : IsZero Z

我得到not end of block 错误，其中data Positive 代表实施。但是，省略 data Positive... 行也不起作用。然后伊德里斯说method Positive is undefined。那么如何在接口中实现类型呢？

以下似乎也不起作用：

data NonZero : Signed t => (a : t) -> Type where
    PositiveNonZero : Signed t => Positive a -> NonZero a
    NegativeNonZero : Signed t => Negative a -> NonZero a

伊德里斯说：Can't find implementation for Signed phTy。那么做这一切的正确语法是什么？也许我做错了？我知道Data.So 的存在，但是经过几次实验后，我觉得它很复杂，我更喜欢使用手动定义的证明，这要简单得多。除了Data.So 的文档本身声明它应该与原语一起使用。

Answer 1

看来我终于想通了。这是有效的代码：

interface Signed t where
    data Positive : t -> Type
    data Negative : t -> Type
    data IsZero : t -> Type

data NonZero : t -> Type where
    PositiveNonZero : Signed t => {a : t} -> Positive a -> NonZero a
    NegativeNonZero : Signed t => {a : t} -> Negative a -> NonZero a


data PositNat : Nat -> Type where
    PN : (n : Nat) -> PositNat (S n)

data NegatNat : Nat -> Type where
    NN : Void -> NegatNat n

data ZeroNat : Nat -> Type where
    ZN : ZeroNat Z

Signed Nat where
    Positive n = PositNat n
    Negative n = NegatNat n
    IsZero = ZeroNat


oneNonZero : NonZero (S Z)
oneNonZero = PositiveNonZero (PN 0)

因此，为了实现接口所需的数据类型，您必须单独定义它，然后才说接口所需的类型等于您定义的类型。

至于取决于接口的类型，你只需要指定一个额外的隐式参数来声明a的类型（不幸的是不能写Positive (a : t) -> NonZero a。你实际上似乎需要那个隐式。除此之外，它似乎工作正常，所以我相信这就是问题的答案。当然，欢迎更多了解 Idris 的人提供任何额外的意见。