diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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! diff --git a/finitary.cabal b/finitary.cabal --- a/finitary.cabal +++ b/finitary.cabal @@ -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 diff --git a/src/Data/Finitary.hs b/src/Data/Finitary.hs --- a/src/Data/Finitary.hs +++ b/src/Data/Finitary.hs @@ -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 + - Copyright (C) 2019-2020 Koz Ross - - 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 . -} -{-# 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 diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -1,3 +1,10 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + {- - Copyright (C) 2019 Koz Ross - @@ -15,165 +22,209 @@ - along with this program. If not, see . -} -{-# 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