动态模式匹配嵌套的GADT从包装器中返回

Posted 2021-04-08

我最近问过如何制作一个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上尝试过Eqing 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模式匹配每个）。

答案

为了实现具有签名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。至关重要的是，个别案件必须逐一拼写，因为它是提供证据的构造者本身。