gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-03 21:41:44 26 4
gpt4 key购买 nike

我有

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.EqualityType.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/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com