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

Language | Haskell2010 |

Runtime witnesses of type-level integers.

## Synopsis

- data SNumber a (n :: Integer) where
- class Integral a => SNumberRepr a where
- type SafeSNumber a :: Integer -> Constraint

- snumber :: forall n a. (SNumberRepr a, SafeSNumber a n, KnownInteger n) => SNumber a n
- trySNumber :: forall n a. (SNumberRepr a, KnownInteger n) => Maybe (SNumber a n)
- unsafeUncheckedSNumber :: forall n a. (Num a, KnownInteger n) => SNumber a n
- unsafeMkSNumber :: forall n a. SafeSNumber a n => a -> SNumber a n
- unsafeTryMkSNumber :: forall n a. SNumberRepr a => Integer -> Maybe (SNumber a n)
- unsafeUncheckedMkSNumber :: forall n a. a -> SNumber a n
- data SomeSNumber a = forall n. SomeSNumber (SNumber a n)
- someSNumberVal :: SNumberRepr a => a -> SomeSNumber a
- withSNumber :: SNumberRepr a => a -> (forall n. SNumber a n -> r) -> r
- data SOrdering m n where
- SLT :: CmpInteger m n ~ 'LT => SOrdering m n
- SEQ :: CmpInteger m n ~ 'EQ => SOrdering m n
- SGT :: CmpInteger m n ~ 'GT => SOrdering m n

- compareSNumber :: forall m n a. Ord a => SNumber a m -> SNumber a n -> SOrdering m n
- sameSNumber :: Eq a => SNumber a m -> SNumber a n -> Maybe (m :~: n)
- class Integral a => OverflowArith a where
- overflowAdd :: a -> a -> (Bool, a)
- overflowSub :: a -> a -> (Bool, a)
- overflowMul :: a -> a -> (Bool, a)

- tryAdd :: (SNumberRepr a, OverflowArith a) => SNumber a m -> SNumber a n -> Maybe (SNumber a (m + n))
- trySub :: (SNumberRepr a, OverflowArith a) => SNumber a m -> SNumber a n -> Maybe (SNumber a (m - n))
- tryMul :: (SNumberRepr a, OverflowArith a) => SNumber a m -> SNumber a n -> Maybe (SNumber a (m * n))
- data UnrepresentableSNumber = UnrepresentableSNumber String Integer Integer
- chkAdd :: (SNumberRepr a, OverflowArith a, HasCallStack) => SNumber a m -> SNumber a n -> SNumber a (m + n)
- chkSub :: (SNumberRepr a, OverflowArith a, HasCallStack) => SNumber a m -> SNumber a n -> SNumber a (m - n)
- chkMul :: (SNumberRepr a, OverflowArith a, HasCallStack) => SNumber a m -> SNumber a n -> SNumber a (m * n)
- divExact :: SNumberRepr a => SNumber a (m * n) -> SNumber a n -> SNumber a m
- class KnownSNumber a n where
- snumberVal_ :: SNumber a n

- snumberVal :: forall n a. KnownSNumber a n => SNumber a n
- reifySNumber :: forall a n r. SNumber a n -> (KnownSNumber a n => r) -> r
- reifySNumberAsNat :: forall n r a. Integral a => SNumber a ('Pos n) -> (KnownNat n => r) -> r
- type IntBits = 64
- type IntMin = 'Neg (2 ^ (IntBits - 1))
- type IntMaxP1 = 'Pos (2 ^ (IntBits - 1))
- type WordBits = 64
- type WordMaxP1 = 'Pos (2 ^ WordBits)

# SNumber

data SNumber a (n :: Integer) where Source #

`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

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.

- 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

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`

).

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

pattern N# :: forall (n :: Integer) a. a -> SNumber a n | Create an This pattern is identical to the newtype constructor of |

pattern SN :: forall (n :: Integer) a. a -> SNumber a n | A unidirectional pattern for matching This allows the pseudo-field-selector |

class Integral a => SNumberRepr a Source #

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`

.

type SafeSNumber a :: Integer -> Constraint Source #

#### Instances

SNumberRepr Int Source # | |

Defined in Data.SNumber type SafeSNumber Int :: Integer -> Constraint Source # | |

SNumberRepr Integer Source # | |

Defined in Data.SNumber type SafeSNumber Integer :: Integer -> Constraint Source # | |

SNumberRepr Natural Source # | |

Defined in Data.SNumber type SafeSNumber Natural :: Integer -> Constraint Source # | |

SNumberRepr Word Source # | |

Defined in Data.SNumber type SafeSNumber Word :: Integer -> Constraint Source # |

## Creation

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

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) Source #

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 Source #

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 Source #

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) Source #

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 Source #

Create an `SNumber`

for `n`

, with no safety measures whatsoever.

## Existentials

data SomeSNumber a Source #

forall n. SomeSNumber (SNumber a n) |

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

Create an

from any value of type `SNumber`

a`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 Source #

Like `someSNumberVal`

, but in quantified CPS style rather than GADT style.

## Comparison

data SOrdering m n where Source #

Ordering results carrying evidence of type-level ordering relations.

SLT :: CmpInteger m n ~ 'LT => SOrdering m n | |

SEQ :: CmpInteger m n ~ 'EQ => SOrdering m n | This doesn't currently prove m ~ n, but since we've forbidden SNumbers
of |

SGT :: CmpInteger m n ~ 'GT => SOrdering m n |

compareSNumber :: forall m n a. Ord a => SNumber a m -> SNumber a n -> SOrdering m n Source #

Compare two type-level `Integer`

s using their runtime witnesses.

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

Test equality of two type-level `Integer`

s using their runtime witnesses.

## Arithmetic

class Integral a => OverflowArith a where Source #

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.

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

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

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

### In `Maybe`

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

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)) Source #

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)) Source #

Compute a runtime witness of `m * n`

, or `Nothing`

.

### Checked

data UnrepresentableSNumber Source #

#### Instances

Show UnrepresentableSNumber Source # | |

Defined in Data.SNumber showsPrec :: Int -> UnrepresentableSNumber -> ShowS # show :: UnrepresentableSNumber -> String # showList :: [UnrepresentableSNumber] -> ShowS # | |

Exception UnrepresentableSNumber Source # | |

Defined in Data.SNumber |

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

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) Source #

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) Source #

Compute a runtime witness of `m * n`

, or throw.

## Infallible

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

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 Source #

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
`Integer`

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

Nothing

snumberVal_ :: SNumber a n Source #

Implementation of `snumberVal`

.

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

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

#### Instances

(SNumberRepr a, KnownInteger n) => KnownSNumber a n Source # | |

Defined in Data.SNumber snumberVal_ :: SNumber a n Source # |

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

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 Source #

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 Source #