作為一個(有些人為的)示例,假設我想使用泛型來確定型別何時無人居住(通過非底部值)。我可以很好地到達那里:
class Absurd a where
absurd :: a -> b
default absurd :: (Generic a, GAbsurd (Rep a)) => a -> b
absurd = gabsurd . from
class GAbsurd f where
gabsurd :: f p -> b
instance GAbsurd f => GAbsurd (M1 i c f) where
gabsurd (M1 x) = gabsurd x
instance Absurd c => GAbsurd (K1 i c) where
gabsurd (K1 x) = absurd x
instance GAbsurd V1 where
gabsurd = \case
instance (GAbsurd a, GAbsurd b) => GAbsurd (a : : b) where
gabsurd (L1 x) = gabsurd x
gabsurd (R1 x) = gabsurd x
當我需要為:*:. 只需要一個GAbsurd aorGAbsurd b來實作GAbsurd (a :*: b),但是我能做的最好的就是同時要求兩者,這太強大了。例如:
data Void
data X = X Char Void
顯然X是一個“荒謬”的型別,但不能推斷,因為雖然Void是荒謬的,但Char不是,所以約束(Absurd Char, Absurd Void)無法解決。
我想做的是使用某種“約束析取”,如下所示:
instance (GAbsurd a || GAbsurd b) => GAbsurd (a :*: b) where
gabsurd (x :*: y) = case eitherConstraint of
LeftC -> gabsurd x
RightC -> gabsurd y
However, under the open world assumption, that's not possible. In fact, the code in Data.Boring (which also holds Absurd) simply ignores the problem entirely:
There are two reasonable instances for
GAbsurd (f :*: g), so we define neither
So this leads me to the question: why is the open world assumption so important? My best guess is that it has something to do with orphan instances, but even then shouldn't GHC have a list of all imported modules?
uj5u.com熱心網友回復:
我不確定關鍵問題是孤兒實體和模塊。
我認為主要問題是在面對約束分離時很難保持實體定義的連貫性和編譯效率。問題是您想象的語法中的假設eitherConstraint不能在編譯時簡單地在本地解決。例如,考慮以下功能:
foo :: (GAbsurd a) => GAbsurd (a :*: b)
foo = gabsurd
bar :: (GAbsurd b) => GAbsurd (a :*: b)
bar = gabsurd
這些都是型別正確的。在每種情況下,GAbsurd (a :*: b)都需要一個實體,并且可以通過GAbsurd a或的析取來提供一個實體GAbsurd b。gabsurd (a :*: b) = gabsurd a但是,對于第一個和第二個功能,實際實作這些功能的明顯的編譯時本地解決方案gabsurd (a :*: b) = gabsurd b會導致不連貫性。對于這個特定示例來說這不是問題,但是如果這些是Ord實體,并且我們使用一個多型函式將物件插入到 aSet中,并使用另一個多型函式在其中查找物件,Set那么如果它們最終出現,我們可能會遇到真正的問題對同一型別使用兩個不同Ord的實體。
為了保持連貫性,我們基本上必須攜帶大量額外的型別資訊來解決選擇實體時的析取問題。而且,我們可能不得不在傳遞這些資訊和在運行時評估它之間做出選擇,或者為即使是非常微不足道的程式生成指數數量的專用實體。
轉載請註明出處,本文鏈接:https://www.uj5u.com/shujuku/456091.html
標籤:haskell generics constraints ghc
上一篇:洗掉合并排序的鏈表中的重復項
