`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

예, 두 가지 표현 사이에가는 (:==의 구현이 올바른지 가정) 수이지만, 계산을 필요로한다.

필요한 정보가 부울 자체에 없습니다 (it's been erased to a single bit). 당신은 그것을 복구해야합니다. 여기에는 두 명의 참가자가 원래의 불리언 동등성 테스트 (즉, 런타임에 유지해야 함)를 묻는 작업과 결과에 대한 지식을 사용하여 불가능한 경우를 제거하는 작업이 포함됩니다. 이미 답을 알고있는 계산을 다시 수행하는 것은 지겨운 일입니다!

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) 

? 부울을 사용하지 마십시오!