2

我正在尝试编写一个Data.Typeable.gcast适用于 kind 类型系列的变体* -> *。我正在寻找的是：

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

它检查xandk是否属于同一类型并且相等，然后返回提供的T b（我们那时知道它与T a- T 可能不是单射的，但它是一个函数！）或Nothing，否则。

我有一个解决方法，将违规内容包装T a在 a newtype、 using 中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类型。

4

1 回答 1

3

您尝试做的事情不可能按照您实施的方式进行。相反，您可以使用

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) ()
于 2013-02-28T21:45:30.380 回答