<html><body><div dir="ltr">We do have monomorphic unboxed literals via <code style="border:1px solid rgb(206,206,206);background-color:rgb(248,248,248);padding:0px 3px;border-radius:4px">ExtendedLiterals</code>. 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.,</div><div dir="ltr"><br></div><div dir="ltr"><code style="border:1px solid rgb(206,206,206);background-color:rgb(248,248,248);padding:0px 3px;border-radius:4px">0xFF#Word8</code> is monomorphically a <code style="border:1px solid rgb(206,206,206);background-color:rgb(248,248,248);padding:0px 3px;border-radius:4px">Word8#</code>.<br></div><div dir="ltr"><br></div><div dir="ltr">So could we have:</div><div dir="ltr"><br></div><div dir="ltr"><code style="border:1px solid rgb(206,206,206);background-color:rgb(248,248,248);padding:0px 3px;border-radius:4px">0xFF@Word8</code> (or similar notation) is a boxed <code style="border:1px solid rgb(206,206,206);background-color:rgb(248,248,248);padding:0px 3px;border-radius:4px">Word8</code>? And that would automatically be promoted to the type level.<br></div><div dir="ltr"><br></div><div dir="ltr">Really, shouldn’t both the boxed and unboxed variants be promotable to the type level?</div><div dir="ltr"><br></div><div dir="ltr">— Lyle</div><div dir="ltr"><br></div>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Oct 30, 2023 at 2:04:48 AM, Simon Peyton Jones <<a href="mailto:simon.peytonjones@gmail.com">simon.peytonjones@gmail.com</a>> wrote:<br></div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" type="cite">
<div dir="ltr"><div class="gmail_default" style="font-family:tahoma,sans-serif">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.</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">Simon<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 30 Oct 2023 at 08:20, Vladislav Zavialov via ghc-devs <<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">> I am working on some code where it is useful to have types indexed by a 16-bit unsigned value.<br>
<br>
This is great to hear. I've always wanted to make it possible to<br>
promote all numeric types: Natural, Word8, Word16, Word32, Word64,<br>
Integer, Int8, Int16, Int32, Int64. (Then, as the next step, even the<br>
floating-point types Float and Double). I see it as a step towards<br>
universal promotion, i.e. being able to use any data type as a kind.<br>
<br>
The problem is that such a change would require a GHC proposal, and I<br>
don't have a strong motivating use case to write one. But you seem to<br>
have one! If you'd like to co-author a GHC proposal and if the<br>
proposal gets accepted, I can implement the feature.<br>
<br>
Here's how I imagine it could work.<br>
<br>
1. Currently, a type-level literal like `15` is inferred to have kind<br>
`Nat` (and `Nat` is a synonym for `Natural` nowadays). At the<br>
term-level, however, the type of `15` is `forall {a}. Num a => a`. I'd<br>
like to follow the term-level precedent as closely as possible, except<br>
we don't have type class constraints in kinds, so it's going to be<br>
simply `15 :: forall {k}. k`.<br>
<br>
2. The desugaring should also follow the term-level precedent. `15`<br>
actually stands for `fromInteger (15 :: Integer)`, and I expect no<br>
less at the type level, where we could introduce a type family<br>
`FromInteger :: Integer -> k`, with the following instances<br>
<br>
type instance FromInteger @Natural n = NaturalFromInteger n<br>
type instance FromInteger @Word8 n = Word8FromInteger n<br>
type instance FromInteger @Word16 n = Word16FromInteger n<br>
...<br>
<br>
The helper type families `NaturalFromInteger`, `Word8FromInteger`,<br>
`Word16FromInteger` etc. are partial, e.g. `NaturalFromInteger (10 ::<br>
Integer)` yields `10 :: Natural` whereas `NaturalFromInteger (-10)` is<br>
stuck.<br>
<br>
I have a fairly good idea of what it'd take to implement this (i.e.<br>
the changes to the GHC parser, type checker, and libraries), and the<br>
change has been on my mind for a while. The use case that you have<br>
might be the last piece of the puzzle to get this thing rolling.<br>
<br>
Can you tell more about the code you're writing? Would it be possible<br>
to use it as the basis for the "Motivation" section of a GHC proposal?<br>
<br>
Vlad<br>
<br>
On Mon, Oct 30, 2023 at 6:06 AM Viktor Dukhovni <<a href="mailto:ietf-dane@dukhovni.org" target="_blank">ietf-dane@dukhovni.org</a>> wrote:<br>
><br>
> I am working on some code where it is useful to have types indexed by a<br>
> 16-bit unsigned value.<br>
><br>
> Presently, I am using type-level naturals and having to now and then<br>
> provide witnesses that a 'Nat' value I am working with is at most 65535.<br>
><br>
> Also, perhaps there's some inefficiency here, as Naturals have two<br>
> constructors, and so a more complex representation with (AFAIK) no<br>
> unboxed forms.<br>
><br>
> I was wondering what it would take to have type-level fixed-size<br>
> Words (Word8, Word16, Word32, Word64) to go along with the Nats?<br>
><br>
> It looks like some of the machinery (KnownWord16, SomeWord16, wordVal16,<br>
> etc.) can be copied straight out of GHC.TypeNats with minor changes, and<br>
> that much works, but the three major things that are't easily done seem<br>
> to be:<br>
><br>
> - There are it seems no TypeReps for types of Kind Word16, so one can't<br>
> have (Typeable (Foo w)) with (w :: Word16).<br>
><br>
> - There are no literals of a promoted Word16 Kind.<br>
><br>
> type Foo :: Word16 -> Type<br>
> data Foo w = MkFoo Int<br>
><br>
> -- 1 has Kind 'Natural' (a.k.a. Nat)<br>
> x = MkFoo 13 :: Foo 1 -- Rejected,<br>
><br>
> -- The new ExtendedLiterals syntax does not help<br>
> --<br>
> x = MkFoo 13 :: Foo (W16# 1#Word16) -- Syntax error!<br>
><br>
> - There are unsurprisingly also no built-in 'KnownWord16' instances<br>
> for any hypothetical type-level literals of Kind Word16.<br>
><br>
> Likely the use case for type-level fixed-size words is too specialised<br>
> to rush to shoehorn into GHC, but is there something on the not too<br>
> distant horizon that would make it easier and reasonable to have<br>
> fixed-size unsigned integral type literals available?<br>
><br>
> [ I don't see a use-case for unsigned versions, they can trivially be<br>
> represented by the unsigned value of the same width. ]<br>
><br>
> With some inconvenience, in many cases I can perhaps synthesise Proxies<br>
> for types of Kind Word16, and just never use literals directly.<br>
><br>
> --<br>
> Viktor.<br>
> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>
<div>
<div>
_______________________________________________<br>ghc-devs mailing list<br><a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</div>
</div>
</blockquote>
</div></body></html>