haskell - 如何为类型家族编写 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 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约束。

另一种选择是将可键入的字典具体化为 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) ()