Haskell:用 Typeable 证明 `exists t. a ~ D t`

Question

我有

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 等)，但我无法让它工作。谁有办法做到这一点？

Answer 1

可以利用 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"