如果证明是正交的有帮助吗？

Question

假设我有一个函数

f : Vect m Nat -> Vect n Nat -> {auto _ : Proof m n} -> Foo m n

哪里

data Proof : Nat -> Nat -> Type where
  Eq : Proof x x
  One : Proof 1 _

我可以将

Proof 1 1

制作为

Eq

或

One

。因此，这些不是“正交的”。在更复杂的示例中，我可以使用递归数据构造函数，在其中我可以提供

Constructor1 Constructor2

或

Constructor3 Constructor1

等证明。如果构造函数不正交有什么关系吗？特别是，它是否会妨碍证据搜索？

Answer 1

正交数据构造器使功能实现更简单、更清晰。使用重叠的构造函数，您将在模式之间重复行为，例如

foo : Proof x y -> ?
foo Eq = ?eq
foo One = ?one  -- duplicates `foo (Eq {x = 1})`