所以：有什么意义？

Question

So类型的预期用途是什么？音译成阿格达：

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看起来比一个“正确”的证明长期有严重的缺点：图案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，你可以把它变成主张：​​，这比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成为一个真正有用的数据类型，因为x : So true立即减少了tt由于对⊤埃塔规则。这允许使用So像一个约束：在伪Haskell中，我们可以写

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

，如果n是规范形式（即suc (suc (suc ... zero))），然后n <=? 3可以被编译器检查，不需要证明。在实际阿格达是

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

我this答案（这是{_ : False (m ≟ 0)}有）使用这一招。我想这是不可能写出机器的可用版本的描述下here没有这个简单的定义：

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

其中T是在阿格达的标准库So。

而且，在实例参数存在So -as-A-数据类型可被用作So -as-A-约束：

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