8

Is there any connection implemented between propositional and promoted equality?

Let's say I have

prf :: x :~: y

in scope for some Symbols; by pattern matching on it being Refl, I can transform that into

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

like this:

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

But what about the other direction? If I try

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

then all I get is

• Could not deduce: x ~ y
  from the context: 'True ~ (x :== y)
Benjamin Hodgson
  • 42,952
  • 15
  • 108
  • 157
Cactus
  • 27,075
  • 9
  • 69
  • 149
  • 1
    Sure, `toProp _ = unsafeCoerce Refl`. `sameSymbol` is defined this way, so I doubt you can do better. – effectfully Jun 21 '16 at 09:27
  • 1
    You could also write `toProp Refl = fromJust $ sameSymbol (Proxy :: Proxy x) (Proxy :: Proxy y)` but this is only slightly better than using `unsafeCoerce`. – user2407038 Jun 21 '16 at 15:43

1 Answers1

8

Yes, going between the two representations is possible (assuming the implementation of :== is correct), but it requires computation.

The information you need is not present in the Boolean itself (it's been erased to a single bit); you have to recover it. This involves interrogating the two participants of the original Boolean equality test (which means you have to keep them around at runtime), and using your knowledge of the result to eliminate the impossible cases. It's rather tedious to re-perform a computation for which you already know the answer!

Working in Agda, and using naturals instead of strings (because they're simpler):

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 principle I think you could make this work in Haskell using singletons, but why bother? Don't use Booleans!

Benjamin Hodgson
  • 42,952
  • 15
  • 108
  • 157
  • 1
    This is the right answer, but I fear that this is not doable in Haskell at the moment. In Haskell `n,m` can not be eliminated since they have an opaque-ish type `Symbol`. We could rely on the `KnownSymbol n` instance, however that only allows one to recover the name of the symbol as a string at the value level, which does not help. – chi Jun 20 '16 at 16:01
  • 1
    @chi Yeah, that's what I was trying to get at when I said "you need to have the values at runtime". The type specified in the question is not satisfiable in Haskell, you'd need parameters of type `Sing x` and `Sing y` in there. – Benjamin Hodgson Jun 20 '16 at 16:07
  • @BenjaminHodgson: but even if I had `Sing x` and `Sing y` parameters, I'm not sure (for `Symbol`s) that I can recurse on them. – Cactus Jun 21 '16 at 01:22