[GHC] #13181: Introduce GHC.TypeNats module with natVal
#13181: Introduce GHC.TypeNats module with natVal -------------------------------------+------------------------------------- Reporter: phadej | Owner: phadej Type: feature | Status: new request | Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 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: -------------------------------------+------------------------------------- See [https://mail.haskell.org/pipermail/libraries/2017-January/027615.html libraries thread] Currently we have in the GHC.TypeLits module {{{ natVal :: forall n proxy. KnowNat n => proxy n -> Integer }}} However, the result integer is never negative. Numeric.Natural module is in base since base-4.8.0.0. --- I propose that we introduce new module GHC.TypeNats with natVal and natVal' {{{ natVal :: forall n proxy. KnownNat n => proxy n -> Natural }}} and {{{ natVal' :: forall n. KnownNat n => Proxy# n -> Natural }}} and other KnownNat related terms and type families. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13181> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13181: Introduce GHC.TypeNats module with natVal -------------------------------------+------------------------------------- Reporter: phadej | Owner: phadej Type: feature request | Status: patch Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3024 Wiki Page: | -------------------------------------+------------------------------------- Changes (by phadej): * status: new => patch * differential: => Phab:D3024 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13181#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13181: Introduce GHC.TypeNats module with natVal -------------------------------------+------------------------------------- Reporter: phadej | Owner: phadej Type: feature request | Status: patch Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3024 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"1fcede43d2b30f33b7505e25eb6b1f321be0407f/ghc" 1fcede43/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="1fcede43d2b30f33b7505e25eb6b1f321be0407f" Introduce GHC.TypeNats module, change KnownNat evidence to be Natural Reviewers: dfeuer, austin, hvr, bgamari Reviewed By: bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D3024 GHC Trac Issues: #13181 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13181#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13181: Introduce GHC.TypeNats module with natVal -------------------------------------+------------------------------------- Reporter: phadej | Owner: phadej Type: feature request | Status: patch Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3024 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): This implementation is lacking motivation anywhere so I will add it in case anyone was wondering. One possible design choice would have been to keep the internal representation as an `Integer` and at the interface boundary do the error- checking when converting to a `Natural` once. Oleg preferred this implementation as it will cause the compiler to fail sooner if we accidentally do something like cause an interflow by subtracting or anything like that. The interface boundary is shifted to converting into `EvTerm`. There is a related ticket #13186 which talks about actually representing the evidence as `Natural` as well. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13181#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13181: Introduce GHC.TypeNats module with natVal -------------------------------------+------------------------------------- Reporter: phadej | Owner: phadej Type: feature request | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3024 Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * status: patch => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13181#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC