propositionalpromoted相等性之间是否实现了任何连接?

假设我有

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)

最佳答案

是的,可以在两种表示形式之间进行切换(假设:==的实现是正确的),但是需要进行计算。

bool 值本身(it's been erased to a single bit)中不存在您需要的信息;您必须将其恢复。这涉及到询问原始 bool 相等测试的两个参与者(这意味着您必须在运行时保持它们的状态),并使用对结果的了解来消除不可能的情况。重新执行您已经知道答案的计算非常繁琐!

在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)

原则上,我认为您可以使用Singleton在Haskell中进行这项工作,但是为什么要麻烦呢?不要使用 bool 值!

关于haskell - `a :~: b`和 `(a :== b) :~: True`之间有任何联系吗?,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/37923470/

10-12 12:44
查看更多