Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,247
    • Issues 5,247
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 577
    • Merge requests 577
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #15547
Closed
Open
Issue created Aug 21, 2018 by ChaiTRex@trac-ChaiTRex

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking