Data.SInt

Provides a singleton type for a subset of Nats, represented by Int.

This is particularly useful when working with length-indexed array types, since the array primitives generally expect lengths and indices to be Ints. Thus, there's no need to pay the runtime cost of lugging around Naturals to handle greater-than-maxInt-length arrays, since the underlying primitives don't handle them either.

An SInt n is trusted absolutely by downstream code to contain an Int n' s.t. fromIntegral n' == natVal' @n Proxy#. In particular, this trust extends to a willingness to use two runtime-equal SInts as proof that their type parameters are equal, or to use GHC primitives in a way that's only memory-safe if this property holds. This means it should be considered unsafe to construct an SInt in any way that's not statically guaranteed to produce the correct runtime value, and to construct one with an incorrect runtime value is equivalent to using unsafeCoerce incorrectly.

SInt should be seen as a more efficient implementation of data SNat n = KnownNat n => SNat, so that constructing an incorrect SInt would be equivalent to producing an incorrect KnownNat instance.

SInts are constructed safely by staticSIntVal with no overhead, by sintVal with runtime bounds checks based on a KnownNat instance, or by various arithmetic functions.

Documentation

data SInt (n :: Nat) where

A singleton type linking a runtime Int and a type-level Nat.

Bundled Patterns

pattern SI# :: Int -> SInt n

Construct an SInt unsafely. Incorrect uses cause undefined behavior.

See the module intro for more details; prefer to use safe methods to construct SInts, and treat this constructor equivalently to unsafeCoerce.

pattern SI :: Int -> SInt n

A unidirectional pattern for safely deconstructing SInts.

This lets us export unSInt as if it were a field selector, without making it legal to use in record updates (because this pattern is unidirectional).

Instances

Show (SInt n)

Defined in Data.SInt

Methods

showsPrec :: Int -> SInt n -> ShowS

show :: SInt n -> String

showList :: [SInt n] -> ShowS

Portray (SInt n)

Defined in Data.SInt

Methods

portray :: SInt n -> Portrayal

portrayList :: [SInt n] -> Portrayal

Diff (SInt n)

Defined in Data.SInt

Methods

diff :: SInt n -> SInt n -> Maybe Portrayal

trySIntVal :: forall n. KnownNat n => Maybe (SInt n)

Produce an SInt for a given KnownNat, or Nothing if out of range.

sintVal :: forall n. (HasCallStack, KnownNat n) => SInt n

Produce an SInt for a given KnownNat, or error if out of range.

reifySInt :: forall n r. SInt n -> (KnownNat n => r) -> r

Bring an SInt back into the type level as a KnownNat instance.

withSInt :: HasCallStack => Int -> (forall n. SInt n -> r) -> r

Use an Int as an existentially-quantified SInt.

addSInt :: HasCallStack => SInt m -> SInt n -> SInt (m + n)

Add two SInts with bounds checks; error if the result overflows.

subSInt :: HasCallStack => SInt m -> SInt n -> SInt (m - n)

Subtract two SInts with bounds checks; error if the result is negative.

subSIntLE :: n <= m => SInt m -> SInt n -> SInt (m - n)

Subtract two SInts, using an inequality constraint to rule out overflow.

subSIntL :: SInt (m + n) -> SInt m -> SInt n

"Un-add" an SInt from another SInt, on the left.

This form of subSInt is more convenient in certain cases when a type signature ensures a particular SInt is of the form m + n.

mulSInt :: HasCallStack => SInt m -> SInt n -> SInt (m * n)

Multiply two SInts with bounds checks; error if the result overflows.

divSIntL :: SInt (m * n) -> SInt m -> SInt n

"Un-multiply" an SInt by another SInt, on the left.

This form of divSInt is more convenient in certain cases when a type signature ensures a particular SInt is of the form m * n.

divSIntR :: SInt (m * n) -> SInt n -> SInt m

"Un-multiply" an SInt by another SInt, on the right.

This form of divSInt is more convenient in certain cases when a type signature ensures a particular SInt is of the form m * n.

staticSIntVal :: forall n. (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n

Like sintVal, but with static proof that it's in-bounds.

This optimizes down to an actual primitive literal wrapped in the appropriate constructors, unlike sintVal, where the bounds checking gets in the way. If you're constructing a statically-known SInt, use staticSIntVal; while if you're constructing an SInt from a runtime KnownNat instance, you'll have to use sintVal.

Internal

type IntMaxP1 = 2 ^ (64 - 1)

One more than the maximum representable Int on the current platform.