爲GADTs

Question

自動獲得節目實例假設我有一個複雜GADT與許多隱藏類型參數的構造函數：

data T where 
    A :: Num n => n -> T 
    B :: (Num n, Integral m) => n -> m -> T 
    C :: Floating a => [a] -> T 
    -- and so on 
    Z :: Num n => n -> n -> T 

我想使這個數據類型showable，而無需手動編寫的實例。問題是，由於Show不再是Num的超類，因此編譯器只需添加一個簡單的deriving instance Show T即可推斷它必須將Show約束添加到所有內部隱藏類型參數中。

對於每個隱藏類型參數時，它輸出像

Could not deduce (Show n) arising from a use of 'showsPrec' 
from the context Num n 
    bound by a pattern with constructor 
      A :: forall n. Num n => n -> T 
... 
Possible fix: 
    add (Show n) to the context of the data constructor 'A' 

添加Show約束到數據類型是不是一種選擇，因爲相關它限制了T可能居民。好像deriving instanec Show T應該在隱藏的數據類型上引入約束Show，雖然我不確定。

我該怎麼辦？

Answer 1

我有一個有趣的想法，不知道它有多實用。但是，如果您希望T在參數可顯示時可顯示，但也可用於不可顯示參數，則可使用ConstraintKinds通過約束參數化T。

{-# LANGUAGE GADTs, ConstraintKinds #-} 

import Data.Kind 

data T :: (* -> Constraint) -> * where 
    A :: (Num n, c n) => n -> T c 
    B :: (Num n, c n, Integral m, c m) => n -> m -> T c 
    ... 

然後T Show將showable ... 也許

deriving instance Show (T Show) 

（與StandaloneDeriving擴展名）會工作，但最起碼​​，T在原則上是showable，你可以寫實例手動。

雖然我的實際建議是要體現存在。存在型與收集其觀察值相當。舉例來說，如果你有一個像

class Foo a where 
    getBool :: a -> Bool 
    getInt :: a -> Int 

則存在

data AFoo where 
    AFoo :: Foo a => a 

一類是完全等同於(Bool,Int)，因爲你唯一可以用Foo其類型，你不知道的是做請撥打getBool或撥打getInt。你在你的數據類型使用Num，並且Num有沒有觀察，因爲如果你有一個未知的a與Num a，您可以通過調用的方法Num唯一要做的就是讓更多的a s出，並且從來都沒有混凝土。所以，你的A構造

A :: (Num n) => n -> T 

給你什麼，你可能也只是說

A :: T 

Integral，在另一方面，有toInteger爲觀察。所以，你很可能取代

B :: (Num n, Integral m) => n -> m -> T 

與

B :: Integer -> T 

（我們失去了n參數，並與Integer更換m）。我不認爲這在技術上是等同的，因爲我們可能已經實施了與Integral不同的操作，但是我們現在已經掌握了相當的技術，並且我懷疑您是否需要它（我會對如何做）。