A function `nat2Word# :: KnownNat n => Proxy# n -> Word#`
It would be nice if there were the function (perhaps in GHC.Prim) nat2Word# :: KnownNat n => Proxy# n -> Word# that was essentially (\ W# w# -> w#) . fromInteger . natVal, except that it produces the Word# at compile-time rather than runtime and that it works with Proxy# (for its no-runtime-representation, totally-free nature) instead of Proxy.
This would enable compile-time computations on Nats to produce a literal Word# without any runtime expense at all, which seems nice if you're dealing with primitives because you want to avoid runtime expense.
Motivating example
I'm learning primitive types and type-level arithmetic by making a simple set of fixed-width integer types where the type contains a Nat for the number of bits in the fixed-width integer.
Going from the following Nats to their corresponding Word#s at compile time even when optimizations are turned off during development would be very nice:
| `Div (n + 63) 64` \\\\= | the highest index we should try to access via `indexWordArray#` |
|---|---|
| `Mod (n - 1) 64 + 1` \\\\= | except when `n == 0`, the number of bits actually used in the \\\\ most-significant word |
| `2^(Mod (n + 63) 64 + 1) - 1` \\\\= | the unsigned integer narrowing bitmask to use on the \\\\ most-significant word |
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.4.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |