如何为类型族编写gcast？

Question

我正在尝试编写Data.Typeable.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类型。

Answer 1

你试图做的是不可能的，你已经实现它。相反，你可以使用

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 t@Typeable Typeable x = fmap fromNT $ gcastT $ (NT x) `asT` t 

（代码没有测试，但应该差不多正确）

一旦你有了这个你可以通过明确的类型签名

使用

type instance T Int =() 

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