functional-programming - 所以 : what's the point?

Question

So 的预期目的是什么？类型？音译为Agda:

data So : Bool → Set where
  oh : So true

So将 bool 命题提升为逻辑命题。 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 上构建逻辑关系似乎更自然。 s 以确保脱节:

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

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

我真的不相信规范 So (disjoint s s')比 Disjoint s s' 写起来更简单- 你必须定义 bool 值 disjoint在没有类型检查器帮助的情况下运行 - 无论如何Disjoint当你想要操纵其中包含的证据时，它会物有所值。

我也怀疑 So构建 Product 时省力.为了给出 So (disjoint s s') 的值，你还是要在s上做足够多的模式匹配和 s'以满足类型检查器，它们实际上是不相交的。丢弃由此产生的证据似乎是一种浪费。
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立即减少到 tt由于 ⊤ 的 eta 规则.这允许使用 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是 So在 Agda 的标准库中。

此外，在存在实例参数的情况下 So -as-a-data-type 可以用作 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