那么：有什么意义呢？

Question

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')

我习惯于为我想证明的关于我的程序的事情构建证据术语。在Schemas 上构建逻辑关系以确保脱节似乎更自然：

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

So 与“正确的”证明术语相比似乎有严重的缺点：oh 上的模式匹配没有给你任何信息，你可以用它来进行另一个术语类型检查（是吗？） -这意味着So 值不能有效地参与交互式证明。将此与Disjoint 的计算有用性进行对比，后者表示为s' 中的每一列都没有出现在s 中的证明列表。

我真的不相信规范 So (disjoint s s') 比 Disjoint s s' 更容易编写 - 你必须在没有类型检查器帮助的情况下定义布尔 disjoint 函数 - 无论如何Disjoint 支付当您想操纵其中包含的证据时，为自己。

我也怀疑So 在构建Product 时是否会省力。为了给出So (disjoint s s') 的值，您仍然需要对s 和s' 进行足够的模式匹配，以满足类型检查器的要求，即它们实际上是不相交的。丢弃由此产生的证据似乎是一种浪费。

So 对于部署它的代码的作者和用户来说似乎都很笨拙。 '那么'，在什么情况下我想使用So？

Answer 1

如果你已经有了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

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

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

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

此外，在存在实例参数的情况下，So-as-a-data-type 可以用作 So-as-a-constraint：

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