`a：〜：b`と`（a：== b）：〜：True`の間には何らかの関係がありますか？

Question

propositionalとpromotedの間に等しい接続が実装されていますか？

のは、私はいくつかのSymbolのためのスコープに

prf :: x :~: y 

があるとしましょう。

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

しかし、どのような他の方向について：それはReflであることにパターンマッチングによって、私はこのような

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

にそれを変換することができますか？私は

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

はい、2つの表現の間で行くこと（:==の実装が正しいと仮定した場合）可能であるが、それは計算を必要とします。

必要な情報はブール値自体には存在しません（it's been erased to a single bit）。それを回復する必要があります。これには、元のブール値の等価性テスト（実行時にそれらを保持しなければならないことを意味する）と、結果に関する知識を使用して、不可能なケースを排除するという2人の参加者に質問する必要があります。すでに答えを知っている計算を再実行するのは面倒です！

（彼らは単純だから）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でこの作業を行うことができると思うが、なぜわざわざ？ブーリアンを使わないでください！