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