haskell - 从包装器中动态匹配嵌套的 GADT

Question

我最近问如何制作 GADT 实例的同构列表:Function returning result of any constructor of a GADT

tl;博士

{-#LANGUAGE GADTs, EmptyDataDecls #-}
module Main where

-- Define a contrived GADT
data TFoo
data TBar
data Thing a where
  Foo :: Int -> Thing TFoo
  Bar :: String -> Thing TBar

data SomeThing = forall a. SomeThing (Thing a)

combine :: [SomeThing]
combine = [Something $ Foo 1, SomeThing $ Bar "abc"]

现在，我在动态“解包”它们时遇到了一些麻烦。假设我们有这个(仍然是人为的，但更接近我的真实用例)代码:

{-#LANGUAGE GADTs, EmptyDataDecls #-}
module Main where

-- Define a contrived GADT
data Thing a where
  Thing :: TKind a -> Thing a

data TFoo
data TBar
data TKind a where
  Foo :: TKind TFoo
  Bar :: TKind TBar

data SomeThing = forall a. SomeThing (Thing a)

example :: SomeThing
example = SomeThing $ Thing Foo

extractThingWithTKind :: TKind a -> SomeThing -> Either String (Thing a)
extractThingWithTKind k st = case st of
                               SomeThing t@(Thing k) -> Right t
                               _                     -> Left "nope"

以上不起作用，因为 t在 Right t没有类型 Thing a .从本质上讲，我理解为什么这不起作用。 k上的模式匹配不做我想要的(仅当 k 与传入的相同时才匹配)。但这是我在逼近我想要的方面的最佳尝试。我试过 instance ing Eq在 TKind a , 但因为 (==) :: a -> a -> Bool ，这将不起作用(相等性取决于运行时可能不同的类型)。我可以包装 TKind像我一样 Thing ，但那样我只会把问题推低。

去除动态，我尝试了模式匹配 Thing TFoo明确地:

extractThingWithFoo :: SomeThing -> Either String (Thing TFoo)
extractThingWithFoo st = case st of
                            SomeThing t@(Thing Foo) -> Right t
                            _                       -> Left "nope" 

这有效!但这是否意味着我不能进行动态匹配？必须为每种类型重复上述方法将是一种真正的痛苦TKind (在非人为的版本中，有很多)。我看到的唯一其他解决方案是更改 SomeThing是一个 sum 类型，每个 TKind 有一个包装器，但随后您只是将重复的代码移动到不同的位置(并强制所有 SomeThing 的使用对每个进行模式匹配)。

Answer 1

为了实现带有签名的函数extractThingWithTKind :: TKind a -> SomeThing -> Either String (Thing a) ，我们需要能够确定里面是什么 SomeThing是 TKind a或不。 GADT 构造函数是这种类型相等性的见证，但它们需要显式模式匹配以在函数的局部范围内“解开”这些假设。

extractThingWithTKind :: TKind a -> SomeThing -> Either String (Thing a)
extractThingWithTKind Foo (SomeThing t@(Thing Foo)) = Right t
extractThingWithTKind Bar (SomeThing t@(Thing Bar)) = Right t
extractThingWithTKind _ _ = Left "nope"

第一个参数的模式匹配产生了 a ~ TFoo 的假设(在第一种情况下)，对第二个参数的进一步模式匹配证明 SomeThing 里面的东西也是TFoo .至关重要的是，个案必须一一说明，因为提供证据的是 build 者本身。