我有
data D t = ...
data SomeStuff = forall a (Typeable a, ...) => SomeStuff a
在某些时候,我得到了一个 SomeStuff,我想尝试将其内部 a
转换为 D t
(其中 t
可以any 类型,我只对 D
部分感兴趣)。一些东西(在伪 Haskell 中)看起来像:
case someStuff of
SomeStuff (_ :: a) -> case eqT :: Maybe (a :~: (exists t. D t)) of
Just Refl -> -- proven that `exists t. a ~ D t`
Nothing -> -- nothing to do here
我一直在摆弄 Data.Type.Equality
和 Type.Reflection
(如 App 等),但我无法让它工作。谁有办法做到这一点?
最佳答案
可以利用 Type.Reflection
来测试类型是否为 D _
形式,如下所示。
我们首先给出一些以您的示例为模型的具体定义,以便我们稍后可以测试我们的代码。
{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, TypeOperators, TypeApplications #-}
{-# OPTIONS -Wall #-}
import Type.Reflection
data D t = D1 | D2 -- whatever
data SomeStuff = forall a. (Typeable a, Show a) => SomeStuff a
然后,我们测试 D _
如下:
foo :: SomeStuff -> (forall t. D t -> String) -> String
foo (SomeStuff (x :: a)) f = case typeRep @a of
App d _ | Just HRefl <- eqTypeRep (typeRep @D) d -> f x
_ -> "the SomeStuff argument does not contain a value of type D t for any t"
在上面,我们将 SomeStuff
值和多态函数 f
作为参数。后者需要 D _
形式的参数,此处仅用于说明我们的方法确实有效——如果不需要,可以删除 f
参数那个。
之后,我们采用 takeRep @a
对我们未知类型 a
的(反射)类型表示进行建模。我们检查它是否与模式 App d _
匹配,即类型 a
是否是 d
对我们不关心的东西的应用 _
。如果是这样,我们检查 d
是否确实是我们的 D
类型构造函数的(反射(reflect)表示)。将 eqTypeRepl
的结果与 Just HRefl
进行匹配,使 GHC 假设 a ~ D t
为一些新的类型变量 t
,这就是我们想要的。之后,我们可以调用 f x
确认 GHC 推断出所需的类型。
作为替代方案,我们可以利用 View 模式使我们的代码更紧凑,而不会过多牺牲可读性:
foo :: SomeStuff -> (forall t. D t -> String) -> String
foo (SomeStuff (x :: a)) f = case typeRep @a of
App (eqTypeRep (typeRep @D) -> Just HRefl) _ -> f x
_ -> "the SomeStuff argument does not contain a value of type D t for any t"
关于Haskell:用 Typeable 证明 `exists t. a ~ D t`,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/67105950/