在模式同义词中调用函数

Question

我正在拉链上实现一些功能,其中孔类型是存在量化的,即我有这样的东西:

data Zipper (c :: Type -> Constraint) ... =
  forall hole. (c hole, ...) =>
    Zipper hole ...

dot表示我认为与我的问题无关的实现细节.现在考虑一些数据类型:

data Tree = Fork Tree Tree | Leaf Int

我想拥有的是检查我在树上的位置的能力.在简单递归的情况下,实现此目的的标准方法是模式匹配:

case hole of
  Fork _ _ -> doSomething
  Leaf _   -> doSomethingElse

然而,孔的类型是存在量化的,因此简单的模式匹配是不可行的.我的想法是使用类型类

class WhereAmI p a where
    position :: a -> p a

data Position :: Type -> Type where
    C_Leaf :: Position Tree
    C_Fork :: Position Tree
    -- possibly more constructors if we're traversing
    -- multiple data structures

然后我可以做类似的事情

f :: Zipper (WhereAmI Position) Tree -> Int
f (Zipper hole _) = case position hole of
  C_Leaf -> let (Leaf x) = hole in x
  otherwise -> ...

然而,我想要的是使用像这样的魔法替换C_Leaf类似的东西at @"Leaf"(即使用原始构造函数名称)

class WhereAmI' p (a :: Symbol) where
  position' :: Proxy a -> p

instance WhereAmI' (Position Tree) "Leaf" where
  position' _ = C_Leaf

instance WhereAmI' (Position Tree) "Fork" where
  position' _ = C_Fork

at :: forall a p. WhereAmI' p a => p
at = position (Proxy :: Proxy a)

这甚至可以工作,除了我不能at用作模式,如果我试图使它成为模式,GHC抱怨模式中的解析错误...

是否有一些聪明的方法来实现我在这里要描述的内容？

Answer 1

据我所知，这实际上是不可能的。没有办法从函数返回用于匹配的模式，并且由于 GADT 的改进方式（我认为），似乎不可能做任何比直接模式匹配。例如，我失败的尝试之一：

\n\n

instance Eq (Position a) where\n  C_Leaf == C_Leaf = True\n  C_Fork == C_Fork = True\n  _ == _ = False\n\npattern At x = ((\\y -> at x == y) -> True)\n

\n\n

这应该允许您编写case position hole of At @"Leaf" -> ...，但它不会进行类型检查，大概是因为类型细化过程。澄清：

\n\n

C_Leaf -> ...                -- This works\n((== C_Leaf) -> True) -> ... -- This doesn\'t work\ny | y == C_Leaf -> ...       -- This doesn\'t work\n

\n\n

我得到的后两个错误是Couldn\'t match expected type \xe2\x80\x98Tree\xe2\x80\x99 with actual type \xe2\x80\x98hole\xe2\x80\x99. 我实际上不确定为什么会发生这种情况，但我目前的理论是，表达式对于类型细化来说太复杂，无法正确“采用”：就编译器而言，没有理由期望当类型错误时==总是返回（即使我们知道这种情况永远不会发生）。所以这是不允许的。Falsehole

\n\n\n\n

我想知道，为什么您认为 usingat @"Leaf"比 using 更好C_Leaf？这并不是说您在一个版本中比在另一个版本中真正“使用原始构造函数名称”：它们都使用原始名称，并添加了一些额外的字符。我想在前一种情况下，您可以允许传入任意构造函数符号进行匹配，但这种事情通常似乎是不允许的，所以无论如何您都不能这样做。据我所知，使用符号方法实际上并没有获得任何好处。

\n\n

老实说，如果您的hole类型将被限制为Position无论如何都支持的构造函数，那么我真的不明白从一开始就使其存在的意义。创建拉链可能包含的所有类型的总和类型并将其作为类型参数传递会更简单。但我不太了解你的用例，所以我可能是错的。

\n\n\n\n

如果你真的愿意，我想你可以使用 Template Haskell 来完成你想要的事情。这将允许类似的事情：

\n\n

$(at "Leaf") -> ...\n

\n\n

假设您编写了适当的 TH 函数，它只会C_Leaf -> ...在编译时转换为，这样编译就不会出现问题。

\n