Re: Type-level sized Word literals???

[Lyle Kopnicky]

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

Re: Type-level sized Word literals???

[Viktor Dukhovni]

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

Re: Type-level sized Word literals???

[Richard Eisenberg]

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

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Type-level sized Word literals???

[Vladislav Zavialov via ghc-devs]

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

Re: 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@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
> 

Re: Type-level sized Word literals???

[Vladislav Zavialov via ghc-devs]

> 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

Type-level sized Word literals???

[Viktor Dukhovni]

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