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

GHC ghc-devs at haskell.org
Fri Feb 3 11:31:02 UTC 2017


#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


More information about the ghc-tickets mailing list