Type-level sized Word literals???

[Simon Peyton Jones]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20231030/b7b8719f/attachment.html>