numeric-kinds (empty) → 0.1.0.0
raw patch · 6 files changed
+590/−0 lines, 6 filesdep +base
Dependencies added: base
Files
- CHANGELOG.md +3/−0
- LICENSE +202/−0
- numeric-kinds.cabal +47/−0
- src/Kinds/Integer.hs +173/−0
- src/Kinds/Integer.hs-boot +24/−0
- src/Kinds/Num.hs +141/−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.
+ numeric-kinds.cabal view
@@ -0,0 +1,47 @@+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: 05ac8c3fea5a45f8da84a8ec3977066bf0902c70969070e7baab2643ef9c665b++name: numeric-kinds+version: 0.1.0.0+synopsis: Type-level numeric types, classes, and instances.+description: This provides numeric types meant for use at the type level with -XDataKinds,+ along with type families that act like type-level typeclasses providing+ various operations.+ .+ Currently, this primarily exists in support of+ <https://hackage.haskell.org/package/snumber snumber> and+ <https://hackage.haskell.org/package/dependent-literals-plugin dependent-literals-plugin>,+ and the only type-level numeric type in the current version is @Integer@.+category: Numeric+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: numeric-kinds++library+ exposed-modules:+ Kinds.Integer+ Kinds.Num+ other-modules:+ Paths_numeric_kinds+ hs-source-dirs:+ src+ build-depends:+ base >=4.12 && <4.16+ default-language: Haskell2010
+ src/Kinds/Integer.hs view
@@ -0,0 +1,173 @@+-- 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.++-- | Type-level 'Integer'.+--+-- Import Integer qualified as K and refer to it as K.Integer.+--+-- It turns out this is approximately identical to an in-progress GHC change+-- https://github.com/ghc-proposals/ghc-proposals/pull/154, right down to the+-- particulars of how to encode kind-classes. Apparently I was on the right+-- track! TODO(awpr): when that thing is merged and readily available, remove+-- this or turn it into a compat package.+--+-- Once that proposal is complete, we can migrate by replacing K.Integer with+-- just Integer.++{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Kinds.Integer+ ( -- * Type-level Integers+ Integer(..), ToInteger++ -- ** Runtime Values+ , KnownInteger(..)++ -- ** Specialized Arithmetic and Comparison+ , AddInteger, SubInteger, CmpInteger, MulInteger+ , type (-#)++ -- * Axioms+ , plusMinusInverseL, plusMinusInverseR+ , mulCommutes++ -- * Utility+ , CaseOrdering+ ) where++import Prelude hiding (Integer)+import qualified Prelude as P++import Data.Type.Equality ((:~:)(..))+import GHC.Exts (proxy#)+import GHC.TypeNats (KnownNat, Nat, natVal')+import Unsafe.Coerce (unsafeCoerce)++import Kinds.Num (type (+), type (-), type (*), Cmp, FromNat, ToInteger)++-- | Type-level signed numbers+data Integer = Pos Nat | Neg Nat++-- | Mostly internal; the "snumber" package provides more useful functionality.+class KnownInteger (n :: Integer) where+ integerVal :: P.Integer++instance KnownNat n => KnownInteger ('Pos n) where+ integerVal = toInteger $ natVal' @n proxy#++instance KnownNat n => KnownInteger ('Neg n) where+ integerVal =+ let x = natVal' @n proxy#+ in if x == 0+ then error "illegal KnownInteger (-0)"+ else negate $ toInteger x++type instance Cmp {- k=Integer -} x y = CmpInteger x y+type instance FromNat {- k=Integer -} n = 'Pos n++type instance ToInteger {- k=Integer -} n = n++type instance x + y = AddInteger x y++type instance x - y = SubInteger x y++type instance x * y = MulInteger x y++-- | Comparison of type-level integers.+type family CmpInteger m n where+ CmpInteger ('Pos m) ('Pos n) = Cmp m n+ CmpInteger ('Pos 0) ('Neg 0) = 'EQ+ CmpInteger ('Pos m) ('Neg n) = 'GT+ CmpInteger ('Neg 0) ('Pos 0) = 'EQ+ CmpInteger ('Neg m) ('Pos n) = 'LT+ CmpInteger ('Neg m) ('Neg n) = Cmp n m -- Note: reversed++-- | Type-level eliminator for 'Ordering'.+--+-- @CaseOrdering o lt eq gt@ selects from among @lt@, @eq@, and @gt@ according+-- to @o@. This is primarily exported so Haddock doesn't complain about being+-- unable to link it when it's mentioned in type instance clauses.+type family CaseOrdering (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) :: k where+ CaseOrdering 'LT lt eq gt = lt+ CaseOrdering 'EQ lt eq gt = eq+ CaseOrdering 'GT lt eq gt = gt++-- | Given two 'Nat's @m@ and @n@, computes @m - n@ as an 'Integer'.+type family (m :: Nat) -# (n :: Nat) where+ -- Redundant cases solely to make sure we get stuck reducing '-#' rather+ -- than reducing @CaseOrdering (Cmp m n) tons of junk@ when the magnitude is+ -- a type variable. This is similar to adding a bang pattern or case+ -- statement to a term-level function to make it strict in its arguments; but+ -- we don't have case statements or bang patterns in type families, so we add+ -- clauses instead.+ n -# 0 = 'Pos n -- Order matters: 0 -# 0 should be 'Pos 0+ 0 -# n = 'Neg n++ m -# n = CaseOrdering (Cmp m n)+ ('Neg (n - m))+ ('Pos 0)+ ('Pos (m - n))++-- | Addition of type-level integers.+type family AddInteger m n where+ AddInteger ('Pos m) ('Pos n) = 'Pos (m + n)+ AddInteger ('Pos m) ('Neg n) = m -# n+ AddInteger ('Neg m) ('Pos n) = n -# m+ AddInteger ('Neg m) ('Neg n) = 'Neg (m + n)++-- | Subtraction of type-level integers.+type family SubInteger m n where+ -- Note we could define this as @AddInteger m (Negate n)@, but then GHC would+ -- reduce eagerly to this when the parameters are type variables, and+ -- irreducible calls to 'SubInteger' would appear in error messages as+ -- @AddInteger m (Negate n)@ rather than the more readable @SubInteger m n@.+ -- So, we tolerate some duplicated code in order to make sure we get stuck on+ -- 'SubInteger' rather than later.+ SubInteger ('Pos m) ('Pos n) = m -# n+ SubInteger ('Pos m) ('Neg n) = 'Pos (m + n)+ SubInteger ('Neg m) ('Pos n) = 'Neg (m + n)+ SubInteger ('Neg m) ('Neg n) = n -# m++-- | Multiplication of type-level integers.+type family MulInteger m n where+ MulInteger ('Pos m) ('Pos n) = 'Pos (m * n)+ MulInteger ('Pos m) ('Neg n) = 0 -# (m * n)+ MulInteger ('Neg m) ('Pos n) = 0 -# (m * n)+ MulInteger ('Neg m) ('Neg n) = 'Pos (m * n)++unsafeAxiom :: a :~: b+unsafeAxiom = unsafeCoerce Refl++-- | Subtracting the right summand gives back the left summand.+plusMinusInverseR :: (m + n) -# n :~: 'Pos m+plusMinusInverseR = unsafeAxiom++-- | Subtracting the left summand gives back the right summand.+plusMinusInverseL :: (m + n) -# m :~: 'Pos n+plusMinusInverseL = unsafeAxiom++-- | Multiplication of integers is commutative.+mulCommutes :: MulInteger m n :~: MulInteger n m+mulCommutes = unsafeAxiom
+ src/Kinds/Integer.hs-boot view
@@ -0,0 +1,24 @@+-- 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.++module Kinds.Integer (Integer(..)) where++import Prelude hiding (Integer)++import GHC.TypeNats (Nat)++-- 'ToInteger' wants to live in "Kinds.Num", but "Kinds.Integer" wants to+-- depend on "Kinds.Num". Break the cycle by bootstrapping just the 'Integer'+-- type.+data Integer = Pos Nat | Neg Nat
+ src/Kinds/Num.hs view
@@ -0,0 +1,141 @@+-- 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.++-- | Type-level 'Ord' and 'Num'.+--+-- This provides "kindclasses" (actually open type families) with functionality+-- analogous to that provided by the typeclasses 'Ord' and 'Num'. Since+-- type-level typeclasses don't exist, instead we translate each would-be+-- method to its own open type family; then "instances" are implemented by+-- providing clauses for each type family "method". Unfortunately this means+-- we can't group methods into classes that must be implemented all-or-none,+-- but in practice this seems to be okay.++{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++module Kinds.Num+ ( -- * Comparisons+ Cmp+ , type (<?), type (<=?), type (==?), type (/=?), type (>=?), type (>?)++ -- ** Inequality Constraints+ , type (<), type (<=), type (==), type (/=), type (>=), type (>)++ -- * Conversions+ , FromNat, ToInteger++ -- * Arithmetic+ , type (+), type (-), type (*)++ -- * Utility+ , Proven, IsLT, IsLE, IsGT, IsGE, IsEQ, IsNE+ ) where++import Prelude hiding (Integer)++import GHC.TypeNats (CmpNat, Nat)+import qualified GHC.TypeNats as N (type (+), type (-), type (*))++import {-# source #-} Kinds.Integer (Integer(..))++-- | Type-level Ord "kindclass".+--+-- Note this has an invisible dependent @k@ parameter that makes the+-- textually-identical instances for different kinds actually different. Neat!+type family Cmp (x :: k) (y :: k) :: Ordering++-- That is, this is @Cmp {k=Nat} x y@, which is distinct from+-- @Cmp {k=Integer} x y@, even though both of them are written as @Cmp x y@.+type instance Cmp {- k=Nat -} x y = CmpNat x y++-- | Type-level numeric conversion from 'Nat'. Like 'fromInteger' in 'Num'.+type family FromNat (n :: Nat) :: k++type instance FromNat {- k=Nat -} n = n++-- | Type-level conversion to 'Integer'. Like 'toInteger' in 'Integral'.+type family ToInteger (n :: k) :: Integer++type instance ToInteger {- k=Nat -} n = 'Pos n++-- | Type-level addition "kindclass".+type family (x :: k) + (y :: k) :: k++type instance x + y = (N.+) x y -- HLint doesn't like qualified TypeOperators.++-- | Type-level subtraction "kindclass".+type family (x :: k) - (y :: k) :: k++type instance x - y = (N.-) x y++-- | Type-level multiplication "kindclass".+type family (x :: k) * (y :: k) :: k++type instance x * y = (N.*) x y++infix 4 <?, >?, <=?, >=?, ==?, /=?++type x <? y = IsLT (Cmp x y)+type x >? y = IsGT (Cmp x y)+type x <=? y = IsLE (Cmp x y)+type x >=? y = IsGE (Cmp x y)+type x ==? y = IsEQ (Cmp x y)+type x /=? y = IsNE (Cmp x y)++-- | Turns a type-level 'Bool' into a 'Data.Kind.Constraint' that it's 'True'.+type Proven b = b ~ 'True++infix 4 <, >, <=, >=, ==, /=++type x < y = Cmp x y ~ 'LT+type x > y = Cmp x y ~ 'GT+type x == y = Cmp x y ~ 'EQ+type x <= y = Proven (x <=? y)+type x >= y = Proven (x >=? y)+type x /= y = Proven (x /=? y)++-- | Test whether an 'Ordering' is 'LT'.+type family IsLT o where+ IsLT 'LT = 'True+ IsLT o = 'False++-- | Test whether an 'Ordering' is 'LT' or 'EQ'.+type family IsLE o where+ IsLE 'GT = 'False+ IsLE o = 'True++-- | Test whether an 'Ordering' is 'GT'.+type family IsGT o where+ IsGT 'GT = 'True+ IsGT o = 'False++-- | Test whether an 'Ordering' is 'GT' or 'EQ'.+type family IsGE o where+ IsGE 'LT = 'False+ IsGE o = 'True++-- | Test whether an 'Ordering' is 'EQ'.+type family IsEQ o where+ IsEQ 'EQ = 'True+ IsEQ o = 'False++-- | Test whether an 'Ordering' is 'LT' or 'GT'.+type family IsNE o where+ IsNE 'EQ = 'False+ IsNE o = 'True