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

Question

我最近问过如何制作一个GADT实例的同源列表:函数返回 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"

以上不起作用,因为tin Right t没有类型Thing a.从本质上讲,我理解为什么这不起作用.模式匹配就k没有做我想要的事情(只有与k传入的模式匹配才匹配).但这是我最接近我想要的东西.我试着instance荷兰国际集团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也是a TFoo.至关重要的是,个别案件必须逐一拼写,因为它是提供证据的构造者本身.