Haskell：用 Typeable 证明 ` 存在 t。一个〜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（如应用程序等），但我无法让它工作。有人有办法吗？

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 类型构造函数的（反映的表示）。将eqTypeRepl 与Just HRefl 的结果相匹配，使得GHC 假设a ~ D t 用于一些新的类型变量t，这正是我们想要的。之后，我们可以致电f x 确认 GHC 推断出想要的类型。

作为替代方案，我们可以利用视图模式来使我们的代码更紧凑，而不会过多牺牲可读性：

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"