`a :~: b` 和 `(a :== b) :~: True` 之间有什么联系吗? [英] Is there any connection between `a :~: b` and `(a :== b) :~: True`?

问题描述

propositional 和 促进平等?

假设我有

prf :: x :~: y

在一些Symbol的范围内；通过模式匹配是 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)

推荐答案

是的，在两种表示之间切换是可能的(假设 :== 的实现是正确的)，但它需要计算.

Yes, going between the two representations is possible (assuming the implementation of :== is correct), but it requires computation.

您需要的信息不存在于布尔值本身中(它已被删除为一位);你必须恢复它.这涉及询问原始布尔相等性测试的两个参与者(这意味着您必须在运行时保留他们)，并使用您对结果的了解来消除不可能的情况.重新执行一个你已经知道答案的计算是相当乏味的！

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屋！