模式同义词作为函数的无趣/困惑

如何解决模式同义词作为函数的无趣/困惑

使用 PatternSynonyms (explicitly bidirectional form)，模式到表达式的方程实际上形成一个函数，但拼写为大写（前提是您最终得到正确类型的完全饱和的数据构造） .然后考虑（在 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 作为伪构造函数/模式看起来很不错，因为它是一个单射函数。

解决方法

考虑一下你的模式同义词的这种用法：

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)

以我自己（有限的）经验，这是相当地道的。当你有一个双向模式同义词时，你通常会像上面那样使用视图模式。