Data.SNumber

Runtime witnesses of type-level integers.

SNumber

data SNumber a (n :: Integer) where

SNumber a n is a runtime representation of the value of n.

For N# n :: SNumber a n and N# m :: SNumber a m, the following must hold:

• n ~ m iff n == m (according to the Eq instance of a).
• CmpInteger m n ~ 'LT iff compare m n == LT (according to Ord).
• CmpInteger m n ~ 'EQ iff compare m n == EQ.
• CmpInteger m n ~ 'GT iff compare m n == GT.
• toInteger n == integerVal @n.
• a upholds the Ord laws.

These are exactly the set of things we're willing to unsafeCoerce proofs for. It is unsafe to construct an SNumber that violates these by any means.

Note that the first requirement means that you must never construct N# 0 :: SNumber _ ('Neg 0), because that would prove that 'Neg 0 ~ 'Pos 0. In practice, we largely ignore the existence of 'Neg 0: trySNumber (and, by extension, the instance derivation via KnownInteger) will throw a runtime error when trying to construct 'Neg 0, and SafeSNumber instances explicitly exclude 'Neg 0 with type-level checks.

There are six main ways to introduce an SNumber, from the cartesian product of several choices

• How do you validate that the value is in-bounds for the representation type?

  • If by runtime checks, the function name has a "try" infix.
  • If by trusting the caller blindly, the function name has an "unsafe" prefix and an "Unchecked" infix.
  • If by type-level bounds checks, the function name has neither of these.

• How do you validate that the runtime Integer value matches the type-level Integer?

  • If by trusting the user to pass in the right Integer, the function has an "unsafe" prefix and a "Mk" infix: we're "making" the SNumber from a runtime value rather than deriving it from KnownNat.
  • If by getting it from a KnownNat instance, the function name doesn't have that infix.

Thus:

• snumber: type-level checks, safe KnownNat.
• trySNumber: runtime checks, safe KnownNat.
• unsafeUncheckedSNumber: no checks, safe KnownNat.
• unsafeMkSNumber: type-level checks, unsafe Integer parameter.
• unsafeTryMkSNumber: runtime checks, unsafe Integer parameter.
• unsafeUncheckedMkSNumber: no checks, unsafe a parameter. a.k.a. N#.

Finally, there's one other way to get an SNumber: by asking the constraint solver to give you one, with a KnownSNumber class and its snumberVal method. Currently, this will be solved automatically from KnownNat by using trySNumber, and of course it can be solved from a matching instance in the function's context (which compiles to an a parameter for KnownSNumber a n).

Bundled Patterns

pattern SNumber :: forall (n :: Integer) a. SNumberRepr a => KnownSNumber a n => SNumber a n

Treat SNumber as if it were a GADT containing a KnownSNumber instance.

pattern N# :: forall (n :: Integer) a. a -> SNumber a n

Create an SNumber for n, with no safety measures whatsoever.

This pattern is identical to the newtype constructor of SNumber except that it isn't actualy a newtype constructor, so having it in scope doesn't allow unsound coercions across SNumber types.

pattern SN :: forall (n :: Integer) a. a -> SNumber a n

A unidirectional pattern for matching SNumbers.

This allows the pseudo-field-selector unSNumber to be exported bundled with SNumber, so it can be imported by SNumber(..) as if it were a normal field selector of a record definition. If this were done as part of N#, it'd allow unsafely changing an SNumber's representation without using any identifiers that indicate unsafety, by way of record update syntax.

Instances

Show a => Show (SNumber a n)

Defined in Data.SNumber

Methods

showsPrec :: Int -> SNumber a n -> ShowS

show :: SNumber a n -> String

showList :: [SNumber a n] -> ShowS

class Integral a => SNumberRepr a

The class of types that are suitable for use as integer value witnesses.

Implementing an instance of this class amounts to asserting that the type and its Integral, Ord, and Eq instances uphold the requirements of SNumber, for any integer n that satisfies SafeSNumber a n.

Furthermore, it requires that every value of a is an integer, i.e. that forall x :: a. exists y :: Integer. x == fromInteger y, toInteger x == y. This ensures we can wrap any a in SomeSNumberVal and be sure it corresponds to a valid K.Integer.

Associated Types

type SafeSNumber a :: Integer -> Constraint

SafeSNumber a n witnesses that N# n is a valid SNumber a n.

Instances

SNumberRepr Int

Defined in Data.SNumber

Associated Types

type SafeSNumber Int :: Integer -> Constraint

