那么：有什么意义呢？

其预期目的是什么So https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/So.idr#L14类型？音译为阿格达：

data So : Bool → Set where
  oh : So true

So将布尔命题提升为逻辑命题。 Oury 和 Swierstra 的介绍性论文圆周率的力量 http://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf给出了由表的列索引的关系代数的示例.求两个表的乘积要求它们具有不同的列，为此它们使用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 and s'为了让类型检查器知道它们实际上是不相交的。丢弃由此产生的证据似乎是一种浪费。

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

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

So与“适当的”相比似乎有严重的缺点 证明术语：模式匹配oh没有给你任何信息 您可以用它进行另一个术语类型检查。作为推论，So价值观不能有效地参与交互式证明。 将此与计算有用性进行对比Disjoint， 哪个 表示为证明列表，其中的每一列s'不 出现在s.

So确实为您提供了相同的信息Disjoint- 你只需要提取它。基本上，如果两者之间没有不一致的话disjoint and 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

and if n是规范形式（即suc (suc (suc ... zero))), then n <=? 3可以由编译器检查，不需要证明。实际上 Agda 是

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

我用了这个技巧this https://stackoverflow.com/a/28589398/3237465答案（这是{_ : False (m ≟ 0)}那里）。我想编写所描述的机器的可用版本是不可能的here https://stackoverflow.com/a/31105948/3237465没有这个简单的定义：

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

where T is 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