[GHC] #13181: Introduce GHC.TypeNats module with natVal

GHC ghc-devs at haskell.org
Tue Jan 24 15:41:08 UTC 2017


#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


More information about the ghc-tickets mailing list