如何爲類型族編寫gcast？

我正在嘗試編寫Data.Typeable.gcast的變體，它適用於種類爲* -> *的類型族。我正在尋找的是：如何爲類型族編寫gcast？

{-# LANGUAGE TypeFamilies #-} 
import Data.Typeable 

type family T 

gcastT :: (Typeable a,Typeable b) => T a -> Maybe (T b) 
gcastT = undefined -- but that's not working too well!

會通過類比gcast :: (Typeable a,Typeable b) => f a -> Maybe (f b)。

這可能嗎？

我可以改變的背景下(Typeable (T a),Typeable (T b)) =>但我更喜歡這個簽名審美的原因：gcast不需要Typeable1 f，畢竟。

一些背景的情況下，我解決什麼其實我是想實現錯誤的問題：我的目標是編寫一個函數matchAndExtract：

matchAndExtract :: (Eq a, Typeable a, Eq b, Typeable b) => a -> b -> T b -> Maybe (T a) 
matchAndExtract x k v = if (cast x == Just k) then gcastT v else Nothing

這對於正在支票x和k然後返回提供的T b（我們當時知道它與T a相同 - T可能不是內射的，但它是是的函數！）或Nothing，否則返回提供的T b。

我已經通過包裝違規T a在newtype，使用gcast，再次展開了一個變通辦法：

matchAndExtractF :: (Eq a, Typeable a, Eq b, Typeable b) => a -> b -> f b -> Maybe (f a) 
matchAndExtractF x k v = if (cast x == Just k) then gcast v else Nothing 

newtype WrapT a = WrapT { unWrapT :: T a } 

matchAndExtractViaWrap :: (Eq a, Typeable a, Eq b, Typeable b) => a -> b -> T b -> Maybe (T a) 
matchAndExtractViaWrap x k v = fmap unWrapT $ matchAndExtractF a k (WrapT v)

但只是蹭到我走錯了路！這也適用於T a不是Typeable的實例;這再次表明Typeable (T a)上下文不應該被需要。

解決方法是完全可以接受的，但我想擺脫虛假WrapT類型。

來源

2013-02-28 yatima2975

不可能。類型族不是內射的，因此你不能解決它們以這種方式來的約束。 – 2013-02-28 21:44:04

但知道'可鍵入'並不意味着'可鍵入（T a）'！ – 2013-03-01 00:12:30

@DanielWagner：沒錯，但是我有限的測試包括一個'T a'顯然不是'Typeable'成員的情況。現在我不明白爲什麼'matchAndExtractViaWrap'工作！這可能是GHC中的錯誤（我正在使用7.6.1）？我會嘗試明天實施'unsafeCoerce' ... – yatima2975 2013-03-01 00:40:53

你試圖做的是不可能的，你已經實現它。相反，你可以使用

type family T x :: * 
newtype NT x = NT {fromNT :: T x} 
gcastT :: (Typeable a, Typeable b) => NT a -> Maybe (NT b) 
gcastT = gcast

在這種情況下，你不需要使用Eq約束。

另一種選擇是將分型詞典具體化到GADTs

data Type x where 
    Typeable :: Typeable x => Type x 

asT :: NT x -> Type x -> NT x 
asT = const 

gcastTD :: Type a -> Type b -> Type a -> Maybe (T b) 
gcastTD [email protected] Typeable x = fmap fromNT $ gcastT $ (NT x) `asT` t

（代碼沒有測試，但應該差不多正確）

一旦你有了這個你可以通過明確的類型簽名

使用

type instance T Int =() 

justUnit = gcastTD (Typeable :: Type Int) (Typeable :: Type Int)()

來源

2013-02-28 21:45:30

謝謝，這是我一起去的解決方案。 – yatima2975 2013-03-03 15:21:40

如何爲類型族編寫gcast？

回答

相關問題