Idris

Question

是否可以在 Idris 中为接口创建可在接口本身内使用的可判定属性？

例如 - 假设我们有一个简单的接口 Foo 和一个数据类型 FooTypeEmpty 表示给定的 foo 对象是 'empty '（定义为 'is indexed by two zeros'）的语句：

interface Foo (foo : Nat -> Nat -> Type -> Type) where
    mkEmpty : foo 0 0 a
    isEmpty : (f : foo n m a) -> Bool

data FooTypeEmpty : (Foo foo) => foo n m a -> Type where
    MkFooTypeEmpty : (Foo foo) => (f : foo 0 0 a) -> FooTypeEmpty f

是否可以为 isEmpty 方法提供以下类型？:

isEmpty : (f : foo n m a) -> Dec (FooTypeEmpty f)

也就是说，利用 FooTypeEmpty 以便 isEmpty returns 证明（或矛盾）给定的 foo 对象是 'empty' ?

我用一个 mutual 块试过了，但这不会进行类型检查：

mutual
    interface Foo (foo : Nat -> Nat -> Type -> Type) where
        mkEmpty : foo 0 0 a
        isEmpty : (f : foo n m a) -> Dec (FooTypeEmpty f)

    data FooTypeEmpty : (Foo foo) => foo n m a -> Type where
        FTE : (Foo foo) => (f : foo 0 0 a) -> FooTypeEmpty f

更一般地说：是否可以在所有实现的 valid/required 接口方法中合并证明？

Answer 1

您无法访问您在他的定义中构建的 Foo，isEmpty 需要它。接口只是奇特的数据构造函数，所以你的接口大致相当于：

MkFoo : (foo : Nat -> Nat -> Type -> Type) ->
        (mkEmpty : foo 0 0 a) ->
        (isEmpty : ((f : foo n m a) -> 
            Dec (FooTypeEmpty f {Foo interface=MkFoo foo mkEmpty isEmpty})) ->
        Foo foo

由于 isEmpty 中对 MkFoo 的自我引用，Foo 不会是严格正的，因此不是总的。

所以你必须事先定义证明类型。只需使用相同类型的参数：

data FooTypeEmpty : {foo : Nat -> Nat -> Type -> Type} -> 
                    foo n m a -> Type where
    FTE : {foo : Nat -> Nat -> Type -> Type} ->
          (f : foo 0 0 a) -> FooTypeEmpty f

interface Foo (foo : Nat -> Nat -> Type -> Type) where
    mkEmpty : foo 0 0 a
    isEmpty : (f : foo n m a) -> Dec (FooTypeEmpty f)

data Bar : Nat -> Nat -> Type -> Type where
  Empty : Bar 0 0 a

Foo Bar where
  mkEmpty = Empty
  isEmpty = \Empty => Yes (FTE Empty)

如果你想证明一些关于给接口的函数的事情，只要把它们作为额外的参数（这里mkEmpty）：

data FooTypeEmpty : {foo : Nat -> Nat -> Type -> Type} -> 
                    {mkEmpty : foo 0 0 a} ->
                    foo n m a -> Type where
    FTE : {foo : Nat -> Nat -> Type -> Type} ->
          {mkEmpty : foo 0 0 a} ->
          FooTypeEmpty mkEmpty

interface Foo (foo : Nat -> Nat -> Type -> Type) where
    mkEmpty : foo 0 0 a
    isEmpty : (f : foo n m a) -> Dec (FooTypeEmpty {mkEmpty} f)

data Bar : Nat -> Nat -> Type -> Type where
  Empty : Bar 0 0 a

Foo Bar where
  mkEmpty = Empty
  isEmpty = \Empty => Yes FTE

唯一不能给 FooTypeEmpty 的函数是使用证明本身的函数。

Idris - 通常为接口创建可判定的属性/证明

Idris - create decidable properties/ proofs in general for interfaces