finitary 1.2.0.0 → 2.0.0.0
raw patch · 5 files changed
+462/−340 lines, 5 filesdep +hspecdep +hspec-hedgehogdep −coercible-utilsdep −finitarydep −monad-loopsdep ~basedep ~bitvecdep ~finite-typelitsPVP ok
version bump matches the API change (PVP)
Dependencies added: hspec, hspec-hedgehog
Dependencies removed: coercible-utils, finitary, monad-loops
Dependency ranges changed: base, bitvec, finite-typelits, ghc-typelits-knownnat, ghc-typelits-natnormalise, hedgehog, primitive, template-haskell, typelits-witnesses, vector, vector-sized
API changes (from Hackage documentation)
- Data.Finitary: instance forall k (a :: k). Data.Finitary.Finitary (Data.Proxy.Proxy a)
- Data.Finitary: instance forall k a (b :: k). Data.Finitary.Finitary a => Data.Finitary.Finitary (Data.Functor.Const.Const a b)
+ Data.Finitary: instance Data.Finitary.Finitary (Data.Proxy.Proxy a)
+ Data.Finitary: instance Data.Finitary.Finitary a => Data.Finitary.Finitary (Data.Functor.Const.Const a b)
- Data.Finitary: next :: (Finitary a, Alternative f) => a -> f a
+ Data.Finitary: next :: Finitary a => a -> Maybe a
- Data.Finitary: previous :: (Finitary a, Alternative f) => a -> f a
+ Data.Finitary: previous :: Finitary a => a -> Maybe a
Files
- CHANGELOG.md +9/−0
- README.md +15/−12
- finitary.cabal +75/−57
- src/Data/Finitary.hs +165/−124
- test/Main.hs +198/−147
CHANGELOG.md view
@@ -1,5 +1,14 @@ # Revision history for finitary +## 2.0.0.0 -- 2020-05-05++* Support GHC 8.10+* Remove support for GHCs older than 8.6+* Remove dependency on ``coercible-utils``+* ``previous`` and ``next`` now return ``Maybe``s+* Better tests+* Better documentation+ ## 1.2.0.0 -- 2019-10-17 * Remove ``nextSkipping`` and ``previousSkipping`` as unnecessary.
README.md view
@@ -42,7 +42,7 @@ somehow. While ``base`` and the Haskell Report certainly provide some limits on its behaviour, a lot of questions remain unanswered, including: -* What is the cardinality of this type?+* How many inhabitants does this type have? * What are the 'safe' values of ``Int`` I can feed to ``toEnum``? * For any ``x``, is ``toEnum . (+ 1) . fromEnum $ x`` safe (in that it'll give us a value instead of blowing up)?@@ -97,18 +97,19 @@ ``GHC.Generics``: ```haskell+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE TypeInType #-}--import GHC.Generics-import GHC.TypeNats-import Data.Word+{-# LANGUAGE DerivingStrategies #-} -import qualified Data.Vector.Sized as VS+import Data.Finitary (Finitary)+import Data.Vector.Sized (Vector)+import Data.Word (Word8)+import GHC.Generics (Generic) -data Foo = Bar | Baz (Word8, Word8) | Quux (VS.Vector 4 Bool)- deriving (Eq, Generic, Finitary) +data Foo = Bar | Baz (Word8, Word8) | Quux (Vector 4 Bool)+ deriving stock (Eq, Generic)+ deriving anyclass (Finitary) ``` Furthermore, GHC will even calculate the cardinality for you. To assist in this,@@ -134,9 +135,11 @@ ## What will this work on? -Currently, we have tested ``finitary`` (meaning 'run tests, not just compiled')-on GHCs 8.2.2, 8.4.4, 8.6.5 and 8.8.1. If you would like any additional versions -supported, please let us know.+Currently, we support the lates three versions of GHC. This, as current, is:++* 8.6.5+* 8.8.3+* 8.10.1 So far, the tests have all been on x86_64 GNU/Linux. If you have results on other platforms or architectures, please let us know too!
finitary.cabal view
@@ -1,63 +1,81 @@-cabal-version: 2.2-name: finitary--- PVP summary: +-+------- breaking API changes--- | | +----- non-breaking API additions--- | | | +--- code changes with no API change-version: 1.2.0.0-synopsis: A better, more type-safe Enum.-description: Provides a type class witnessing that a type has- finitely-many inhabitants, as well as its cardinality.- Also provides an auto-deriving framework using GHC- Generics, together with a range of instances for existing- types.-homepage: https://notabug.org/koz.ross/finitary-bug-reports: https://notabug.org/koz/ross/finitary/issues-license: GPL-3.0-or-later-license-file: LICENSE.md-author: Koz Ross-maintainer: koz.ross@retro-freedom.nz-copyright: (C) Koz Ross 2019-category: Data-build-type: Simple-tested-with: GHC == 8.8.1,- GHC == 8.6.5, - GHC == 8.4.4,- GHC == 8.2.2-extra-source-files: CHANGELOG.md,- README.md,- LICENSE.md+cabal-version: 2.2+name: finitary+version: 2.0.0.0+synopsis: A better, more type-safe Enum.+description:+ Provides a type class witnessing that a type has+ finitely-many inhabitants, as well as its cardinality.+ Also provides an auto-deriving framework using GHC+ Generics, together with a range of instances for existing+ types. +homepage: https://notabug.org/koz.ross/finitary+bug-reports: https://notabug.org/koz.ross/finitary/issues+license: GPL-3.0-or-later+license-file: LICENSE.md+author: Koz Ross+maintainer: koz.ross@retro-freedom.nz+copyright: (C) Koz Ross 2019-2020+category: Data+build-type: Simple+tested-with: GHC ==8.6.5 || ==8.8.3 || ==8.10.1+extra-source-files:+ CHANGELOG.md+ README.md+ LICENSE.md+ source-repository head- type: git- location: git://notabug.org/koz.ross/finitary.git+ type: git+ location: git://notabug.org/koz.ross/finitary.git library- exposed-modules: Data.Finitary- other-modules: Data.Finitary.TH- build-depends: base >= 4.10 && < 4.14,- finite-typelits >= 0.1.4.2 && < 0.2.0.0,- coercible-utils >= 0.0.0 && < 1.0.0,- ghc-typelits-knownnat >= 0.7 && < 0.8,- ghc-typelits-natnormalise >= 0.7 && < 0.8,- vector-sized >= 1.4.0.0 && < 1.5.0.0,- template-haskell >= 2.12.0.0 && < 2.16.0.0,- bitvec >= 1.0.0.1 && < 1.2.0.0,- primitive >= 0.6.4.0 && < 0.8.0.0,- vector >= 0.12.0.3 && < 0.13.0.0,- typelits-witnesses >= 0.4.0.0 && < 0.5.0.0- hs-source-dirs: src- default-language: Haskell2010+ exposed-modules: Data.Finitary+ other-modules: Data.Finitary.TH+ build-depends:+ , base >=4.12 && <5+ , bitvec ^>=1.0.3.0+ , finite-typelits ^>=0.1.4.2+ , ghc-typelits-knownnat ^>=0.7.2+ , ghc-typelits-natnormalise ^>=0.7.2+ , primitive ^>=0.7.0.1+ , template-haskell >=2.14.0.0 && <3.0.0.0+ , typelits-witnesses ^>=0.4.0.0+ , vector ^>=0.12.1.2+ , vector-sized ^>=1.4.1.0 + hs-source-dirs: src+ ghc-options:+ -Wall -Wcompat -Wincomplete-record-updates+ -Wincomplete-uni-patterns -Wredundant-constraints++ default-language: Haskell2010+ test-suite tests- type: exitcode-stdio-1.0- main-is: Main.hs- hs-source-dirs: test- ghc-options: -O2 -threaded -rtsopts -with-rtsopts=-N- build-depends: base,- hedgehog >= 1.0.1 && < 1.2,- finitary,- finite-typelits,- vector-sized,- monad-loops >= 0.4.3 && < 0.5.0,- bitvec- default-language: Haskell2010+ type: exitcode-stdio-1.0+ main-is: Main.hs+ other-modules:+ Data.Finitary+ Data.Finitary.TH++ build-depends:+ , base+ , bitvec+ , finite-typelits+ , ghc-typelits-knownnat+ , ghc-typelits-natnormalise+ , hedgehog ^>=1.0.2+ , hspec ^>=2.7.1+ , hspec-hedgehog ^>=0.0.1.2+ , primitive+ , template-haskell+ , typelits-witnesses+ , vector+ , vector-sized++ hs-source-dirs: test src+ ghc-options:+ -Wall -Wcompat -Wincomplete-record-updates+ -Wincomplete-uni-patterns -Wredundant-constraints -O2 -threaded+ -with-rtsopts=-N++ default-language: Haskell2010
src/Data/Finitary.hs view
@@ -1,5 +1,22 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstrainedClassMethods #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoStarIsType #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+ {-- - Copyright (C) 2019 Koz Ross <koz.ross@retro-freedom.nz>+ - Copyright (C) 2019-2020 Koz Ross <koz.ross@retro-freedom.nz> - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by@@ -15,31 +32,10 @@ - along with this program. If not, see <http://www.gnu.org/licenses/>. -} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}--{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE ConstrainedClassMethods #-}-{-# LANGUAGE TypeInType #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE CPP #-}--#if MIN_VERSION_base(4,12,0)-{-# LANGUAGE NoStarIsType #-}-#endif---- | +-- | -- Module: Data.Finitary -- Description: A type class witnessing that a type has finite cardinality.--- Copyright: (C) Koz Ross, 2019+-- Copyright: (C) Koz Ross, 2019-2020 -- License: GPL version 3.0 or later -- Maintainer: koz.ross@retro-freedom.nz -- Stability: Experimental@@ -47,7 +43,7 @@ -- -- This package provides the 'Finitary' type class, a range of useful -- \'base\' instances for commonly-used finitary types, and some helper--- functions for enumerating values of types with 'Finitary' instances. +-- functions for enumerating values of types with 'Finitary' instances. -- -- For your own types, there are three possible ways to define an instance of -- 'Finitary':@@ -59,12 +55,15 @@ -- -- > {-# LANGUAGE DeriveAnyClass #-} -- > {-# LANGUAGE DeriveGeneric #-}+-- > {-# LANGUAGE DerivingStrategies #-} -- >--- > import GHC.Generics--- > import Data.Word+-- > import Data.Finitary (Finitary)+-- > import Data.Word (Word8, Word16)+-- > import GHC.Generics (Generic) -- > -- > data Foo = Bar | Baz (Word8, Word8) | Quux Word16--- > deriving (Eq, Generic, Finitary)+-- > deriving stock (Eq, Generic)+-- > deriving anyclass (Finitary) -- -- This is the easiest method, and also the safest, as GHC will automatically -- determine the cardinality of @Foo@, as well as defining law-abiding methods.@@ -75,59 +74,79 @@ -- If you want a manually-defined instance, but don't wish to define every -- method, only 'fromFinite' and 'toFinite' are needed, along with -- 'Cardinality'. 'Cardinality' in particular must be defined with care, as--- otherwise, you may end up with inconstructable values or indexes that don't +-- otherwise, you may end up with inconstructable values or indexes that don't -- correspond to anything. -- -- __By defining everything__ -- -- For maximum control, you can define all the methods. Ensure you follow all -- the laws!----module Data.Finitary (- Finitary(..),- -- * Enumeration functions- inhabitants, inhabitantsFrom, inhabitantsTo, inhabitantsFromTo-) where+module Data.Finitary+ ( Finitary (..), -import Data.List.NonEmpty (NonEmpty(..))-import Data.Bifunctor (bimap, first)-import Numeric.Natural (Natural)-import Data.Semigroup (Max, Min, Sum, Product, Dual, Last, First, Any, All)-import Data.Functor.Identity (Identity)-import Data.Int (Int8, Int16, Int32, Int64)-import Data.Word (Word8, Word16, Word32, Word64)-import Data.Proxy (Proxy(..))-import Data.Void (Void)-import Data.Bool (bool)-import CoercibleUtils (op)-import GHC.Generics (Generic, Rep, U1(..), K1(..), V1, (:+:)(..), (:*:)(..), M1(..), from, to)-import Control.Applicative (Alternative(..), Const)-import Data.Kind (Type)-import GHC.TypeNats-import Data.Finite (Finite, finites, separateSum, separateProduct, combineProduct, weakenN, shiftN)-import Data.Ord (Down(..))-import Control.Monad.Primitive (PrimMonad(..))+ -- * Enumeration functions+ inhabitants,+ inhabitantsFrom,+ inhabitantsTo,+ inhabitantsFromTo,+ )+where++import Control.Applicative (Alternative (..), Const) import Control.Monad (forM_, join)-import GHC.TypeLits.Compare (isLE)-import Data.Type.Equality ((:~:)(..))+import Control.Monad.Primitive (PrimMonad (..)) import Control.Monad.ST (ST, runST)-import Foreign.Storable (Storable)--import qualified Data.List.NonEmpty as NE+import Data.Bifunctor (bimap, first) import qualified Data.Bit as B import qualified Data.Bit.ThreadSafe as BTS-import qualified Data.Vector.Sized as VS+import Data.Bool (bool)+import Data.Finitary.TH+import Data.Finite+ ( Finite,+ combineProduct,+ finites,+ separateProduct,+ separateSum,+ shiftN,+ weakenN,+ )+import Data.Functor.Identity (Identity)+import Data.Int (Int16, Int32, Int64, Int8)+import Data.Kind (Type)+import Data.List.NonEmpty (NonEmpty (..))+import qualified Data.List.NonEmpty as NE+import Data.Ord (Down (..))+import Data.Proxy (Proxy (..))+import Data.Semigroup (All, Any, Dual, First, Last, Max, Min, Product, Sum)+import Data.Type.Equality ((:~:) (..)) import qualified Data.Vector.Generic as VG-import qualified Data.Vector.Mutable.Sized as VMS-import qualified Data.Vector.Generic.Sized as VGS import qualified Data.Vector.Generic.Mutable as VGM import qualified Data.Vector.Generic.Mutable.Sized as VGMS-import qualified Data.Vector.Unboxed.Sized as VUS-import qualified Data.Vector.Unboxed.Mutable.Sized as VUMS-import qualified Data.Vector.Storable.Sized as VSS+import qualified Data.Vector.Generic.Sized as VGS+import qualified Data.Vector.Mutable.Sized as VMS+import qualified Data.Vector.Sized as VS import qualified Data.Vector.Storable.Mutable.Sized as VSMS--import Data.Finitary.TH+import qualified Data.Vector.Storable.Sized as VSS+import qualified Data.Vector.Unboxed.Mutable.Sized as VUMS+import qualified Data.Vector.Unboxed.Sized as VUS+import Data.Void (Void)+import Data.Word (Word16, Word32, Word64, Word8)+import Foreign.Storable (Storable)+import GHC.Generics+ ( (:*:) (..),+ (:+:) (..),+ Generic,+ K1 (..),+ M1 (..),+ Rep,+ U1 (..),+ V1,+ from,+ to,+ )+import GHC.TypeLits.Compare (isLE)+import GHC.TypeNats+import Numeric.Natural (Natural) -- | Witnesses an isomorphism between @a@ and some @(KnownNat n) => Finite n@. -- Effectively, a lawful instance of this shows that @a@ has exactly @n@@@ -160,64 +179,71 @@ -- -- Lastly, if you define any of the other methods, these laws must hold: ----- * \[ a \neq \emptyset \rightarrow \texttt{start} = \texttt{fromFinite} \; \texttt{minBound} \]--- * \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; \texttt{maxBound} \]--- * \[ \forall x :: a \; \texttt{end} \neq x \rightarrow \texttt{next} \; x =+-- * \[ a \neq \emptyset \rightarrow \texttt{start} :: a = \texttt{fromFinite} \; \texttt{minBound} \]+-- * \[ a \neq \emptyset \rightarrow \texttt{end} :: a = \texttt{fromFinite} \; \texttt{maxBound} \]+-- * \[ \forall x :: a \; \texttt{end} :: a \neq x \rightarrow \texttt{next} \; x = -- (\texttt{fromFinite} \circ + 1 \circ \texttt{toFinite}) \; x \]--- * \[ \forall x :: a \; \texttt{start} \neq x \rightarrow \texttt{previous} \; x =+-- * \[ \forall x :: a \; \texttt{start} :: a \neq x \rightarrow \texttt{previous} \; x = -- (\texttt{fromFinite} \circ - 1 \circ \texttt{toFinite}) \; x \]--- +-- -- Together with the fact that @Finite n@ is well-ordered whenever @KnownNat n@ -- holds, a law-abiding @Finitary@ instance for a type @a@ defines a constructive -- [well-order](https://en.wikipedia.org/wiki/Well-order), witnessed by -- 'toFinite' and 'fromFinite', which agrees with the @Ord@ instance for @a@, if -- any.--- +-- -- We /strongly/ suggest that @fromFinite@ and @toFinite@ should have--- time complexity \(\Theta(1)\), or, if that's not possible, \(O(\texttt{Cardinality} \; a)\). +-- time complexity \(\Theta(1)\), or, if that's not possible, \(O(\texttt{Cardinality} \; a)\). -- The latter is the case for instances generated using -- @Generics@-based derivation, but not for \'basic\' types; thus, these -- functions for your derived types will only be as slow as their \'structure\', -- rather than their \'contents\', provided the contents are of these \'basic\'--- types. +-- types. class (Eq a, KnownNat (Cardinality a)) => Finitary (a :: Type) where- -- | How many (non-@_|_@) inhabitants @a@ has, as a typelevel natural number. + -- | How many (non-@_|_@) inhabitants @a@ has, as a typelevel natural number. type Cardinality a :: Nat+ type Cardinality a = GCardinality (Rep a)+ -- | Converts an index into its corresponding inhabitant. fromFinite :: Finite (Cardinality a) -> a default fromFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => Finite (Cardinality a) -> a fromFinite = to . gFromFinite+ -- | Converts an inhabitant to its corresponding index. toFinite :: a -> Finite (Cardinality a) default toFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => a -> Finite (Cardinality a) toFinite = gToFinite . from+ -- | The first inhabitant, by index, assuming @a@ has any inhabitants. start :: (1 <= Cardinality a) => a start = fromFinite minBound+ -- | The last inhabitant, by index, assuming @a@ has any inhabitants. end :: (1 <= Cardinality a) => a end = fromFinite maxBound+ -- | @previous x@ gives the inhabitant whose index precedes the index of @x@, -- or 'empty' if no such index exists.- previous :: (Alternative f) => a -> f a+ previous :: a -> Maybe a previous = fmap fromFinite . guarded (/= maxBound) . dec . toFinite+ -- | @next x@ gives the inhabitant whose index follows the index of @x@, or -- 'empty' if no such index exists.- next :: (Alternative f) => a -> f a+ next :: a -> Maybe a next = fmap fromFinite . guarded (/= minBound) . inc . toFinite class (KnownNat (GCardinality a)) => GFinitary (a :: Type -> Type) where type GCardinality a :: Nat gFromFinite :: Finite (GCardinality a) -> a x- gToFinite :: a x -> Finite (GCardinality a) + gToFinite :: a x -> Finite (GCardinality a) instance GFinitary V1 where type GCardinality V1 = 0 {-# INLINE gFromFinite #-} gFromFinite = const undefined {-# INLINE gToFinite #-}- gToFinite = const undefined + gToFinite = const undefined instance GFinitary U1 where type GCardinality U1 = 1@@ -231,7 +257,7 @@ {-# INLINE gFromFinite #-} gFromFinite = K1 . fromFinite {-# INLINE gToFinite #-}- gToFinite = toFinite . op K1+ gToFinite = toFinite . unK1 instance (GFinitary a, GFinitary b) => GFinitary (a :+: b) where type GCardinality (a :+: b) = GCardinality a + GCardinality b@@ -239,13 +265,14 @@ gFromFinite = either (L1 . gFromFinite) (R1 . gFromFinite) . separateSum {-# INLINE gToFinite #-} gToFinite (L1 x) = weakenN . gToFinite $ x- gToFinite (R1 x) = shiftN . gToFinite $ x + gToFinite (R1 x) = shiftN . gToFinite $ x instance (GFinitary a, GFinitary b) => GFinitary (a :*: b) where type GCardinality (a :*: b) = GCardinality a * GCardinality b {-# INLINE gFromFinite #-}- gFromFinite i = let (x, y) = separateProduct' i in- gFromFinite x :*: gFromFinite y+ gFromFinite i =+ let (x, y) = separateProduct' i+ in gFromFinite x :*: gFromFinite y {-# INLINE gToFinite #-} gToFinite (x :*: y) = combineProduct' @(GCardinality a) @(GCardinality b) (weakenN . gToFinite $ x, weakenN . gToFinite $ y) @@ -254,7 +281,7 @@ {-# INLINE gFromFinite #-} gFromFinite = M1 . gFromFinite {-# INLINE gToFinite #-}- gToFinite = gToFinite . op M1+ gToFinite = gToFinite . unM1 -- * Instances -- Basic types@@ -276,7 +303,7 @@ {-# INLINE fromFinite #-} fromFinite = B.Bit . toEnum . fromEnum {-# INLINE toFinite #-}- toFinite = toEnum . fromEnum . op B.Bit+ toFinite = toEnum . fromEnum . B.unBit {-# INLINE start #-} start = minBound {-# INLINE end #-}@@ -291,7 +318,7 @@ {-# INLINE fromFinite #-} fromFinite = BTS.Bit . toEnum . fromEnum {-# INLINE toFinite #-}- toFinite = toEnum . fromEnum . op BTS.Bit+ toFinite = toEnum . fromEnum . BTS.unBit {-# INLINE start #-} start = minBound {-# INLINE end #-}@@ -381,7 +408,7 @@ instance Finitary Int8 where type Cardinality Int8 = $(cardinalityOf @Int8)- {-# INLINE fromFinite #-} + {-# INLINE fromFinite #-} fromFinite = fromIntegral . subtract 128 . fromIntegral @_ @Int16 {-# INLINE toFinite #-} toFinite = fromIntegral . (+ 128) . fromIntegral @_ @Int16@@ -396,7 +423,7 @@ instance Finitary Int16 where type Cardinality Int16 = $(cardinalityOf @Int16)- {-# INLINE fromFinite #-} + {-# INLINE fromFinite #-} fromFinite = fromIntegral . subtract 32768 . fromIntegral @_ @Int32 {-# INLINE toFinite #-} toFinite = fromIntegral . (+ 32768) . fromIntegral @_ @Int32@@ -537,12 +564,9 @@ instance (Finitary a) => Finitary (Down a) where type Cardinality (Down a) = Cardinality a {-# INLINE fromFinite #-}- fromFinite = Down . fromFinite . opp- where opp = fromIntegral @_ @(Finite (Cardinality a)) . (`mod` n) . (* (n - 1)) . (+ 1) . fromIntegral @_ @Natural - n = natVal @(Cardinality a) Proxy+ fromFinite = Down . fromFinite . opp @a {-# INLINE toFinite #-}- toFinite = fromIntegral @_ @(Finite (Cardinality a)) . (`mod` n) . (* (n - 1)) . (+ 1) . fromIntegral @_ @Natural . toFinite . op Down- where n = natVal @(Cardinality a) Proxy + toFinite (Down x) = opp @a . toFinite $ x -- | A fixed-length vector over a type @a@ with an instance of @Finitary@ can be -- thought of as a fixed-length word over an alphabet of size @Cardinality a@.@@ -554,10 +578,12 @@ type Cardinality (VS.Vector n a) = Cardinality a ^ n {-# INLINE fromFinite #-} fromFinite i = runST (go i)- where go :: Finite (Cardinality (VS.Vector n a)) -> ST s (VS.Vector n a)- go ix = do v <- VMS.new- unroll v ix- VS.unsafeFreeze v+ where+ go :: Finite (Cardinality (VS.Vector n a)) -> ST s (VS.Vector n a)+ go ix = do+ v <- VMS.new+ unroll v ix+ VS.unsafeFreeze v {-# INLINE toFinite #-} toFinite = roll @@ -565,10 +591,12 @@ type Cardinality (VUS.Vector n a) = Cardinality a ^ n {-# INLINE fromFinite #-} fromFinite i = runST (go i)- where go :: Finite (Cardinality (VUS.Vector n a)) -> ST s (VUS.Vector n a)- go ix = do v <- VUMS.new- unroll v ix- VUS.unsafeFreeze v+ where+ go :: Finite (Cardinality (VUS.Vector n a)) -> ST s (VUS.Vector n a)+ go ix = do+ v <- VUMS.new+ unroll v ix+ VUS.unsafeFreeze v {-# INLINE toFinite #-} toFinite = roll @@ -576,10 +604,12 @@ type Cardinality (VSS.Vector n a) = Cardinality a ^ n {-# INLINE fromFinite #-} fromFinite i = runST (go i)- where go :: Finite (Cardinality (VSS.Vector n a)) -> ST s (VSS.Vector n a)- go ix = do v <- VSMS.new- unroll v ix- VSS.unsafeFreeze v+ where+ go :: Finite (Cardinality (VSS.Vector n a)) -> ST s (VSS.Vector n a)+ go ix = do+ v <- VSMS.new+ unroll v ix+ VSS.unsafeFreeze v {-# INLINE toFinite #-} toFinite = roll @@ -588,53 +618,58 @@ -- | Produce every inhabitant of @a@, in ascending order of indexes. -- If you want descending order, use @Down a@ instead. {-# INLINE inhabitants #-}-inhabitants :: forall (a :: Type) . (Finitary a) => [a]+inhabitants :: forall (a :: Type). (Finitary a) => [a] inhabitants = fromFinite <$> finites -- | Produce every inhabitant of @a@, starting with the argument, in ascending -- order of indexes. -- If you want descending order, use @Down a@ instead. {-# INLINE inhabitantsFrom #-}-inhabitantsFrom :: forall (a :: Type) . (Finitary a) => a -> NonEmpty a-inhabitantsFrom x = x :| concatMap @Maybe (fmap fromFinite . enumFrom . toFinite) (next x) +inhabitantsFrom :: forall (a :: Type). (Finitary a) => a -> NonEmpty a+inhabitantsFrom x = x :| concatMap @Maybe (fmap fromFinite . enumFrom . toFinite) (next x) -- | Produce every inhabitant of @a@, up to and including the argument, in -- ascending order of indexes. -- If you want descending order, use @Down a@ instead. {-# INLINE inhabitantsTo #-}-inhabitantsTo :: forall (a :: Type) . (Finitary a) => a -> NonEmpty a-inhabitantsTo x = NE.fromList (fromFinite <$> [0 .. toFinite x]) +inhabitantsTo :: forall (a :: Type). (Finitary a) => a -> NonEmpty a+inhabitantsTo x = NE.fromList (fromFinite <$> [0 .. toFinite x]) -- | Produce every inhabitant of @a@, starting with the first argument, up to -- the second argument, in ascending order of indexes. @inhabitantsFromTo x y@ -- will produce the empty list if @toFinite x > toFinite y@. -- If you want descending order, use @Down a@ instead. {-# INLINE inhabitantsFromTo #-}-inhabitantsFromTo :: forall (a :: Type) . (Finitary a) => a -> a -> [a]+inhabitantsFromTo :: forall (a :: Type). (Finitary a) => a -> a -> [a] inhabitantsFromTo lo hi = fromFinite <$> [toFinite lo .. toFinite hi] -- Helpers {-# INLINE combineProduct' #-}-combineProduct' :: forall n m . (KnownNat n, KnownNat m) => (Finite n, Finite m) -> Finite (n * m)+combineProduct' :: forall n m. (KnownNat n, KnownNat m) => (Finite n, Finite m) -> Finite (n * m) combineProduct' = fromIntegral . uncurry (+) . first ((natVal $ Proxy @m) *) . bimap @_ @_ @Natural @_ @Natural fromIntegral fromIntegral {-# INLINE separateProduct' #-}-separateProduct' :: forall n m . (KnownNat n, KnownNat m) => Finite (n * m) -> (Finite n, Finite m)+separateProduct' :: forall n m. (KnownNat n, KnownNat m) => Finite (n * m) -> (Finite n, Finite m) separateProduct' = bimap (fromIntegral . (\x -> fromIntegral x `div` natVal @m Proxy)) (fromIntegral . (\x -> fromIntegral x `mod` natVal @m Proxy)) . join (,) -unroll :: forall a m v n . (Finitary a, PrimMonad m, KnownNat n, VGM.MVector v a) => VGMS.MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()-unroll v acc = forM_ @_ @_ @_ @() (isLE (Proxy @1) (Proxy @n)) - (\Refl -> do let (d, r) = separateProduct @(Cardinality a ^ (n -1)) @(Cardinality a) acc- let x = fromFinite r- VGMS.write v 0 x- unroll (VGMS.tail v) d)+unroll :: forall a m v n. (Finitary a, PrimMonad m, KnownNat n, VGM.MVector v a) => VGMS.MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()+unroll v acc =+ forM_ @_ @_ @_ @()+ (isLE (Proxy @1) (Proxy @n))+ ( \Refl -> do+ let (d, r) = separateProduct @(Cardinality a ^ (n -1)) @(Cardinality a) acc+ let x = fromFinite r+ VGMS.write v 0 x+ unroll (VGMS.tail v) d+ ) -roll :: forall a v n . (Finitary a, VG.Vector v a, KnownNat n) => VGS.Vector v n a -> Finite (Cardinality a ^ n)+roll :: forall a v n. (Finitary a, VG.Vector v a, KnownNat n) => VGS.Vector v n a -> Finite (Cardinality a ^ n) roll v = case isLE (Proxy @1) (Proxy @n) of- Nothing -> 0- Just Refl -> let (h, t) = (VGS.head v, VGS.tail v) in- combineProduct (roll t, toFinite h) + Nothing -> 0+ Just Refl ->+ let (h, t) = (VGS.head v, VGS.tail v)+ in combineProduct (roll t, toFinite h) {-# INLINE inc #-} inc :: (Num a) => a -> a@@ -645,5 +680,11 @@ dec = subtract 1 {-# INLINE guarded #-}-guarded :: forall (a :: Type) (f :: Type -> Type) . (Alternative f) => (a -> Bool) -> a -> f a+guarded :: forall (a :: Type) (f :: Type -> Type). (Alternative f) => (a -> Bool) -> a -> f a guarded p x = bool empty (pure x) (p x)++{-# INLINE opp #-}+opp :: forall a. (KnownNat (Cardinality a)) => Finite (Cardinality a) -> Finite (Cardinality a)+opp = fromIntegral @_ @(Finite (Cardinality a)) . (`mod` n) . (* (n - 1)) . inc . fromIntegral @_ @Natural+ where+ n = natVal @(Cardinality a) Proxy
test/Main.hs view
@@ -1,3 +1,10 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+ {- - Copyright (C) 2019 Koz Ross <koz.ross@retro-freedom.nz> -@@ -15,165 +22,209 @@ - along with this program. If not, see <http://www.gnu.org/licenses/>. -} -{-# LANGUAGE DeriveAnyClass #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE TypeInType #-}-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE RankNTypes #-}- module Main where -import Data.List (sort, sortOn)-import Data.Ord (Down)-import Data.Maybe (isNothing, isJust)-import Data.Int (Int8, Int16, Int32, Int64)-import Data.Word (Word8, Word16, Word32, Word64)-import GHC.TypeNats-import GHC.Generics-import Data.Kind (Type)-import Data.Finite (Finite, finites)-import Data.Proxy (Proxy(..))-import Control.Monad.Loops (andM)-import Data.Typeable (Typeable, typeRep)-import Data.String (fromString)-import Hedgehog--import qualified Hedgehog.Gen as G-import qualified Hedgehog.Range as R-import qualified Data.Vector.Sized as VS-import qualified Data.Vector.Unboxed.Sized as VUS-import qualified Data.Vector.Storable.Sized as VSS-import qualified Data.Bit as B-import qualified Data.Bit.ThreadSafe as BTS--import Data.Finitary---- A representation of types-data SomeFinitaryRep where- SomeFinitaryRep :: forall (a :: Type) . (Finitary a, Ord a, Show a, Typeable a, 1 <= (Cardinality a)) => Proxy a -> SomeFinitaryRep---- A representation of test functions-data SomeTestFunction where- SomeTestFunction :: (forall (a :: Type) . (Finitary a, Ord a, Show a, 1 <= (Cardinality a)) => Proxy a -> Property) -> SomeTestFunction---- Some weird generic-data Foo = Bar | Baz (VS.Vector 4 Bool) | Quux Word8- deriving (Eq, Show, Typeable, Generic, Finitary, Ord)---- Something I will need for further tests-iterateMN :: forall (m :: Type -> Type) (a :: Type) (b :: Type) . (Eq a, Bounded a, Enum a, Monad m) => a -> (b -> m b) -> b -> m b-iterateMN i f x = if i == minBound- then f x- else iterateMN (pred i) f x >>= f---- How much testing do I want to do for random inputs?-testLimit :: forall (a :: Type) (b :: Type) . (Finitary a, Num b) => b-testLimit = fromIntegral . (* 2) . min 32767 . natVal $ Proxy @(Cardinality a) ---- Generators-choose :: forall (a :: Type) m . (MonadGen m, Finitary a) => m a-choose = fromFinite <$> chooseFinite--chooseFinite :: forall (n :: Nat) m . (KnownNat n, MonadGen m) => m (Finite n)-chooseFinite = fromIntegral <$> G.integral (R.linear 0 limit)- where limit = subtract @Integer 1 . fromIntegral . natVal @n $ Proxy---- Data-allTheTypes :: [SomeFinitaryRep]-allTheTypes = [- SomeFinitaryRep @(Proxy Int) Proxy,- SomeFinitaryRep @Bool Proxy,- SomeFinitaryRep @B.Bit Proxy,- SomeFinitaryRep @BTS.Bit Proxy,- SomeFinitaryRep @Ordering Proxy,- SomeFinitaryRep @Char Proxy,- SomeFinitaryRep @Word8 Proxy,- SomeFinitaryRep @Word16 Proxy,- SomeFinitaryRep @Word32 Proxy,- SomeFinitaryRep @Word64 Proxy,- SomeFinitaryRep @Int16 Proxy,- SomeFinitaryRep @Int8 Proxy,- SomeFinitaryRep @Int32 Proxy,- SomeFinitaryRep @Int64 Proxy,- SomeFinitaryRep @Int Proxy,- SomeFinitaryRep @Word Proxy,- SomeFinitaryRep @(Down Int) Proxy,- SomeFinitaryRep @(Maybe Word8) Proxy,- SomeFinitaryRep @(Either Word8 Int8) Proxy,- SomeFinitaryRep @(Word8, Int8) Proxy,- SomeFinitaryRep @(VS.Vector 4 Bool) Proxy,- SomeFinitaryRep @(VUS.Vector 4 Bool) Proxy,- SomeFinitaryRep @(VSS.Vector 4 Bool) Proxy- ]+import Data.Finitary (Finitary (..))+import Data.Int (Int16, Int32, Int8)+import Data.Ord (Down (..))+import qualified Data.Vector.Sized as V+import qualified Data.Vector.Storable.Sized as VS+import Data.Vector.Unboxed.Sized (Unbox)+import qualified Data.Vector.Unboxed.Sized as VU+import Data.Word (Word16, Word32, Word8)+import Foreign.Storable (Storable)+import GHC.Generics (Generic)+import Hedgehog ((===), Gen, PropertyT, forAll)+import qualified Hedgehog.Gen as Gen+import Hedgehog.Range (constantBounded)+import Test.Hspec (SpecWith, describe, hspec, it, parallel)+import Test.Hspec.Hedgehog (hedgehog, modifyMaxSize) -constructTest :: SomeTestFunction -> GroupName -> IO Bool-constructTest (SomeTestFunction testFunc) name = checkParallel . Group name $ fmap go allTheTypes- where go (SomeFinitaryRep p) = (fromString . show . typeRep $ p, testFunc p)+main :: IO ()+main = hspec . parallel $ do+ describe "Bijectivity and order preservation" $ do+ checkBijection "Char" Gen.unicode+ checkBijection "Word8" (Gen.enumBounded @_ @Word8)+ modifyMaxSize (const 10000)+ . checkBijection "Word16"+ $ Gen.enumBounded @_ @Word16+ modifyMaxSize (const 10000)+ . checkBijection "Word32"+ $ Gen.enumBounded @_ @Word32+ modifyMaxSize (const 10000)+ . checkBijection "Word64"+ $ Gen.word64 constantBounded+ checkBijection "Int8" (Gen.enumBounded @_ @Int8)+ modifyMaxSize (const 10000)+ . checkBijection "Int16"+ $ Gen.enumBounded @_ @Int16+ modifyMaxSize (const 10000)+ . checkBijection "Int32"+ $ Gen.enumBounded @_ @Int32+ modifyMaxSize (const 10000)+ . checkBijection "Int64"+ $ Gen.int64 constantBounded+ modifyMaxSize (const 10000)+ . checkBijection "Int"+ $ Gen.int constantBounded+ modifyMaxSize (const 10000)+ . checkBijection "Word"+ $ Gen.word constantBounded+ describe "Down" $ do+ checkMonotonic "Bool" Gen.bool+ modifyMaxSize (const 10000)+ . checkMonotonic "Int"+ $ (Gen.enumBounded @_ @Int)+ modifyMaxSize (const 10000)+ . checkMonotonic "(Either Int Bool)"+ $ Gen.choice+ [ Left <$> Gen.enumBounded @_ @Int,+ Right <$> Gen.enumBounded @_ @Bool+ ]+ modifyMaxSize (const 10000)+ . checkMonotonic "(Int, Bool)"+ $ ( (,)+ <$> Gen.enumBounded @_ @Int+ <*> Gen.enumBounded @_ @Bool+ )+ modifyMaxSize (const 10000)+ . checkMonotonic "of a user-defined type"+ $ genFoo+ describe "Fixed-length vectors" $ do+ modifyMaxSize (const 10000)+ . checkStorable "Int8"+ . genStorable+ $ Gen.enumBounded @_ @Int8+ modifyMaxSize (const 10000)+ . checkUnboxed "Int8"+ . genUnboxed+ $ Gen.enumBounded @_ @Int8+ modifyMaxSize (const 10000)+ . checkRegular "Int8"+ . genRegular+ $ Gen.enumBounded @_ @Int8+ modifyMaxSize (const 10000)+ . checkUnboxed "(Int8, Int8)"+ . genUnboxed+ $ ( (,) <$> Gen.enumBounded @_ @Int8+ <*> Gen.enumBounded @_ @Int8+ )+ modifyMaxSize (const 10000)+ . checkRegular "(Int8, Int8)"+ . genRegular+ $ ( (,) <$> Gen.enumBounded @_ @Int8+ <*> Gen.enumBounded @_ @Int8+ )+ modifyMaxSize (const 10000)+ . checkRegular "Either Int8 Bool"+ . genRegular+ . Gen.choice+ $ [ Left <$> Gen.enumBounded @_ @Int8,+ Right <$> Gen.bool+ ]+ modifyMaxSize (const 10000)+ . checkRegular "a user defined type"+ . genRegular+ $ genFoo --- Properties-isBijection :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property-isBijection _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a- x === (fromFinite . toFinite $ x))+-- Helpers -isOrderPreserving :: forall (a :: Type) . (Finitary a, Ord a) => Proxy a -> Property-isOrderPreserving _ = withTests (testLimit @a) (property $ do i <- forAll $ chooseFinite @(Cardinality a)- j <- forAll $ chooseFinite @(Cardinality a)- assert (fromFinite @a i > fromFinite @a j || i <= j)) +data Foo+ = Bar+ | Baz Int8+ | Quux (Int8, Int8)+ deriving stock (Eq, Ord, Generic, Show)+ deriving anyclass (Finitary) -startIsCorrect :: forall (a :: Type) . (Finitary a, Show a, 1 <= (Cardinality a)) => Proxy a -> Property-startIsCorrect _ = property $ start @a === fromFinite minBound+checkStorable ::+ forall a.+ (Storable a, Finitary a, Show a, Ord a) =>+ String ->+ Gen (VS.Vector 10 a) ->+ SpecWith ()+checkStorable name =+ it ("should biject a Storable Vector of " <> name)+ . hedgehog+ . bicheck @(VS.Vector 10 a) -previousStartNothing :: forall (a :: Type) . (Finitary a, 1 <= (Cardinality a)) => Proxy a -> Property-previousStartNothing _ = property $ assert (isNothing . previous $ start @a)+checkRegular ::+ forall a.+ (Finitary a, Show a, Ord a) =>+ String ->+ Gen (V.Vector 10 a) ->+ SpecWith ()+checkRegular name =+ it ("should biject a Vector of " <> name)+ . hedgehog+ . bicheck @(V.Vector 10 a) -endNextNothing :: forall (a :: Type) . (Finitary a, 1 <= (Cardinality a)) => Proxy a -> Property-endNextNothing _ = property $ assert (isNothing . next $ end @a)+checkUnboxed ::+ forall a.+ (Unbox a, Finitary a, Show a, Ord a) =>+ String ->+ Gen (VU.Vector 10 a) ->+ SpecWith ()+checkUnboxed name =+ it ("should biject an Unboxed Vector of " <> name)+ . hedgehog+ . bicheck @(VU.Vector 10 a) -endIsCorrect :: forall (a :: Type) . (Finitary a, Show a, 1 <= (Cardinality a)) => Proxy a -> Property-endIsCorrect _ = property $ end @a === fromFinite maxBound+bicheck :: forall a. (Show a, Finitary a, Ord a) => Gen a -> PropertyT IO ()+bicheck gen = do+ v <- forAll gen+ let iv = toFinite v+ v === (fromFinite . toFinite $ v)+ iv === (toFinite @a . fromFinite $ iv)+ v' <- forAll gen+ let iv' = toFinite v'+ compare v v' === compare iv iv' -previousIsCorrect :: forall (a :: Type) . (Finitary a, 1 <= Cardinality a, Show a) => Proxy a -> Property-previousIsCorrect _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a- if x == start- then success- else assert . isJust . previous $ x)+genStorable :: (Storable a) => Gen a -> Gen (VS.Vector 10 a)+genStorable = VS.replicateM -nextIsCorrect :: forall (a :: Type) . (Finitary a, 1 <= Cardinality a, Show a) => Proxy a -> Property-nextIsCorrect _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a- if x == end- then success- else assert . isJust . next $ x)+genUnboxed :: (Unbox a) => Gen a -> Gen (VU.Vector 10 a)+genUnboxed = VU.replicateM --- Check the behaviour of the tuple generic so that we don't violate--- order-preservation-agreesWithOrd :: Property-agreesWithOrd = property $ do let xs = (,) <$> [LT ..] <*> [False ..]- sort xs === sortOn toFinite xs+genRegular :: Gen a -> Gen (V.Vector 10 a)+genRegular = V.replicateM --- Check that we can enumerate properly and that our type, in order, is--- isomorphic to 'finites'-enumeratesProperly :: Property-enumeratesProperly = property $ do let xs = (,) <$> [LT ..] <*> [False ..]- (toFinite <$> sort xs) === finites+genFoo :: Gen Foo+genFoo =+ Gen.choice+ [ pure Bar,+ Baz <$> Gen.enumBounded,+ Quux <$> ((,) <$> Gen.enumBounded <*> Gen.enumBounded)+ ] --- All the tests I want to use-allTests :: [(SomeTestFunction, GroupName)]-allTests = [- (SomeTestFunction isBijection, "bijectivity"),- (SomeTestFunction isOrderPreserving, "order preservation"),- (SomeTestFunction startIsCorrect, "start"),- (SomeTestFunction endIsCorrect, "end"),- (SomeTestFunction previousStartNothing, "previous + start"),- (SomeTestFunction endNextNothing, "next + end"),- (SomeTestFunction previousIsCorrect, "previous"),- (SomeTestFunction nextIsCorrect, "next")- ]+checkBijection :: forall a. (Show a, Ord a, Finitary a) => String -> Gen a -> SpecWith ()+checkBijection name gen =+ it ("should biject " <> name <> " with fromFinite and toFinite preserving order")+ . hedgehog+ $ go+ where+ go = do+ x <- forAll gen+ let ix = toFinite x+ x === (fromFinite . toFinite $ x)+ ix === (toFinite @a . fromFinite $ ix)+ y <- forAll gen+ let iy = toFinite y+ compare x y === compare ix iy -main :: IO Bool-main = andM . (:) (checkSequential . Group "Ord agreement" $ [("ordering", agreesWithOrd), ("totality", enumeratesProperly)]) . fmap (uncurry constructTest) $ allTests+checkMonotonic :: (Show a, Finitary a) => String -> Gen a -> SpecWith ()+checkMonotonic name gen =+ it ("should be Ord-monotonic on Down " <> name)+ . hedgehog+ $ go+ where+ go = do+ x <- forAll gen+ y <- forAll gen+ let dx = toFinite . Down $ x+ let dy = toFinite . Down $ y+ let ix = toFinite x+ let iy = toFinite y+ case compare ix iy of+ LT -> compare dx dy === GT+ EQ -> compare dx dy === EQ+ GT -> compare dx dy === LT