Esiste una connessione tra `a: ~: b` e` (a: == b): ~: True`?

Question

Esiste una connessione implementata tra l'uguaglianza propositional e promoted?

Diciamo che ho

prf :: x :~: y 

portata per alcuni Symbol s; dal pattern matching su di esso essendo Refl, posso trasformarla in

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

come questo:

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

Ma per quanto riguarda l'altra direzione? Se provo

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

allora tutto quello che ottiene è

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

Answer 1

Sì, in corso tra le due rappresentazioni è possibile (assumendo la realizzazione di :== è corretto), ma richiede il calcolo.

Le informazioni necessarie non sono presenti nello stesso booleano (it's been erased to a single bit); devi recuperarlo. Ciò comporta l'interrogazione dei due partecipanti al test di uguaglianza booleana originale (il che significa che devi tenerli in giro durante il runtime) e usare la tua conoscenza del risultato per eliminare i casi impossibili. È piuttosto noioso riprovare un calcolo per il quale già conosci la risposta!

Lavorare in Agda, e l'utilizzo di prodotti naturali, invece di stringhe (perché sono più semplici):

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) 

In linea di massima penso che si potrebbe fare questo lavoro in Haskell utilizzando singletons, ma perché preoccuparsi? Non usare Booleans!