`a：〜：b`和`（a：== b）：〜：True`之间是否有联系？ [英] Is there any connection between `a :~: b` and `(a :== b) :~: True`?

问题描述

是否有命题和提升平等吗？

假设我有

Let's say I have

prf :: x :~: y

在某些符号 s的范围内;通过模式匹配它是 Refl ，我可以将它转换为

in scope for some Symbols; by pattern matching on it being Refl, I can transform that into

prf' :: (x :== y) :~: True

像这样：

fromProp :: (KnownSymbol x, KnownSymbol y) => x :~: y -> (x :== y) :~: True
fromProp Refl = Refl

关于另一个方向？如果我尝试

But what about the other direction? If I try

toProp :: (KnownSymbol x, KnownSymbol y) => (x :== y) :~: True -> x :~: y
toProp Refl = Refl

然后我得到的是

• Could not deduce: x ~ y
  from the context: 'True ~ (x :== y)

是的，两个表示之间可以进行（假设执行：== 是正确的），但它需要计算。

The information you need is not present in the Boolean itself (it's been erased to a single bit); you have to recover it. This involves interrogating the two participants of the original Boolean equality test (which means you have to keep them around at runtime), and using your knowledge of the result to eliminate the impossible cases. It's rather tedious to re-perform a computation for which you already know the answer!

您需要的信息不存在于布尔值中（它已被删除到一个位置）;你必须恢复它。这涉及到询问原始布尔相等性测试的两个参与者（这意味着您必须在运行时保持它们），并使用您对结果的了解来消除不可能的情况。重新执行一个你已经知道答案的计算非常繁琐！

在Agda中工作，使用自然代替字符串（因为它们更简单）：

Working in Agda, and using naturals instead of strings (because they're simpler):

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Bool

_==_ : ℕ -> ℕ -> Bool
zero == zero = true
suc n == suc m = n == m
_ == _ = false

==-refl : forall n -> (n == n) ≡ true
==-refl zero = refl
==-refl (suc n) = ==-refl n


fromProp : forall {n m} -> n ≡ m -> (n == m) ≡ true
fromProp {n} refl = ==-refl n

-- we have ways of making you talk
toProp : forall {n m} -> (n == m) ≡ true -> n ≡ m
toProp {zero} {zero} refl = refl
toProp {zero} {suc m} ()
toProp {suc n} {zero} ()
toProp {suc n} {suc m} p = cong suc (toProp {n}{m} p)

原则上，我认为你可以使用单例在Haskell中完成这项工作，但为什么呢？不要使用布尔值！

In principle I think you could make this work in Haskell using singletons, but why bother? Don't use Booleans!

这篇关于`a：〜：b`和`（a：== b）：〜：True`之间是否有联系？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！