[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
#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