#15547: A function `nat2Word# :: KnownNat n => Proxy# n -> Word#` -------------------------------------+------------------------------------- Reporter: ChaiTRex | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 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: -------------------------------------+------------------------------------- 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 [https://hackage.haskell.org/package/base-4.11.1.0/docs/GHC- Exts.html#t:Proxy-35- its no-runtime-representation, totally-free nature]) instead of `Proxy`. This would enable compile-time computations on `Nat`s 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 `Nat`s 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 || -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15547 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler