6

使用PatternSynonyms（显式双向形式），pattern-to-expr 方程实际上形成了一个函数，但拼写为大写（假设您最终得到一个正确类型的完全饱和的数据结构）。然后考虑（在 GHC 8.10.2）

{-# LANGUAGE  PatternSynonyms, ViewPatterns  #-}

data Nat = Zero | Succ Nat                deriving (Eq, Show, Read)

--  Pattern Synonyms as functions?

pattern Pred :: Nat -> Nat
pattern Pred n <- {- what goes here? -}           where
  Pred (Succ n) = n
pattern One           = Succ Zero

zero = Pred One                      -- shows as Zero OK

那么我应该为pattern Pred n <- ???价值模式顶线添加什么？或者我可以不使用Pred n模式匹配吗？似乎有效（但我不明白为什么）是一种视图模式

pattern Pred n <-  (Succ -> n)          where ...   -- seems to work, but why?

isZero (Pred One) = True
isZero _          = False

-- isZero (Pred One) ===> True ; isZero Zero ===> True
-- isZero (Succ One) ===> False; isZero One  ===> False

Pred在这里用作伪构造函数/模式看起来很不错，因为它是一个单射函数。

4

1 回答 1

7

考虑您的模式同义词的这种用法：

succ' :: Nat -> Nat
succ' (Pred n) = n

当然，其意图是返回参数的后继。

在这种情况下，很明显，当参数是 时，k变量n必须绑定到Succ k。鉴于这种直觉，我们需要找到一种完全可以做到这一点的模式，一种可以在这里使用的模式，而不是Pred n：

succ' :: Nat -> Nat
succ' ({- bind n to Succ k -}) = n

事实证明，您的视图模式正是这样做的。这会很好用：

succ' :: Nat -> Nat
succ' (Succ -> n) = n

因此，我们必须定义

pattern Pred n <- (Succ -> n)

在我自己（有限的）经验中，这是相当地道的。当您拥有双向模式同义词时，您通常会使用上述视图模式。

于 2021-01-20T12:31:03.027 回答