Richard Eisenberg, inspired by Rinat Striungis
haskell
This proposal is discussed at this pull request.
GHC currently uses GHC.TypeLits.Nat
to describe compile-time natural numbers but Numeric.Natural.Natural
to describe runtime ones. This proposal unifies the two by making GHC.TypeLits.Nat
a synonym for Numeric.Natural.Natural
.
GHC should not have two different types to represent natural numbers. One is enough. The existence of the separate kind Nat
and the impossibility of using Natural
at compile time (and data constructors with Natural
fields) is an unnecessary complication. It forces us to create redundant types with Nat
fields in their constructors (making these types uninhabited at runtime) only for use at compile time. This is more cumbersome than the promotion of ordinary data types.
Consider this data type with fields of type Natural
:
data Point = MkPoint Natural Natural
Point
is inhabited by terms, but not by types:
p = MkPoint 3 5 -- ok
type P = MkPoint 3 5 -- not ok
Alternatively, we could declare it with fields of type Nat
:
data Point = MkPoint Nat Nat
Then it would have the opposite issue:
p = MkPoint 3 5 -- not ok
type P = MkPoint 3 5 -- ok
To avoid declaring two incompatible data types, we could add a parameter to Point
:
data Point n = MkPoint n n
type PointT = Point Natural -- inhabited by terms
type PointK = Point Nat -- inhabited by types
However, this is a roundabout way to go about it, and in more involved scenarios requires additional machinery to support it (such as the Demote
type family in the singletons
package). By unifying Nat
and Natural
, we avoid this issue entirely.
- Add
type Nat = Natural
inGHC.TypeNats
. - Re-export
Natural
fromGHC.TypeNats
andGHC.TypeLits
(along with the current re-export ofNat
). - Assign numbers in types to have kind
Natural
instead of kindNat
.
- Instances written about
Nat
may now needTypeSynonymInstances
, which is implied byFlexibleInstances
. Or, they could be written to useNatural
instead ofNat
. - It is possible for someone to have separate instances today for
Nat
andNatural
, though it is unclear how an instance onNat
would be useful. Having two separate instances for these types will not be possible after this proposal is implemented.
Otherwise, this change should be backward compatible. In particular, this proposal does not change parsing or other aspects of numbers written in types. For example, even though (-5 :: Natural)
parses today (and throws a runtime error), that expression will not parse in types.
- We might be painting ourselves into a corner, having not yet worked out the way we will support other types of compile-time literals. But I (Richard) think this will be OK.
- Do nothing.
- None at this time.
- This is already implemented, by Rinat Striungis.