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@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.peytonjo...@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@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-d...@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@haskell.org >> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> _______________________________________________ >> ghc-devs mailing list >> ghc-devs@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs