Safe Haskell | None |
---|---|

Language | Haskell2010 |

Provides a singleton type for a subset of `Nat`

s, 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
`Int`

s. Thus, there's no need to pay the runtime cost of lugging around
`Natural`

s to handle greater-than-maxInt-length arrays, since the underlying
primitives don't handle them either.

An

is trusted absolutely by downstream code to contain an `SInt`

n`Int`

`n'`

s.t. `fromIntegral n' == natVal' @n Proxy#`

. In particular, this
trust extends to a willingness to use two runtime-equal `SInt`

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

`SInt`

s are constructed safely by `staticSIntVal`

with no overhead,
by `sintVal`

with runtime bounds checks based on a `KnownNat`

instance, or
by various arithmetic functions.

## Synopsis

- data SInt (n :: Nat) where
- trySIntVal :: forall n. KnownNat n => Maybe (SInt n)
- sintVal :: forall n. (HasCallStack, KnownNat n) => SInt n
- reifySInt :: forall n r. SInt n -> (KnownNat n => r) -> r
- withSInt :: HasCallStack => Int -> (forall n. SInt n -> r) -> r
- addSInt :: HasCallStack => SInt m -> SInt n -> SInt (m + n)
- subSInt :: HasCallStack => SInt m -> SInt n -> SInt (m - n)
- subSIntLE :: n <= m => SInt m -> SInt n -> SInt (m - n)
- subSIntL :: SInt (m + n) -> SInt m -> SInt n
- mulSInt :: HasCallStack => SInt m -> SInt n -> SInt (m * n)
- divSIntL :: SInt (m * n) -> SInt m -> SInt n
- divSIntR :: SInt (m * n) -> SInt n -> SInt m
- staticSIntVal :: forall n. (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n
- type IntMaxP1 = 2 ^ (64 - 1)

# Documentation

data SInt (n :: Nat) where Source #

pattern SI# :: Int -> SInt n | Construct an See the module intro for more details; prefer to use safe methods to
construct |

pattern SI :: Int -> SInt n | A unidirectional pattern for safely deconstructing This lets us export |

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

Subtract two `SInt`

s, using an inequality constraint to rule out overflow.

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

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`

.