Y a-t-il un lien entre `a: ~: b` et` (a: == b): ~: True`?

Question

Y at-il une connexion implémentée entre propositional et promoted égalité?

Disons que je

prf :: x :~: y 

portée pour certains Symbol s; par modèle correspondant à ce sujet étant Refl, je peux transformer cela en

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

comme ceci:

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

Mais qu'en l'autre sens? Si je tente

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

alors tout ce que je reçois est

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

Answer 1

Oui, aller entre les deux représentations est possible (en supposant la mise en œuvre de :== est correct), mais il nécessite le calcul.

Les informations dont vous avez besoin ne sont pas présentes dans le booléen lui-même (it's been erased to a single bit); vous devez le récupérer. Cela implique d'interroger les deux participants du test d'égalité booléen original (ce qui signifie que vous devez les garder à l'exécution), et d'utiliser votre connaissance du résultat pour éliminer les cas impossibles. Il est plutôt fastidieux de refaire un calcul pour lequel vous connaissez déjà la réponse!

Travailler en Agda, et à l'aide Naturals au lieu de cordes (parce qu'ils sont plus simples):

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) 

En principe, je pense que vous pourriez faire ce travail en Haskell utilisant singletons, mais pourquoi pris la peine? N'utilisez pas de booléens!