Type-level sized Word literals???

[Vladislav Zavialov]

> I am working on some code where it is useful to have types indexed by a 16-bit unsigned value.

This is great to hear. I've always wanted to make it possible to
promote all numeric types: Natural, Word8, Word16, Word32, Word64,
Integer, Int8, Int16, Int32, Int64. (Then, as the next step, even the
floating-point types Float and Double). I see it as a step towards
universal promotion, i.e. being able to use any data type as a kind.

The problem is that such a change would require a GHC proposal, and I
don't have a strong motivating use case to write one. But you seem to
have one! If you'd like to co-author a GHC proposal and if the
proposal gets accepted, I can implement the feature.

Here's how I imagine it could work.

1. Currently, a type-level literal like `15` is inferred to have kind
`Nat` (and `Nat` is a synonym for `Natural` nowadays). At the
term-level, however, the type of `15` is `forall {a}. Num a => a`. I'd
like to follow the term-level precedent as closely as possible, except
we don't have type class constraints in kinds, so it's going to be
simply `15 :: forall {k}. k`.

2. The desugaring should also follow the term-level precedent. `15`
actually stands for `fromInteger (15 :: Integer)`, and I expect no
less at the type level, where we could introduce a type family
`FromInteger :: Integer -> k`, with the following instances

   type instance FromInteger @Natural n = NaturalFromInteger n
   type instance FromInteger @Word8 n = Word8FromInteger n
   type instance FromInteger @Word16 n = Word16FromInteger n
   ...

   The helper type families `NaturalFromInteger`, `Word8FromInteger`,
`Word16FromInteger` etc. are partial, e.g. `NaturalFromInteger (10 ::
Integer)` yields `10 :: Natural` whereas `NaturalFromInteger (-10)` is
stuck.

I have a fairly good idea of what it'd take to implement this (i.e.
the changes to the GHC parser, type checker, and libraries), and the
change has been on my mind for a while. The use case that you have
might be the last piece of the puzzle to get this thing rolling.

Can you tell more about the code you're writing? Would it be possible
to use it as the basis for the "Motivation" section of a GHC proposal?

Vlad

On Mon, Oct 30, 2023 at 6:06 AM Viktor Dukhovni <ietf-dane at dukhovni.org> wrote:
>
> I am working on some code where it is useful to have types indexed by a
> 16-bit unsigned value.
>
> Presently, I am using type-level naturals and having to now and then
> provide witnesses that a 'Nat' value I am working with is at most 65535.
>
> Also, perhaps there's some inefficiency here, as Naturals have two
> constructors, and so a more complex representation with (AFAIK) no
> unboxed forms.
>
> I was wondering what it would take to have type-level fixed-size
> Words (Word8, Word16, Word32, Word64) to go along with the Nats?
>
> It looks like some of the machinery (KnownWord16, SomeWord16, wordVal16,
> etc.) can be copied straight out of GHC.TypeNats with minor changes, and
> that much works, but the three major things that are't easily done seem
> to be:
>
>     - There are it seems no TypeReps for types of Kind Word16, so one can't
>       have (Typeable (Foo w)) with (w :: Word16).
>
>     - There are no literals of a promoted Word16 Kind.
>
>         type Foo :: Word16 -> Type
>         data Foo w = MkFoo Int
>
>         -- 1 has Kind 'Natural' (a.k.a. Nat)
>         x = MkFoo 13 :: Foo 1 -- Rejected,
>
>         -- The new ExtendedLiterals syntax does not help
>         --
>         x = MkFoo 13 :: Foo (W16# 1#Word16) -- Syntax error!
>
>     - There are unsurprisingly also no built-in 'KnownWord16' instances
>       for any hypothetical type-level literals of Kind Word16.
>
> Likely the use case for type-level fixed-size words is too specialised
> to rush to shoehorn into GHC, but is there something on the not too
> distant horizon that would make it easier and reasonable to have
> fixed-size unsigned integral type literals available?
>
> [ I don't see a use-case for unsigned versions, they can trivially be
>   represented by the unsigned value of the same width. ]
>
> With some inconvenience, in many cases I can perhaps synthesise Proxies
> for types of Kind Word16, and just never use literals directly.
>
> --
>     Viktor.
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs