In DNS code I’m working on I found a use for type-level naturals that are restricted to the range of a Word16.
It was tricky to produce a formulation in which the constraints worked as expected (seemingly cosmetic reformulations broke compilation) and did not require the UndecidableInstances extension. Have not had much luck in avoiding AllowAmbiguousTypes.
Is there a better way to express this than:
type Nat16 :: Nat -> Constraint
type Nat16 n = (KnownNat n, CmpNat n 65536 ~ 'LT)
data SomeNat16 where
SomeNat16 :: forall (n :: Nat). Nat16 n => Proxy n -> SomeNat16
-- | Convert 16-bit type-level natural to corresponding RRTYPE.
natToWord16 :: forall (n :: Nat). Nat16 n => Word16
natToWord16 = fromIntegral $ natVal' (proxy# :: Proxy# n)
-- | Convert RRTYPE to 16-bit natural @SomeNat@ singleton.
wordToNat16 :: Word16 -> SomeNat16
wordToNat16 w = case someNatVal $ fromIntegral w of
(SomeNat (_ :: Proxy n)) -> case unsafeCoerce Refl :: (CmpNat n 65536 :~: 'LT) of
Refl -> SomeNat16 (Proxy @n)
You can avoid AllowAmbigousTypes if you accept a proxy as an argument in your natToWord16 just like natVal' does, or you can use forall-> from the RequiredTypeArguments extension (it was introduced in ghc 9.10)
Personally, I would write it like this (but as newtypes):
type Nat16 n = CmpNat n 65536 ~ LT
-- Can be written as a newtype.
data SNat16 (n :: Nat) where
SNat16 :: Nat16 n => !(SNat n) -> SNat16 n
-- This one too, or get it from Data.Some.Newtype.
data Some f where
Some :: f x -> Some f
-- | Convert 16-bit type-level natural to corresponding RRTYPE.
natToWord16 :: SNat16 n -> Word16
natToWord16 n@(SNat16 SNat) = fromIntegral (natVal n)
-- | Convert RRTYPE to 16-bit natural @SomeNat@ singleton.
wordToNat16 :: Word16 -> Some SNat16
wordToNat16 w = withSomeSNat (fromIntegral w) \n -> case magic n of
Refl -> Some (SNat16 n)
where
magic :: proxy n -> CmpNat n 65536 :~: LT
magic _ = unsafeCoerce (Refl @LT)
What extensions and imports were used to get this to compile?
When you mention newtypes, what did you have in mind?
(FWIW, the documentation of Data.Some.Newtype leaves me none the wiser. There are no examples showing how one might use this or introductory prose explaining what problem this is solving. Just the function signatures are far from sufficient).
I think I have approximately the suggested approach, but still not quite clear on making SNat16 into a newtype…
{-# LANGUAGE
GHC2024
, BlockArguments
, DataKinds
, MagicHash
, PatternSynonyms
, ScopedTypeVariables
, TypeApplications
#-}
module Nat16
( type Nat16
, Nat
, natToWord16
, wordToNat16
) where
import Data.Kind (Constraint)
import Data.Typeable ((:~:)(Refl))
import Data.Word (Word16)
import GHC.TypeNats ( Nat, KnownNat, CmpNat, natVal, someNatVal
, withSomeSNat, SNat, pattern SNat)
import GHC.Exts (proxy#)
import Unsafe.Coerce (unsafeCoerce)
import Data.Some.Newtype
type Nat16 :: Nat -> Constraint
type Nat16 n = (KnownNat n, CmpNat n 65536 ~ LT)
-- Can be written as a newtype.
data SNat16 (n :: Nat) where
SNat16 :: Nat16 n => !(SNat n) -> SNat16 n
-- | Convert 16-bit type-level natural to corresponding RRTYPE.
natToWord16 :: Some SNat16 -> Word16
natToWord16 sn = withSome sn go
where
go :: forall n. SNat16 n -> Word16
go (SNat16 p) = fromIntegral $ natVal p
-- | Convert RRTYPE to 16-bit natural @SomeNat@ singleton.
wordToNat16 :: Word16 -> Some SNat16
wordToNat16 w = withSomeSNat (fromIntegral w) go
where
go :: forall n. SNat n -> Some SNat16
go s@SNat = case magic s of { Refl -> Some (SNat16 s) }
magic :: proxy n -> CmpNat n 65536 :~: LT
magic _ = unsafeCoerce (Refl @LT)
Re Some, there’s really nothing to know about it beyond its data declaration: it hides the (last) type variable of its argument. So instead of writing your own SomeFoos and SomeBars, you just import Data.Newtype.Some to use Some Foo and Some Bar.
data SNat16 (n :: Nat) where
SNat16 :: CmpNat n 65536 ~ LT => !(SNat n) -> SNat16 n
matches the pattern in the Equality Constraints section of the article I linked, with L n = CmpNat n 65536, R _ = LT and F = SNat. So the representation would be that of SNat n, i.e. Natural. With Some also being written as a newtype, Some SNat16 would naturally be the same.
wordToNat16 produces a Some SNat16 because it needs to; the function is existential in the hidden n. natToWord16 is universal in n, which Haskell handles just fine without wrappers; it doesn’t need Some, so it shouldn’t be used.
Thanks, that’s helpful. I’ll take a look at the Equality overview.
If at all possible, I’d like to appeal for more detailed documentation of the some library’s modules. They really do need an Overview section accessible to non-experts, and perhaps some examples using the various combinators along with the signatures. Perhaps not quite as detailed as what I contributed for Data.Foldable and Data.Traversable, but a few steps in that direction would be helpful.
Though I’ve been using Haskell for some years, it’s been largely about taking advantage of robust concurrency, much more than sophisticated gymnastics with higher-kinded types, and the terse docs of the library and even the Github notes are sadly rough going…