因此 类型?转换成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 $ c $因为⊤的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 trueSo 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 nand 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 nI 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 ∘ isJustwhere 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
更多推荐
所以:有什么意义?
发布评论