`a :~: b` 和 `(a :== b) :~: True` 之间有什么联系吗？

Question

propositional and promoted等式之间有什么联系吗？

假设我有

prf :: x :~: y

在某些 Symbol 的范围内；通过对其进行模式匹配 Refl，我可以将其转换为

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

像这样：

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

但是另一个方向呢？如果我尝试

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

那么我得到的就是

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

Answer 1

是的，可以在两种表示之间切换（假设 :== 的实现是正确的），但它需要计算。

布尔值本身不存在您需要的信息 (it's been erased to a single bit)；你必须恢复它。这涉及询问原始布尔相等性测试的两个参与者（这意味着您必须在运行时保留它们），并使用您对结果的了解来消除不可能的情况。已经知道答案的计算，重新计算是相当乏味的！

在 Agda 中工作，并使用自然数而不是字符串（因为它们更简单）：

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 中完成这项工作，但何必呢？不要使用布尔值！

`a :~: b` 和 `(a :== b) :~: True` 之间有什么联系吗？

Is there any connection between `a :~: b` and `(a :== b) :~: True`?

haskell

equality

dependent-type

type-level-computation

singleton-type