RFC, add Suc to base

hasSuc :: Int -> Maybe Int
hasSuc n = [ n - 1 | n > 0 ]

pattern Suc :: Int -> Int
pattern Suc n <- (hasSuc -> Just n)
  where Suc n = n + 1

with a more general type

Trac metadata

Trac field	Value
Version	8.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	libraries/base
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tfeature request Trac import core libraries labels

mentioned in issue #11993

Please can you add some motivation for this? Seems like something that could just be provided by a library.

Basically the same rationale as for NPlusKPatterns without some of its problems (doesn't require an extension or non-standard syntax), natural numbers are one of the most prominent inductive definitions (data N = O | S N) and a lot of code mirrors that. Little mental prowess is needed to translate

fac (S n) = (S n) * fac n

into

fac n = n * fac (n - 1)

but I have found myself itching for it in larger examples. Not a great rationale? Agreed. BUT!, no-one said ever, does it even cover patterns like (5 + n)? Funny you ask, in GHC head we can define (but not actually use S as a pattern, I'm interested being wrong):

hasS :: forall n. KnownNat n => Integer -> Maybe Integer
hasS n = [ n - natVal @n Proxy | n >= natVal @n Proxy ]

pattern S :: forall n. KnownNat n => Integer -> Integer
pattern S n <- (hasS @n -> Just n)
  where S n = n + natVal @n Proxy

and if #11350 (closed) gets implemented hopefully it can be used as S @5 n.

Then all we need is some type defaulting such that S m and S @1 m are equivalent, where if a constraint KnownNat n is not satisfied it defaults to n ~ 1... or is that beyond the pale?

I’m not convinced that this is base material. Most pros in wiki:RemoveNPlusK relate to teaching, and I am not sure how many educators want to drag in pattern synonyms into their courses. And if they want, they can simply provide a custom Nat module for their students.

Fair enough :)

closed

Closing as wontfix, since the consensus seems to be to not add Suc to base.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedWon'tFix

added Pnormal label