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