Haskell：用 Typeable 证明`存在 t。一个 ~ D t`

Question

我有

data D t = ...
data SomeStuff = forall a (Typeable a, ...) => SomeStuff a

在某些时候，我得到了一个 SomeStuff，a我想尝试将其内部转换为D t（任何类型t都可以，我只对这部分感兴趣）。一些（在伪 Haskell 中）看起来像：D

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

D _可以通过exploit来测试类型是否为form Type.Reflection，如下。

我们首先给出一些以您的示例为模型的具体定义，以便我们稍后可以测试我们的代码。

{-# 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类型构造函数（的反映表示）。匹配eqTypeReplagainst的结果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"