SNumberRepr Integer

Defined in Data.SNumber

Associated Types

type SafeSNumber Integer :: Integer -> Constraint

SNumberRepr Natural

Defined in Data.SNumber

Associated Types

type SafeSNumber Natural :: Integer -> Constraint

SNumberRepr Word

Defined in Data.SNumber

Associated Types

type SafeSNumber Word :: Integer -> Constraint

Creation

snumber :: forall n a. (SNumberRepr a, SafeSNumber a n, KnownInteger n) => SNumber a n

Construct an SNumber, doing all validation at the type level.

This is completely safe and cannot raise runtime errors.

trySNumber :: forall n a. (SNumberRepr a, KnownInteger n) => Maybe (SNumber a n)

Create an SNumber for n, if it's faithfully represented by a.

This is completely safe, but it may raise runtime errors, because it tests at runtime whether a can represent n correctly.

Unsafe

unsafeUncheckedSNumber :: forall n a. (Num a, KnownInteger n) => SNumber a n

Create an SNumber from a KnownInteger constraint without any checks.

This will cause type unsoundness if the value is not correctly represented by a or if the instances of a do not behave according to the safety requirements described on SNumber.

unsafeMkSNumber :: forall n a. SafeSNumber a n => a -> SNumber a n

Semi-safely construct an SNumber as if by N#.

