Type-level sized Word literals???

Tue Oct 31 20:40:06 UTC 2023

We do have monomorphic unboxed literals via ExtendedLiterals. Can we make
use of those or perhaps a “boxed” variant of those to get monomorphic
literals at the value and type levels? E.g.,

0xFF#Word8 is monomorphically a Word8#.

So could we have:

0xFF at Word8 (or similar notation) is a boxed Word8? And that would
automatically be promoted to the type level.

Really, shouldn’t both the boxed and unboxed variants be promotable to the
type level?

— Lyle

On Oct 30, 2023 at 2:04:48 AM, Simon Peyton Jones <
simon.peytonjones at gmail.com> wrote:

> I'm pretty cautious about attempting to replicate type classes (or a
> weaker version thereof) at the kind level.  An alternative would be to us
> *non-overloaded* literals.
>
> Simon
>
> On Mon, 30 Oct 2023 at 08:20, Vladislav Zavialov via ghc-devs <
> ghc-devs at haskell.org> wrote:
>
>> > 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
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20231031/a646678c/attachment.html>