Opened 3 years ago

Closed 3 years ago

#13181 closed feature request (fixed)

Introduce GHC.TypeNats module with natVal

Reported by: phadej Owned by: phadej
Priority: normal Milestone: 8.2.1
Component: Compiler Version:
Keywords: Cc:
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:

Description

See 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.

Change History (4)

comment:1 Changed 3 years ago by phadej

Differential Rev(s): Phab:D3024
Status: newpatch

comment:2 Changed 3 years ago by Ben Gamari <ben@…>

In 1fcede43/ghc:

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

comment:3 Changed 3 years ago 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.

comment:4 Changed 3 years ago by mpickering

Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.