Callers must ensure that the a argument is fromInteger (integerVal n) (semantically, not syntactically: unsafeSNumber ('Pos 42) 42 is fine and is in fact the intended use case).

The extra constraint here compared to N# ensures that if you write unsafeMkSNumber @n (fromInteger n), the result is either a valid SNumber or a type error. In particular, the cases this rules out are those where toInteger (fromInteger n :: a) /= n or where fromInteger m :: a == fromInteger n does not imply m == n.

unsafeTryMkSNumber :: forall n a. SNumberRepr a => Integer -> Maybe (SNumber a n)

Create an SNumber for n, if it's faithfully represented by a.

As with unsafeMkSNumber, this trusts you to pass integerVal @n, and violating that will lead to type unsoundness.

This tests at runtime whether a represents n correctly.

unsafeUncheckedMkSNumber :: forall n a. a -> SNumber a n

Create an SNumber for n, with no safety measures whatsoever.

Existentials

data SomeSNumber a

An SNumber with an existential Integer type parameter.

Constructors

forall n. SomeSNumber (SNumber a n)

someSNumberVal :: SNumberRepr a => a -> SomeSNumber a

Create an SNumber a from any value of type a.

Since SNumberRepr guarantees every a value is an integer, we can freely wrap up a value in an SNumber with existential Integer type parameter.

withSNumber :: SNumberRepr a => a -> (forall n. SNumber a n -> r) -> r

Like someSNumberVal, but in quantified CPS style rather than GADT style.

Comparison

compareSNumber :: forall m n a. Ord a => SNumber a m -> SNumber a n -> OrderingI m n

Compare two type-level Integers using their runtime witnesses.

sameSNumber :: Eq a => SNumber a m -> SNumber a n -> Maybe (m :~: n)

Test equality of two type-level Integers using their runtime witnesses.

Arithmetic

class Integral a => OverflowArith a where

Arithmetic ops with overflow detection.

Laws:

• overflowAdd x y = (False, xy) =>
        toInteger xy === toInteger x + toInteger y

• overflowSub x y = (False, xy) =>
        toInteger xy === toInteger x - toInteger y

• overflowMul x y = (False, xy) =>
        toInteger xy === toInteger x * toInteger y

This is used for arithmetic on SNumber runtime values, so creating incorrect instances is type-unsafe.

Methods

overflowAdd :: a -> a -> (Bool, a)

overflowSub :: a -> a -> (Bool, a)

overflowMul :: a -> a -> (Bool, a)

Instances

OverflowArith Int

Defined in Data.SNumber

Methods

overflowAdd :: Int -> Int -> (Bool, Int)

overflowSub :: Int -> Int -> (Bool, Int)

overflowMul :: Int -> Int -> (Bool, Int)

OverflowArith Integer

Defined in Data.SNumber

Methods

overflowAdd :: Integer -> Integer -> (Bool, Integer)

overflowSub :: Integer -> Integer -> (Bool, Integer)

overflowMul :: Integer -> Integer -> (Bool, Integer)

OverflowArith Natural

Defined in Data.SNumber

Methods

overflowAdd :: Natural -> Natural -> (Bool, Natural)

overflowSub :: Natural -> Natural -> (Bool, Natural)

overflowMul :: Natural -> Natural -> (Bool, Natural)

OverflowArith Word

Defined in Data.SNumber

Methods

overflowAdd :: Word -> Word -> (Bool, Word)

overflowSub :: Word -> Word -> (Bool, Word)

overflowMul :: Word -> Word -> (Bool, Word)

In Maybe

tryAdd :: (SNumberRepr a, OverflowArith a) => SNumber a m -> SNumber a n -> Maybe (SNumber a (m + n))

Compute a runtime witness of m + n, or Nothing.

trySub :: (SNumberRepr a, OverflowArith a) => SNumber a m -> SNumber a n -> Maybe (SNumber a (m - n))

Compute a runtime witness of m - n, or Nothing.

tryMul :: (SNumberRepr a, OverflowArith a) => SNumber a m -> SNumber a n -> Maybe (SNumber a (m * n))

Compute a runtime witness of m * n, or Nothing.

Checked

data UnrepresentableSNumber

An exception for overflows in checked SNumber arithmetic.

Constructors

UnrepresentableSNumber String Integer Integer

Instances

Show UnrepresentableSNumber

Defined in Data.SNumber

Methods

showsPrec :: Int -> UnrepresentableSNumber -> ShowS

show :: UnrepresentableSNumber -> String

showList :: [UnrepresentableSNumber] -> ShowS

Exception UnrepresentableSNumber

Defined in Data.SNumber

Methods

toException :: UnrepresentableSNumber -> SomeException

fromException :: SomeException -> Maybe UnrepresentableSNumber

displayException :: UnrepresentableSNumber -> String

chkAdd :: (SNumberRepr a, OverflowArith a, HasCallStack) => SNumber a m -> SNumber a n -> SNumber a (m + n)

Compute a runtime witness of m + n, or throw.

chkSub :: (SNumberRepr a, OverflowArith a, HasCallStack) => SNumber a m -> SNumber a n -> SNumber a (m - n)

Compute a runtime witness of m - n, or throw.

chkMul :: (SNumberRepr a, OverflowArith a, HasCallStack) => SNumber a m -> SNumber a n -> SNumber a (m * n)

Compute a runtime witness of m * n, or throw.

Infallible

divExact :: SNumberRepr a => SNumber a (m * n) -> SNumber a n -> SNumber a m

Compute a runtime witness of exact division.

We could provide division in terms of Div instead, but Kinds.Integer doesn't currently have division.

Reification to Constraints

class KnownSNumber a n where

Like KnownNat, but represented by a instead of Natural.

This is currently solved automatically from KnownNat via runtime checks, to ease migration (we can incrementally strengthen KnownNat constraints to KnownSNumber constraints), but in the future it may be changed to use SafeSNumber, which will rule out runtime failures but will require additional proofs in order to solve via KnownNat. For statically known Integers, these proofs will be entirely automatic.

This class is meant to be used primarily in instance contexts; for standalone functions, it's probably better to pass an SNumber explicitly.

Minimal complete definition

Nothing

Methods

snumberVal_ :: SNumber a n

Implementation of snumberVal.

This has an inconvenient type variable order because it derives from the order they appear in the class head; see snumberVal.

default snumberVal_ :: (SNumberRepr a, KnownInteger n) => SNumber a n

Instances

(SNumberRepr a, KnownInteger n) => KnownSNumber a n

Defined in Data.SNumber

Methods

snumberVal_ :: SNumber a n

snumberVal :: forall n a. KnownSNumber a n => SNumber a n

Get an SNumber out of the context from KnownSNumber or KnownNat.

This has the number as its first type parameter, for TypeApplications convenience.

reifySNumber :: forall a n r. SNumber a n -> (KnownSNumber a n => r) -> r

Stash an SNumber at the type level as a KnownSNumber instance.

reifySNumberAsNat :: forall n r a. Integral a => SNumber a ('Pos n) -> (KnownNat n => r) -> r

Use a positive SNumber to introduce a KnownNat instance.

Miscellaneous

type IntBits = 64

The number of bits in the present system's Int type.

type IntMin = 'Neg (2 ^ (IntBits - 1))

The smallest representable Int value.

type IntMaxP1 = 'Pos (2 ^ (IntBits - 1))

One more than the largest representable Int value.

type WordBits = 64

The number of bits in the present system's Word type.

type WordMaxP1 = 'Pos (2 ^ WordBits)

One more than the largest representable Word value.