用於推斷約束雙方，如果其他類型的平等

我試圖填補孔下面的代碼片段用於推斷約束雙方，如果其他類型的平等

import Data.Proxy 
import GHC.TypeLits 
import Data.Type.Equality 
import Data.Type.Bool 
import Unsafe.Coerce 

ifThenElse :: forall (a :: Nat) (b :: Nat) x l r. 
    (KnownNat a, KnownNat b, x ~ If (a==b) l r) => 
    Proxy a -> Proxy b -> Either (x :~: l) (x :~: r) 
ifThenElse pa pb = case sameNat pa pb of 
    Just Refl -> Left Refl 
    Nothing -> Right $ unsafeCoerce Refl -- This was the hole

是否有可能和？

編輯：檢查了sameNat的來源，結果證明他們使用unsafeCoerce。我相應地編輯了上面的代碼。

來源

2017-02-15 fakedrake

您應該發佈您的編輯作爲答案（並回滾編輯）。 – Alec

一般問題似乎是，儘管GADT模式匹配提供了等式約束，但它從不提供不等式約束，所以我們不能說服GHC不使用封閉類型族的第一個子句。我們可能需要GHC的更多支持來做到這一點，AFAICS。 – chi

呃，你可以通過查看這種不容易證明的類型來判斷，即使有一個歸納的「Nat」（而不是'GHC.TypeLits'中的破壞的類型）。你是如何設法將自己融入這個特殊的角落的？我們可能會告訴你如何重新設計你的程序，這樣你就不需要這樣粗糙的證明。 –

一種可能的解決方案是使用singletons庫來獲取代表類型級別的term-level函數（反之亦然）。

它的要點是：

import Data.Singletons.Prelude

（...）

case (sing :: Sing a) %:== (sing :: Sing b) of 
    STrue -> Left Refl 
    SFalse -> Right Refl

我已經提出了一個self-contained file所有的進口和語言擴展了。

來源

2017-02-15 12:34:52 gallais

非常感謝！ '％：=='沒有記錄嗎？我找不到它。 – fakedrake

'Data.Singletons.Prelude'重新導出'Data.Singletons.Prelude.Eq'，您可以在其中找到['（％：==）']（https://hackage.haskell.org/package/singletons-2.2 /docs/Data-Singletons-Prelude-Eq.html#v:-37-:-61--61-） – gallais

用於推斷約束雙方，如果其他類型的平等

回答

相關問題