如何为类型族编写gcast？

Question

{-# 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!

一些背景知识，以防我为实际想要实现的目标解决了错误的问题：我的目标是编写一个函数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是否具有相同的类型并相等，然后返回提供的tb（我们当时知道它与ta相同--T可能不是内射的，但它是一个函数！）或nothing，否则。

我已经找到了一个解决办法，将违规的ta包装在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)

这种解决方法是完全可以接受的，但我希望去掉虚假的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约束。

另一个选择是将可键入的词典具体化为GADT

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) ()