问题描述
使用 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)
以我自己(有限的)经验,这是相当地道的。当你有一个双向模式同义词时,你通常会像上面那样使用视图模式。