所以：有什么意义？ [英] So: what's the point?

问题描述

因此 类型？转换成Agda：

  data所以：Bool→Set其中
哦：真的
  

所以将布尔命题提升到逻辑命题。 Oury和Swierstra的介绍性文章 Power 给出了一个由表格列索引的关系代数的例子。取两个表的乘积要求它们有不同的列，它们使用 So ：

  Schema = List（String×U） -  U是SQL类型的Universe 
 
  -  false如果模式共享任何列名称
不相交：模式 - > ;架构 - > Bool 
 disjoint = ... 
 
 data RA：Schema→Set where 
  -  ... 
产品：∀{s s'}→{So（不相交s s'）}→RA s→RA s'→RA（追加s s'）
  

我习惯于为我想证明我的计划的事情构建证据条款。在 Schema s上构建逻辑关系似乎更自然，以确保不相交：

  Disjoint：Rel Schema _ 
 Disjoint s s'= All（λx  - > x∉cols s）（cols s'）
其中cols = map proj 1 
  

所以与合适的证明项相比似乎有严重的缺点： oh 上的模式匹配不会为您提供任何信息，您可以使用该信息进行另一种类型检查（是否？） - 这意味着因此值无法有效参与交互式证明。与 Disjoint 的计算有用性相对比，它表示为一个证明列表，其中 s'中的每列都不会出现在 s 中。

我不相信规格 So （不相交s s'）比不相交s s <更简单 - 您必须定义布尔不相交函数没有来自类型检查器的帮助 - 无论如何不相交当你想操纵其中包含的证据时为它自己支付。

我也怀疑所以在构建产品。为了给出 So（）的所有值，你仍然需要在 s 和 s'来满足它们实际上是不相交的类型检查器。放弃由此产生的证据似乎是一种浪费。

因此对于代码的作者和用户来说似乎都很笨拙在其中部署。 '所以'，在什么情况下我想要用那么？

解决方案

<如果你已经有一个 b：Bool ，你可以把它变成命题：所以b ，这是一个bit比 b≡true 短。有时（我不记得任何实际的情况），没有必要打扰一个正确的数据类型，这个快速解决方案就足够了。

<因此与适当的
证明项相比似乎有严重的缺点：模式匹配 oh 不会给你任何信息
，你可以用它来做另一个术语类型检查。作为推论，
So 值不能有效地参与交互式证明。
与不相交的计算有用性相对比，其中
表示为一个证明列表，其中 s' > s 。

因此可以为您提供与不相交相同的信息 - 您只需提取它即可。基本上，如果不相交和不相交之间没有不一致，那么你应该可以写一个函数 So（disjoint s） - >不相交的s 使用模式匹配，递归和不可能的情况消除。

然而，如果你稍微调整了定义：

 所以：Bool  - >设置
所以true =⊤
所以false =⊥
  

<$ c $因此成为一个非常有用的数据类型，因为 x：因此，真正的会立即减少到 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 
  

我在这个答案（它是 {_：False（m≟0）} there）。我想如果没有这个简单的定义，就不可能写出这里描述的机器的可用版本：

  Is-just：∀{α} {A：Setα}  - >也许A  - >设置
 Is-just = T∘isJust 
  

其中 T 在Agda的标准库中是 So 。

另外，在实例参数因此 -as-a-data-type可以用作所以 -as-a-constraint：

 打开导入Data.Bool.Base 
打开导入Data.Nat.Base 
打开导入Data.Vec 
 
数据所以：Bool  - >设置其中
哦：真正的
 
实例
 oh-instance：所以真正的
 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 =复制0 
 
 ok：Vecℕ2 
 ok = vec 
 
失败：Vecℕ4 
失败= vec 
  

What is the intended purpose of the So type? Transliterating into Agda:

data So : Bool → Set where
  oh : So true

So lifts a Boolean proposition up to a logical one. Oury and Swierstra's introductory paper The Power of Pi gives an example of a relational algebra indexed by the tables' columns. Taking the product of two tables requires that they have different columns, for which they use 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')

I'm used to constructing evidence terms for the things I want to prove about my programs. It seems more natural to construct a logical relation on Schemas to ensure disjointedness:

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

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 (Does it?) - which would mean 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.

I don't really believe that the specification So (disjoint s s') is simpler to write than Disjoint s s' - you have to define the Boolean disjoint function without help from the type-checker - and in any case Disjoint pays for itself when you want to manipulate the evidence contained therein.

I am also sceptical that So saves effort when you're constructing a Product. In order to give a value of So (disjoint s s'), you still have to do enough pattern matching on s and s' to satisfy the type checker that they are in fact disjoint. It seems like a waste to discard the evidence thus generated.

So seems unwieldy for both authors and users of code in which it's deployed. 'So', under what circumstances would I want to use So?

解决方案

If you already have a b : Bool, you can turn it into proposition: So b, which is a bit shorther than b ≡ true. Sometimes (I don't remember any actual case) there is no need to bother with a proper data type, and this quick solution is enough.

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 does give you the same information as Disjoint — you just need to extract it. Basically, if there is no inconsistency between disjoint and Disjoint, then you should be able to write a function So (disjoint s) -> Disjoint s using pattern matching, recursion and impossible cases elimination.

However, if you tweak the definition a bit:

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

So becomes a really useful data type, because x : So true immediately reduces to tt due to the eta-rule for ⊤. This allows to use So like a constraint: in pseudo-Haskell we could write

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

and if n is in canonical form (i.e. suc (suc (suc ... zero))), then n <=? 3 can be checked by the compiler and no proofs are needed. In actual Agda it is

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

I used this trick in this answer (it is {_ : False (m ≟ 0)} there). And I guess it would be impossible to write a usable version of the machinery decribed here without this simple definition:

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

where T is So in the Agda's standard library.

Also, in the presence of instance arguments So-as-a-data-type can be used as 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

这篇关于所以：有什么意义？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！