[GHC] #11992: RFC, add Suc to base
#11992: RFC, add Suc to base -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: | Version: 8.1 libraries/base | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs 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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11992 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11992: RFC, add Suc to base -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): Please can you add some motivation for this? Seems like something that could just be provided by a library. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11992#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11992: RFC, add Suc to base -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Basically the same [https://prime.haskell.org/wiki/RemoveNPlusK 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 {{{#!hs fac (S n) = (S n) * fac n }}} into {{{#!hs 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): {{{#!hs 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 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11992#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11992: RFC, add Suc to base -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nomeata): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11992#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11992: RFC, add Suc to base -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Fair enough :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11992#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11992: RFC, add Suc to base -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: libraries/base | Version: 8.1 Resolution: wontfix | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * status: new => closed * resolution: => wontfix Comment: Closing as wontfix, since the consensus seems to be to not add `Suc` to base. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11992#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC