那么:有什么意义呢？

Question

这种So类型的目的是什么？音译到Agda:

data So : Bool ? Set where
  oh : So true

So将布尔命题提升为逻辑命题.Oury和Swierstra的介绍性论文"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

我在这个答案中使用了这个技巧(它就在{_ : False (m ? 0)}那里).我想这将是不可能写机器描述下的可用版本在这里没有这个简单定义的情况下:

Is-just : ? {?} {A : Set ?} -> Maybe A -> Set
Is-just = T ? isJust

这里T是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