Opened 13 months ago

#15547 new feature request

A function `nat2Word# :: KnownNat n => Proxy# n -> Word#`

Reported by: ChaiTRex Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (0)

Note: See TracTickets for help on using tickets.