那么，重点是什么呢？ (关于IT技术的问题)

Question

那么，重点是什么呢？ (关于IT技术的问题)

functional-programmingagdadependent-typeidris

26

So类型的预期目的是什么？将其译为Agda：

data So : Bool → Set where
  oh : So true

So将布尔命题提升为逻辑命题。Oury和Swierstra的入门论文The Power of Pi给出了一个以表格列索引的关系代数的示例。取两个表格的乘积需要它们拥有不同的列，对此他们使用了So：

Schema = List (String × U)  -- U is the universe of SQL types

-- false iff the schemas share any column names
disjoint : Schema -> Schema -> Bool
disjoint = ...

data RA : Schema → Set where
  -- ...
  Product : ∀ {s s'} → {So (disjoint s s')} → RA s → RA s' → RA (append s s')

我习惯于为我想证明的有关程序的事情构建证据条款。构建逻辑关系以确保Schema的不相交似乎更自然：

Disjoint : Rel Schema _
Disjoint s s' = All (λ x -> x ∉ cols s) (cols s')
  where cols = map proj₁

So和“proper”证明项相比似乎有严重的劣势：在oh上进行模式匹配不会给你任何信息，你不能使用这些信息来检查另一个术语的类型（是吗？）- 这意味着So值不能有效地参与交互式证明。相比之下，Disjoint的计算效用很有用，它被表示为每一列都不出现在s中的证明列表。

我并不真正相信规范So (disjoint s s')比Disjoint s s'更简单易写 - 您必须在没有类型检查器帮助的情况下定义布尔函数disjoint - 而且无论如何，Disjoint在您想要操作其中包含的证据时会很有用。

我还怀疑当您构造一个Product时，So是否节省了精力。为了给出So (disjoint s s')的值，您仍然需要在s和s'上进行足够的模式匹配，以满足类型检查器它们实际上是不相交的。抛弃这样生成的证据似乎是一种浪费。

So对于部署它的代码的作者和用户来说都不太方便。那么，在什么情况下我会想要使用So呢？

- Benjamin Hodgson

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- effectfully · Accepted Answer

如果您已经有一个b : Bool，您可以将其转换为命题：So b，这比b ≡ true要短一些。有时候（我不记得有任何实际情况），没有必要费心去处理正确的数据类型，这个快速解决方案就足够了。

与“适当的”证明术语相比，“So”似乎存在严重的缺点：在oh上进行模式匹配不会给您任何信息，您无法使用它来使另一个项通过类型检查。作为推论，So值不能有用地参与交互式证明。与此形成对比的是Disjoint的计算实用性，它被表示为每个列在s'中不存在于s中的证明列表。

So确实提供了与Disjoint相同的信息——您只需要提取它。基本上，如果disjoint和Disjoint之间没有矛盾，那么您应该能够编写一个函数So (disjoint s) -> Disjoint s，使用模式匹配、递归和不可能的情况消除。

但是，如果您稍微调整一下定义：

So : Bool -> Set
So true  = ⊤
So false = ⊥

So 变成了一个非常有用的数据类型，因为由于 ⊤ 的 eta-规则，x : So true 立即简化为 tt。这使得可以像使用限制条件一样使用 So ：在伪 Haskell 中，我们可以写作：

forall n. (n <=? 3) => Vec A n

如果n处于规范形式（即suc（suc（suc ... zero））），则编译器可以检查n <=? 3，无需证明。在实际的Agda中，它是这样的：

∀ {n} {_ : n <=? 3} -> Vec A n

我在这里的答案中使用了这个技巧（那里是{_ : False (m ≟ 0)}）。我想，如果没有这个简单的定义，就不可能编写一个可用的机器版本，在这里描述。

Is-just : ∀ {α} {A : Set α} -> Maybe A -> Set
Is-just = T ∘ isJust

其中T在Agda标准库中是So。

此外，在存在实例参数的情况下，So作为数据类型可以用作So作为约束条件：

open import Data.Bool.Base
open import Data.Nat.Base
open import Data.Vec

data So : Bool -> Set where
  oh : So true

instance
  oh-instance : So true
  oh-instance = oh

_<=_ : ℕ -> ℕ -> Bool
0     <= m     = true
suc n <= 0     = false
suc n <= suc m = n <= m

vec : ∀ {n} {{_ : So (n <= 3)}} -> Vec ℕ n
vec = replicate 0

ok : Vec ℕ 2
ok = vec

fail : Vec ℕ 4
fail = vec