diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,3 @@ +# 0.1.0.0 + +Initial version. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,202 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/snumber.cabal b/snumber.cabal new file mode 100644 --- /dev/null +++ b/snumber.cabal @@ -0,0 +1,48 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.33.0. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: 1d0ab9e8374cc94aff152971e0a8de1ddbc04e736cfa1bffd8722cff99b603c6 + +name: snumber +version: 0.1.0.0 +synopsis: Indexed numeric types linking type-level and value-level numbers. +description: This provides singletons-style witnesses for type-level integers, and some + limited arithmetic operations on them. Instead of working with (invisible, + implicitly-passed) 'KnownNat' instances, you can work with (visible, + explicitly-mentioned) 'SNumber' values, and can freely convert between the + two forms. + . + This primarily exists in support of + . +category: Constraints +homepage: https://github.com/google/hs-dependent-literals#readme +bug-reports: https://github.com/google/hs-dependent-literals/issues +author: Andrew Pritchard +maintainer: Andrew Pritchard +copyright: 2020-2021 Google LLC +license: Apache-2.0 +license-file: LICENSE +build-type: Simple +extra-source-files: + CHANGELOG.md + +source-repository head + type: git + location: https://github.com/google/hs-dependent-literals + subdir: snumber + +library + exposed-modules: + Data.SNumber + other-modules: + Data.SNumber.Internal + Paths_snumber + hs-source-dirs: + src + build-depends: + base >=4.12 && <4.16 + , numeric-kinds >=0.1 && <0.2 + default-language: Haskell2010 diff --git a/src/Data/SNumber.hs b/src/Data/SNumber.hs new file mode 100644 --- /dev/null +++ b/src/Data/SNumber.hs @@ -0,0 +1,551 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +-- | Runtime witnesses of type-level integers. + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoStarIsType #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} + +module Data.SNumber + ( -- * SNumber + SNumber(N#, SNumber, unSNumber), SNumberRepr(..) + + -- ** Creation + , snumber, trySNumber, unsafeUncheckedSNumber + , unsafeMkSNumber, unsafeTryMkSNumber, unsafeUncheckedMkSNumber + + -- ** Existentials + , SomeSNumber(..), someSNumberVal, withSNumber + + -- ** Comparison + , SOrdering(..), compareSNumber, sameSNumber + + -- ** Arithmetic + , OverflowArith(..) + + -- *** In 'Maybe' + , tryAdd, trySub, tryMul + + -- *** Checked + , UnrepresentableSNumber(..) + , chkAdd, chkSub, chkMul + + -- ** Infallible + , divExact + + -- ** Reification to Constraints + , KnownSNumber(..), snumberVal + , reifySNumber, reifySNumberAsNat + + -- * Miscellaneous + , IntBits, IntMin, IntMaxP1 + , WordBits, WordMaxP1 + ) where + +import Control.Exception (Exception, throw) +import Data.Kind (Constraint, Type) +import Data.Maybe (fromMaybe) +import Data.Proxy (Proxy(..)) +import Data.Type.Equality ((:~:)(Refl)) +import GHC.Exts + ( Word(W#), addWordC#, subWordC#, timesWord2# + , Int(I#), addIntC#, subIntC#, mulIntMayOflo#, (*#) + ) +import GHC.Stack (HasCallStack, withFrozenCallStack) +import GHC.TypeNats (type (^), KnownNat, Nat, SomeNat(..), someNatVal) +import Numeric.Natural (Natural) +import Unsafe.Coerce (unsafeCoerce) + +import Data.SNumber.Internal + ( NegativeReprUnsignedErr, OutOfReprRangeErr + , IsAtLeastMinBound, IsLessThanMaxBound, ForbidNegZero + ) +import Kinds.Integer (CmpInteger, KnownInteger(..), pattern Pos, pattern Neg) +import qualified Kinds.Integer as K (Integer) +import Kinds.Num (type (+), type (-), type (*)) + +#include "MachDeps.h" + +-- | @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. +-- +-- 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@). +newtype SNumber a (n :: K.Integer) = MkSNumber# a + deriving newtype Show + +-- Note: we must be extremely careful to prevent GHC from solving +-- @Data.Coerce.Coercible (SNumber m) (SNumber n)@. Given two applications of +-- the same type constructor @X m@ and @X n@, there are three ways GHC might +-- solve this constraint: +-- * If the two types are equal (in our case, if @m ~ n@), the two types are +-- equal, and therefore GHC will consider the constraint solved. This is +-- obviously fine, and we don't need to prevent it from happening. +-- * If both types are newtypes, whose constructors are in scope, and the two +-- underlying types are coercible, GHC will consider the constraint solved. +-- In our case, the first and third conditions are unavoidably satisfied, so +-- we must prevent the newtype constructor from ever being in scope. We +-- achieve this (except for inside this module) by omitting it from the +-- export list. Instead, we export its behavior as the pattern synonym 'N#' +-- and the selector 'unSNumber'. +-- * If each pair of parameters with nominal role is equal, and each pair of +-- parameters with representational role is coercible (note: parameters with +-- phantom role are ignored), GHC will consider the constraint solved. In +-- our case, the only parameter involved is the 'Integer'; its inferred role +-- is phantom, which means all coercions over it would be solved; so we must +-- use a role annotation to change it. The choice between representational +-- and nominal doesn't matter in practice, because GHC will never solve +-- @Coercible {Integer} m n@ anyway. But we set it to nominal just because +-- that feels more right. + +-- The 'Type' parameter needs to have nominal role, because coercing between +-- types with different Eq/Ord instances is unsafe. +-- +-- See above on 'SNumber' for a description of the coercion behavior of the +-- 'Integer' parameter. +type role SNumber nominal nominal + +-- | 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 N# :: forall (n :: K.Integer) a. a -> SNumber a n +pattern N# {unSNumber} = MkSNumber# unSNumber +{-# COMPLETE N# #-} + +data KnownSNumberDict a n = KnownSNumber a n => KnownSNumberDict + +-- | Treat 'SNumber' as if it were a GADT containing a 'KnownSNumber' instance. +pattern SNumber + :: forall (n :: K.Integer) a. SNumberRepr a => KnownSNumber a n => SNumber a n +pattern SNumber <- + ((\x -> reifySNumber x (KnownSNumberDict @a @n)) -> KnownSNumberDict) + where + SNumber = snumberVal +{-# COMPLETE SNumber #-} + +class LitIsAnything (n :: K.Integer) +instance ForbidNegZero n => LitIsAnything n + +class LitIsUnsignedBits + (w :: Nat) + repr + (a :: K.Integer -> Type) + (n :: K.Integer) +instance ( IsAtLeastMinBound ('Pos 0) (NegativeReprUnsignedErr repr a) n + , IsLessThanMaxBound + ('Pos (2 ^ w)) + (OutOfReprRangeErr ('Pos 0) ('Pos (2 ^ w)) repr a) + n + , ForbidNegZero n + ) + => LitIsUnsignedBits w repr a n + +type SignedReprRangeErr w = + OutOfReprRangeErr ('Neg (2 ^ (w - 1))) ('Pos (2 ^ (w - 1))) + +class LitIsSignedBits (w :: Nat) repr (a :: K.Integer -> Type) (n :: K.Integer) +instance ( IsAtLeastMinBound + ('Neg (2 ^ (w - 1))) + (SignedReprRangeErr w repr a) + n + , IsLessThanMaxBound + ('Pos (2 ^ (w - 1))) + (SignedReprRangeErr w repr a) + n + , ForbidNegZero n + ) + => LitIsSignedBits w repr a n + +type LitIsNonNegative repr a = + IsAtLeastMinBound ('Pos 0) (NegativeReprUnsignedErr repr a) + +-- | The number of bits in the present system's 'Word' type. +type WordBits = WORD_SIZE_IN_BITS + +-- | One more than the largest representable 'Word' value. +type WordMaxP1 = 'Pos (2 ^ WordBits) + +-- | The number of bits in the present system's 'Int' type. +type IntBits = WORD_SIZE_IN_BITS + +-- | The smallest representable 'Int' value. +type IntMin = 'Neg (2 ^ (IntBits - 1)) + +-- | One more than the largest representable 'Int' value. +type IntMaxP1 = 'Pos (2 ^ (IntBits - 1)) + +-- | 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@. +class Integral a => SNumberRepr a where + -- | @SafeSNumber a n@ witnesses that @'N#' n@ is a valid @'SNumber' a n@. + type SafeSNumber a :: K.Integer -> Constraint + +instance SNumberRepr Int where + type SafeSNumber Int = LitIsSignedBits IntBits Int (SNumber Int) + +instance SNumberRepr Word where + type SafeSNumber Word = LitIsUnsignedBits WordBits Word (SNumber Word) + +instance SNumberRepr Integer where + type SafeSNumber Integer = LitIsAnything + +instance SNumberRepr Natural where + type SafeSNumber Natural = LitIsNonNegative Natural (SNumber Natural) + +-- | Construct an 'SNumber', doing all validation at the type level. +-- +-- This is completely safe and cannot raise runtime errors. +snumber + :: forall n a + . (SNumberRepr a, SafeSNumber a n, KnownInteger n) + => SNumber a n +snumber = unsafeMkSNumber (fromInteger (integerVal @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. +trySNumber + :: forall n a + . (SNumberRepr a, KnownInteger n) + => Maybe (SNumber a n) +trySNumber = unsafeTryMkSNumber (integerVal @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'. +unsafeUncheckedSNumber :: forall n a. (Num a, KnownInteger n) => SNumber a n +unsafeUncheckedSNumber = unsafeUncheckedMkSNumber (fromInteger (integerVal @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@. +unsafeMkSNumber :: forall n a. SafeSNumber a n => a -> SNumber a n +unsafeMkSNumber = 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. +unsafeTryMkSNumber + :: forall n a. SNumberRepr a => Integer -> Maybe (SNumber a n) +unsafeTryMkSNumber x = + let x' = fromIntegral x + in if toInteger x' /= x then Nothing else Just (N# x') +{-# INLINE unsafeTryMkSNumber #-} + +-- | Create an 'SNumber' for @n@, with no safety measures whatsoever. +unsafeUncheckedMkSNumber :: forall n a. a -> SNumber a n +unsafeUncheckedMkSNumber = N# + +-- | 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. +class KnownSNumber a n where + -- | Implementation of 'snumberVal'. + -- + -- This has an inconvenient type variable order because it derives from the + -- order they appear in the class head. + snumberVal_ :: SNumber a n + default snumberVal_ :: (SNumberRepr a, KnownInteger n) => SNumber a n + snumberVal_ = fromMaybe (error "KnownSNumber: unrepresentable") trySNumber + +-- TODO(awpr): GHC might helpfully simplify this to KnownInteger in inferred +-- type signatures, so we'll still end up passing Integers around and have +-- runtime type conversions? But we only infer signatures for bindings in +-- let/where clauses, so presumably GHC will solve a 'KnownSNumber' using +-- either a 'KnownSNumber' or 'KnownInteger' instance that's already available, +-- thus doing the best we could do in context? +instance (SNumberRepr a, KnownInteger n) => KnownSNumber 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. +snumberVal :: forall n a. KnownSNumber a n => SNumber a n +snumberVal = snumberVal_ + +-- TODO(awpr): Expose these functions as GEq/GOrd instances. + +-- | Ordering results carrying evidence of type-level ordering relations. +data SOrdering m n where + SLT :: CmpInteger m n ~ 'LT => SOrdering m n + -- | This doesn't currently prove m ~ n, but since we've forbidden SNumbers + -- of @'Neg 0@, it probably could. + SEQ :: CmpInteger m n ~ 'EQ => SOrdering m n + SGT :: CmpInteger m n ~ 'GT => SOrdering m n + +-- | Compare two type-level 'Integer's using their runtime witnesses. +compareSNumber + :: forall m n a. Ord a => SNumber a m -> SNumber a n -> SOrdering m n +compareSNumber (N# x) (N# y) = case compare x y of + LT -> case unsafeCoerce Refl :: CmpInteger m n :~: 'LT of Refl -> SLT + EQ -> case unsafeCoerce Refl :: CmpInteger m n :~: 'EQ of Refl -> SEQ + GT -> case unsafeCoerce Refl :: CmpInteger m n :~: 'GT of Refl -> SGT + +-- | Test equality of two type-level 'Integer's using their runtime witnesses. +sameSNumber :: Eq a => SNumber a m -> SNumber a n -> Maybe (m :~: n) +sameSNumber (N# x) (N# y) + | x == y = Just (unsafeCoerce Refl) + | otherwise = Nothing + +newtype c :=> a = CArr (c => a) + +-- | Stash an 'SNumber' at the type level as a 'KnownSNumber' instance. +reifySNumber :: forall a n r. SNumber a n -> (KnownSNumber a n => r) -> r +reifySNumber n r = f n + where + f :: SNumber a n -> r + f = unsafeCoerce (CArr r :: KnownSNumber a n :=> r) + +-- | Use a positive 'SNumber' to introduce a 'KnownNat' instance. +reifySNumberAsNat + :: forall n r a + . Integral a + => SNumber a ('Pos n) -> (KnownNat n => r) -> r +reifySNumberAsNat (N# x) r = case someNatVal (fromIntegral x) of + SomeNat (_ :: Proxy m) -> case unsafeCoerce Refl :: n :~: m of Refl -> r + +-- | An 'SNumber' with an existential 'K.Integer' type parameter. +data SomeSNumber a = forall n. SomeSNumber (SNumber a n) + +-- | 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 'K.Integer' type parameter. +someSNumberVal :: SNumberRepr a => a -> SomeSNumber a +someSNumberVal x = withSNumber x SomeSNumber + +-- | Like 'someSNumberVal', but in quantified CPS style rather than GADT style. +withSNumber :: SNumberRepr a => a -> (forall n. SNumber a n -> r) -> r +withSNumber x r = r (N# x) + +-- | 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. +class Integral a => OverflowArith a where + overflowAdd :: a -> a -> (Bool, a) + overflowSub :: a -> a -> (Bool, a) + overflowMul :: a -> a -> (Bool, a) + +instance OverflowArith Word where + overflowAdd (W# x) (W# y) = + case addWordC# x y of (# xy, ovf #) -> (I# ovf /= 0, W# xy) + overflowSub (W# x) (W# y) = + case subWordC# x y of (# xy, ovf #) -> (I# ovf /= 0, W# xy) + overflowMul (W# x) (W# y) = + case timesWord2# x y of (# hi, lo #) -> (W# hi /= 0, W# lo) + +instance OverflowArith Int where + overflowAdd (I# x) (I# y) = + case addIntC# x y of (# xy, ovf #) -> (I# ovf /= 0, I# xy) + overflowSub (I# x) (I# y) = + case subIntC# x y of (# xy, ovf #) -> (I# ovf /= 0, I# xy) + overflowMul (I# x) (I# y) = + -- TODO(awpr): Newer versions of base have 'timesInt2#'; consider using CPP + -- to use that when available. + let xy = I# (x *# y) + in case mulIntMayOflo# x y of + ovf -> if I# ovf /= 0 + then (toInteger xy /= toInteger (I# x) * toInteger (I# y), xy) + else (False, I# (x *# y)) + +instance OverflowArith Natural where + overflowAdd x y = (False, x + y) + overflowSub x y = (x > y, x - y) + overflowMul x y = (False, x * y) + +instance OverflowArith Integer where + overflowAdd x y = (False, x + y) + overflowSub x y = (False, x - y) + overflowMul x y = (False, x * y) + +-- Note: this internal helper function will make any SNumber result you want, +-- thus "unsafe". +unsafeMkTry + :: (a -> a -> (Bool, a)) -> SNumber a n -> SNumber a m -> Maybe (SNumber a o) +unsafeMkTry f (N# x) (N# y) = case f x y of + (True, _) -> Nothing + (False, xy) -> Just (N# xy) + +-- | Compute a runtime witness of @m + n@, or 'Nothing'. +tryAdd + :: (SNumberRepr a, OverflowArith a) + => SNumber a m -> SNumber a n -> Maybe (SNumber a (m + n)) +tryAdd = unsafeMkTry overflowAdd + +-- | 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)) +trySub = unsafeMkTry overflowSub + +-- | 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)) +tryMul = unsafeMkTry overflowMul + +data UnrepresentableSNumber = UnrepresentableSNumber String Integer Integer + deriving Show + +instance Exception UnrepresentableSNumber + +-- Note: this internal helper function will make any SNumber result you want, +-- thus "unsafe". +unsafeMkChk + :: (HasCallStack, Integral a) + => String + -> (a -> a -> (Bool, a)) -> SNumber a n -> SNumber a m -> SNumber a o +unsafeMkChk s f (N# x) (N# y) = case f x y of + (True, _) -> throw (UnrepresentableSNumber s (toInteger x) (toInteger y)) + (False, xy) -> N# xy + +-- | Compute a runtime witness of @m + n@, or throw. +chkAdd + :: (SNumberRepr a, OverflowArith a, HasCallStack) + => SNumber a m -> SNumber a n -> SNumber a (m + n) +chkAdd = withFrozenCallStack unsafeMkChk "+" overflowAdd + +-- | 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) +chkSub = withFrozenCallStack unsafeMkChk "-" overflowSub + +-- | 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) +chkMul = withFrozenCallStack unsafeMkChk "*" overflowMul + +-- | Compute a runtime witness of exact division. +-- +-- We could provide division in terms of 'GHC.TypeNats.Div' instead, but +-- "Kinds.Integer" doesn't currently have division. +divExact :: SNumberRepr a => SNumber a (m * n) -> SNumber a n -> SNumber a m +divExact = unsafeMkChk "/" (\x y -> (False, x `div` y)) diff --git a/src/Data/SNumber/Internal.hs b/src/Data/SNumber/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/SNumber/Internal.hs @@ -0,0 +1,114 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.SNumber.Internal + ( NegativeReprUnsignedErr + , IsAtLeastMinBound, IsLessThanMaxBound + , OutOfReprRangeErr, ForbidNegZero + ) where + +import Data.Kind (Constraint, Type) +import GHC.TypeLits (TypeError, ErrorMessage(..)) + +import Prelude hiding (Integer) -- No term-level stuff in this module anyway. +import Kinds.Integer (Integer(..)) +import Kinds.Num (type (-), type (=?), Cmp) + +type family ShowNum (n :: Integer) where + ShowNum ('Pos n) = 'ShowType n + ShowNum ('Neg n) = 'Text "-" ':<>: 'ShowType n + +type ShowTypedNum a n = ShowNum n ':<>: 'Text " :: " ':<>: 'ShowType a + +type ShowRange min maxp1 = + 'Text "(" ':<>: ShowNum min ':<>: 'Text ".." ':<>: + ShowNum (maxp1 - 'Pos 1) ':<>: 'Text ")" + +type NegativeReprUnsignedMsg repr a n = + 'Text "Negative SNumber with unsigned witness type:" ':$$: + 'Text " " ':<>: ShowTypedNum (a n) n + +class NegativeReprUnsignedErr repr (a :: Integer -> Type) (n :: Integer) +instance TypeError (NegativeReprUnsignedMsg repr a n) + => NegativeReprUnsignedErr repr a n + +type OutOfReprRangeMsg min maxp1 repr a n = + 'Text "SNumber overflows witness type:" ':$$: + 'Text " " ':<>: ShowTypedNum (a n) n ':$$: + 'Text "The representable range is " ':<>: ShowRange min maxp1 + +class OutOfReprRangeErr + (min :: Integer) + (maxp1 :: Integer) + repr + (a :: Integer -> Type) + (n :: Integer) +instance TypeError (OutOfReprRangeMsg min maxp1 repr a n) + => OutOfReprRangeErr min maxp1 repr a n + +type family Assert b msg :: Constraint where + Assert 'True c = () + Assert 'False c = c + +type family AssertLessThanMaxBound + u + (n :: Integer) + (maxp1 :: Integer) + (err :: Constraint) where + AssertLessThanMaxBound '() n maxp1 err = Assert (n Constraint) + (n :: Integer) +instance AssertLessThanMaxBound (Reduce (Cmp n maxp1)) n maxp1 (err n) + => IsLessThanMaxBound maxp1 err n + +-- | Assert that a numeric literal is greater than the (negative) min bound. +-- +-- This class name is semi-user-facing: it can appear in error messages when +-- trying to use literals of polymorphic or ambiguous types. +type family AssertAtLeastMinBound u (n :: Integer) (min :: Integer) err where + AssertAtLeastMinBound '() n min err = Assert (n >=? min) err + +class IsAtLeastMinBound + (min :: Integer) + (err :: Integer -> Constraint) + (n :: Integer) +instance AssertAtLeastMinBound (Reduce (Cmp n min)) n min (err n) + => IsAtLeastMinBound min err n + +type family ErrorIfNegZero n :: Constraint where + ErrorIfNegZero ('Neg 0) = TypeError ('Text "Illegal SNumber -0") + ErrorIfNegZero x = () + +class ForbidNegZero (n :: Integer) +instance ErrorIfNegZero n => ForbidNegZero n