那么：有什么意义呢？

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

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

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

与 "proper" 证明术语相比，

So 似乎有严重的缺点：oh 上的模式匹配不会为您提供任何可以用来制作其他术语类型的信息-check（是吗？）——这意味着 So 值不能有效地参与交互式证明。将此与 Disjoint 的计算有用性进行对比，后者表示为 s' 中的每一列未出现在 s.

中的证明列表

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

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

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

Answer 1

如果你已经有一个b : Bool，你可以把它变成命题：So b，比b ≡ true短一点。有时（我不记得任何实际情况）不需要为正确的数据类型而烦恼，这个快速解决方案就足够了。

So seems to have serious disadvantages compared to a "proper" proof-term: pattern matching on oh doesn't give you any information with which you could make another term type-check. As a corollary, So values can't usefully participate in interactive proving. Contrast this with the computational usefulness of Disjoint, which is represented as a list of proofs that each column in s' doesn't appear in s.

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

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

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

So 成为一种非常有用的数据类型，因为 x : So true 由于 ⊤ 的 eta 规则立即减少为 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 answer (it is {_ : False (m ≟ 0)} there). And I guess it would be impossible to write a usable version of the machinery decribed 中使用了这个技巧，但没有这个简单的定义：

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

那么：有什么意义呢？

So: what's the point?

functional-programming

agda

dependent-type

idris