在`a:〜:b`和`(a:== b):〜:True`之间是否有任何联系？

Question

在命题和促进平等之间是否存在任何联系？

让我说我有

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

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

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

在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中完成这项工作,但为什么要这么麻烦？不要使用布尔人!