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 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

Modulo the backward-compatibility piece around today's type-level numbers, I'm in support of this direction. No new type machinery is needed, other than a new interpretation for literals, because type families can already infer a kind argument from the return kind. This is almost entirely a change to libraries, not to GHC itself. Richard

On Oct 30, 2023, at 5:32 AM, Vladislav Zavialov via ghc-devs wrote:

I agree caution is warranted, but I still want the type level to behave as closely as possible to the term level, where literals are currently overloaded.

I don't care if it's monomorphic literals everywhere or overloaded literals everywhere, but I oppose a discrepancy.

Vlad

On Mon, Oct 30, 2023, 10:05 Simon Peyton Jones mailto:simon.peytonjones@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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

On Mon, Oct 30, 2023 at 09:20:16AM +0100, Vladislav Zavialov via ghc-devs wrote:

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?

Working with DNS resource records (A, NS, CNAME, SOA, MX, SRV, ...) requires a runtime extensible data model: - Some RR types will be known at DNS-library compile-time. - Some RR types can defined and added at runtime (application compile-time, and registered with the DNS library). - Some RR types may appear "on the wire" in serialised form, with the RRTYPE not known to either the library or application code. The library data model has separate types for the "rrData" parts of each resource record type, which are existentially quantified in the RR: RR { rrOwner, rrTTL, rrClass, rrData :: RData } RData = forall a. KnownRData a => RData a with the usual: fromRData :: KnownRData a => RData -> Maybe a fromRData (RData a) = cast a To filter a list of resource records to those of a particular RR type, I have: monoList :: forall a t. (KnownRData a, Foldable t) => t RData -> [a] monoList = foldr (maybe id (:) . fromRData) go [] I'd like to be able to use this also to distinguish between "OpaqueRData" resource record types, so there's actually a separate opaque type for each 16-bit RR number: {-# LANGUAGE AllowAmbiguousTypes #-} type OpaqueRData :: Word16 -> Type data OpaqueRData w = OpaqueRData { getOpaqueRData :: Bytes16 } -- Nat16 constraint enforces 65535 ceiling -- natVal16 returns Nat as Word16. -- instance Nat16 n => KnownRData (OpaqueRData n) where rdType = RRTYPE $ natVal16 @n This works, because the phantom indices have to match for "cast" to return a Just value, so that, for example: λ> x1 = RData $ (OpaqueRData (coerce ("abc" :: ShortByteString)) :: OpaqueRData 1) λ> fromRData x1 :: (Maybe (OpaqueRData 1)) Just (OpaqueRData @1 "616263") λ> fromRData x1 :: (Maybe (OpaqueRData 2)) Nothing λ> l1 = monoList [x1] :: [OpaqueRData 1] λ> l2 = monoList [x1] :: [OpaqueRData 2] λ> hPutBuilder stdout $ foldr (presentLn) ("That's all folks!\n") l1 \# 3 616263 That's all folks! λ> hPutBuilder stdout $ foldr (presentLn) ("That's all folks!\n") l2 That's all folks! In addition to labeling unknown RData with Word16 values, I also type-index unknown EDNS options (they're elements of the OPT pseudo RR that carries DNS protocol extensions) and unknown SVCB/HTTPS key/value service parameter pairs. Applications can register novel RData types, EDNS options, and SVCB key/value types at runtime, and the extended code points behave just like the "built-in" ones, because the only "built-in" code points are the opaque ones, the others are registered at runtime by the library as part of default resolver settings. So this is how I end up with Word16-indexed types. One might argue that "OpaqueRData" could be a single type, and that filtering by RRTYPE should have the "rrType" method taking a value to optionally inspect, but I like the type-level separation even between Opaque data of different RRTYPEs, and ditto for EDNS options and SVCB/HTTPS fields. This supports view patterns: f (fromRData -> Just (T_a ipv4)) = ... f (fromRData -> Just (T_aaaa ipv6)) = ... which should "morally" also work for: getBlob42 :: OpaqueRData 42 -> ShortByteString getBlob42 = fromBytes16 . getOpaqueRData f (fmap getBlob42 . fromRData -> Just blob) = ... yielding just the serialised blobs of RRTYPE 42, with little chance of accidentally pulling in blobs of the wrong RRTYPE. I may before long add an associated type to the KnownRData class: type RdType :: Nat -- Ideally some day Word16 making it possible to write: -- Identity functions on the actual Opaque types. toOpaque :: a -> Opaque (RdType a) fromOpaque :: Opaque (RdType a) -> a at which point a simple tweak to the above "blob" pattern match could also work when the RRtype 42 was decoded as known: f (fmap getBlob42 . fromRData . toOpaque -> Just blob)) = ... -- Viktor.