Bounded TypeNats (e.g. to range of Word16)

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)
1 Like

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)

1 Like

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)

Also, UndecidableInstances is quite harmless.

1 Like

I have two question about the above example.

  • 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).

1 Like

GHC.TypeLits.cmpNat!

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE
  MagicHash,
  DataKinds,
  AllowAmbiguousTypes,
  GADTs,
  BlockArguments
#-}

module Main where

import GHC.TypeLits
import GHC.Exts
import Data.Proxy
import Data.Word
import Data.Maybe

...

wordToNat16 :: Word16 -> SomeNat16
wordToNat16 w = fromJust do
  SomeNat n <- someNatVal (fromIntegral w)
  case cmpNat n (Proxy @65536) of
    LTI -> Just (SomeNat16 n)
    EQI -> Nothing
    GTI -> Nothing

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)

The first half of the file I used to test what I posted:

{-# LANGUAGE GHC2021, GADTs, DataKinds, PatternSynonyms, BlockArguments #-}

module Nat16 where

-- GHC/base
import GHC.TypeNats (Nat, SNat, pattern SNat, CmpNat, natVal, withSomeSNat)

-- base
import Data.Type.Equality ((:~:)(..))
import Data.Word (Word16)
import Unsafe.Coerce (unsafeCoerce)

Re newtypes, I posted about the technique recently: GADTs That Can Be Newtypes and How to Roll 'Em · GitHub

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.

  • You comment that data SNat16 n could be a newtype. How?
    • Or is just that, by using Data.Some.Newtype, the derived Some SNat16 is a newtype?
    • What is the representation of that value?
      • With SNat ultimately just a newtype around a Natural, and SNat16 existentially wrapping a SNat is Some SNat16 just a coercion of a Natural?
  • Your natToWord16 takes SNat16 value, what I managed to get working took a Some Snat16. The difference looks superficial, just:
λ> x = wordToNat16 42
λ> case x of { Some fx -> natToWord16 fx }
42

vs.

λ> x = wordToNat16 42
λ> natToWord16 x
42

Is there a reason to prefer one or the other definition?

Inlining type Nat16 n = CmpNat n 65536 ~ LT,

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…