Gibt es eine Verbindung zwischen `a: ~: b` und` (a: == b): ~: True`?

Question

Gibt es eine Verbindung zwischen propositional und promoted Gleichheit?

Lassen Sie uns sagen, ich habe

prf :: x :~: y 

in Rahmen für einige Symbol s; von Pattern-Matching auf sie Refl ist, kann ich das in

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

wie diese Transformation:

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

Aber was ist die andere Richtung? Wenn ich versuche,

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

dann alles, was ich bekommen ist

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

Answer 1

Ja, zwischen den beiden Darstellungen gehen kann (vorausgesetzt, die Umsetzung der :== korrekt ist), aber es erfordert Berechnung.

Die benötigten Informationen sind nicht im Boolean selbst enthalten (it's been erased to a single bit); Sie müssen es wiederherstellen. Dies beinhaltet die Befragung der beiden Teilnehmer des ursprünglichen Booleschen Gleichheitstests (was bedeutet, dass Sie sie zur Laufzeit behalten müssen) und die Verwendung Ihrer Kenntnis des Ergebnisses, um die unmöglichen Fälle zu eliminieren. Es ist ziemlich mühsam, eine Berechnung erneut durchzuführen, für die Sie die Antwort bereits kennen!

Arbeiten in Agda und Naturals statt Strings (weil sie einfacher):

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) 

Grundsätzlich denke ich, diese Arbeit in Haskell mit Singletons machen könnte, aber warum die Mühe machen? Verwenden Sie keine Booleschen Werte!