snumber (empty) → 0.1.0.0
raw patch · 5 files changed
+918/−0 lines, 5 filesdep +basedep +numeric-kinds
Dependencies added: base, numeric-kinds
Files
- CHANGELOG.md +3/−0
- LICENSE +202/−0
- snumber.cabal +48/−0
- src/Data/SNumber.hs +551/−0
- src/Data/SNumber/Internal.hs +114/−0
+ CHANGELOG.md view
@@ -0,0 +1,3 @@+# 0.1.0.0++Initial version.
+ LICENSE view
@@ -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.
+ snumber.cabal view
@@ -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+ <https://hackage.haskell.org/package/dependent-literals-plugin dependent-literals-plugin>.+category: Constraints+homepage: https://github.com/google/hs-dependent-literals#readme+bug-reports: https://github.com/google/hs-dependent-literals/issues+author: Andrew Pritchard <awpr@google.com>+maintainer: Andrew Pritchard <awpr@google.com>+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
+ src/Data/SNumber.hs view
@@ -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))
+ src/Data/SNumber/Internal.hs view
@@ -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 (<?), 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 <? maxp1) err++type family Reduce (x :: k) :: ()+type instance Reduce 'LT = '()+type instance Reduce 'EQ = '()+type instance Reduce 'GT = '()+type instance Reduce 'True = '()+type instance Reduce 'False = '()++class IsLessThanMaxBound+ (maxp1 :: Integer)+ (err :: Integer -> 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