[GHC] #15547: A function `nat2Word# :: KnownNat n => Proxy# n -> Word#`
GHC
ghc-devs at haskell.org
Tue Aug 21 01:30:29 UTC 2018
#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
More information about the ghc-tickets
mailing list