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

Question

与 PatternSynonyms ( explicitly bidirectional form )，pattern-to-expr 方程实际上形成了一个函数，但拼写为大写(假设您最终得到正确类型的完全饱和的数据 constr)。然后考虑(在 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 <- ??? 放什么？值(value)模式顶线？或者我可以不使用 Pred n在模式匹配中？似乎有效(但我不明白为什么)是一种 View 模式

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作为这里的伪构造函数/模式，因为它是一个单射函数。

Answer 1

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

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

当然，其意图是返回参数的后继。
在这种情况下，很明显，当参数是 k , 然后变量 n必须绑定(bind)到 Succ k .鉴于这种直觉，我们需要找到一个完全可以做到这一点的模式，一个可以在这里使用而不是 Pred n 的模式。 :

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

事实证明，您的 View 模式正是这样做的。这会很好用:

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

因此，我们必须定义

pattern Pred n <- (Succ -> n)

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