平等樣

我在ghci中所做的：平等樣

> :set -XTypeOperators 

> import Data.Proxy 
> import Data.Type.Equality 
> import Data.Singletons.Prelude 

> :let p1 = Proxy :: Proxy (Int == Int) 
> :let p2 = Proxy :: Proxy (Int :== Int) 

> :t p1 
p1 :: Proxy 'True 
> :t p2 
p2 :: Proxy (Int :== Int)

爲什麼在第二種情況下類型不是計算出來的？我能以某種方式解決它嗎？我可以創建類PEq（其中:==已定義）的實例嗎？

（GHC 7.10.3）

更新：我發現如何使一個實例。是否有一些原因不包括在內？

> instance PEq ('KProxy :: KProxy *) where { type (:==) x y = x == y }

或簡單的（如在評論中指出的dfeuer）

> instance PEq ('KProxy :: KProxy *)

或導入從TypeRepStar這種情況下：

> import Data.Singletons.TypeRepStar()

來源

2016-02-19 Dmitry Olshansky

你甚至不會需要的類型定義;它默認的是你寫的。 – dfeuer

我的猜測是：他們忘了添加實例。 – dfeuer

它的目的和[這裏]（https://github.com/goldfirere/singletons/issues/106）的解釋。從擴展的討論中可以明顯看出，poly-kinded的'=='是不好的，但是我仍然不清楚爲什麼默認不包含'*'實例。 –

看來，一個理由不包括實例PEq爲singletons中的種類*類似於不包括Eq的多聚集實例base。它被描述爲here。這種情況太常見了，如果存在，我們就無法描述類型函數結果的類型參數的平等。例如：

Succ n == Succ m = n == m

對於在singletons情況下，解決辦法可以定義它：

instance PEq ('KProxy :: KProxy *)

或者只是使用它：

import Data.Singletons.TypeRepStar()

來源

2016-03-04 12:01:56

回答

相關問題