fin 0.2.1 → 0.3.2
raw patch · 7 files changed
Files
- ChangeLog.md +16/−0
- fin.cabal +25/−34
- src/Data/Fin.hs +48/−0
- src/Data/Fin/Enum.hs +0/−177
- src/Data/Nat.hs +0/−10
- src/Data/Type/Nat.hs +50/−7
- test/Inspection.hs +0/−21
ChangeLog.md view
@@ -1,3 +1,19 @@+# Version history for fin++## 0.3.2++- Add `SS' :: SNat n -> SNat (S n)`, pattern synonym with explicit argument.++## 0.3.1++- Support GHC-8.6.5...9.10.1++## 0.3++- Remove `Data.Fin.Enum` module. It didn't work as well as hoped.+- Add `EqP` and `OrdP` instances.+- Add `GShow Fin` instance.+ ## 0.2.1 - Add `boring` instances
fin.cabal view
@@ -1,6 +1,6 @@-cabal-version: >=1.10+cabal-version: 2.2 name: fin-version: 0.2.1+version: 0.3.2 synopsis: Nat and Fin: peano naturals and finite numbers category: Data, Dependent Types, Singletons, Math description:@@ -48,7 +48,7 @@ homepage: https://github.com/phadej/vec bug-reports: https://github.com/phadej/vec/issues-license: BSD3+license: BSD-3-Clause license-file: LICENSE author: Oleg Grenrus <oleg.grenrus@iki.fi> maintainer: Oleg.Grenrus <oleg.grenrus@iki.fi>@@ -56,16 +56,15 @@ build-type: Simple extra-source-files: ChangeLog.md tested-with:- GHC ==7.8.4- || ==7.10.3- || ==8.0.2- || ==8.2.2- || ==8.4.4- || ==8.6.5+ GHC ==8.6.5 || ==8.8.4- || ==8.10.4- || ==9.0.1- || ==9.2.1+ || ==8.10.7+ || ==9.0.2+ || ==9.2.8+ || ==9.4.8+ || ==9.6.5+ || ==9.8.2+ || ==9.10.1 source-repository head type: git@@ -78,7 +77,6 @@ hs-source-dirs: src exposed-modules: Data.Fin- Data.Fin.Enum Data.Nat Data.Type.Nat Data.Type.Nat.LE@@ -86,26 +84,20 @@ Data.Type.Nat.LT other-modules: TrustworthyCompat- build-depends:- base >=4.7 && <4.17- , boring >=0.2 && <0.3- , dec >=0.0.4 && <0.1- , deepseq >=1.3.0.2 && <1.5- , hashable >=1.2.7.0 && <1.5- , QuickCheck >=2.13.2 && <2.15- , some >=1.0.3 && <1.1- , universe-base >=1.1.2 && <1.2 - if !impl(ghc >=8.2)- build-depends: bifunctors >=5.5.3 && <5.6-- if !impl(ghc >=8.0)- build-depends: semigroups >=0.18.5 && <0.21+ -- GHC boot libs+ build-depends:+ , base >=4.12.0.0 && <4.21+ , deepseq >=1.4.4.0 && <1.6 - if !impl(ghc >=7.10)- build-depends:- nats >=1.1.2 && <1.2- , void >=0.7.3 && <0.8+ -- other dependencies+ build-depends:+ , boring ^>=0.2.2+ , dec ^>=0.0.6+ , hashable ^>=1.4.4.0 || ^>=1.5.0.0+ , QuickCheck ^>=2.14.2 || ^>=2.15+ , some ^>=1.0.6+ , universe-base ^>=1.1.4 if impl(ghc >=9.0) -- these flags may abort compilation with GHC-8.10@@ -113,7 +105,6 @@ ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode -- dump-core--- if impl(ghc >= 8.0) -- build-depends: dump-core -- ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html @@ -124,9 +115,9 @@ hs-source-dirs: test default-language: Haskell2010 build-depends:- base+ , base , fin- , inspection-testing >=0.2.0.1 && <0.5+ , inspection-testing >=0.2.0.1 && <0.6 , tagged if !impl(ghc >=8.0)
src/Data/Fin.hs view
@@ -53,8 +53,11 @@ import Control.DeepSeq (NFData (..)) import Data.Bifunctor (bimap)+import Data.EqP (EqP (..))+import Data.GADT.Show (GShow (..)) import Data.Hashable (Hashable (..)) import Data.List.NonEmpty (NonEmpty (..))+import Data.OrdP (OrdP (..)) import Data.Proxy (Proxy (..)) import Data.Type.Nat (Nat (..)) import Data.Typeable (Typeable)@@ -71,10 +74,14 @@ -- $setup -- >>> import Data.List (genericLength) -- >>> import Data.List.NonEmpty (NonEmpty (..))+-- >>> import Data.Foldable (traverse_) -- >>> import Numeric.Natural (Natural) -- >>> import qualified Data.Type.Nat as N -- >>> import qualified Data.Universe.Class as U -- >>> import qualified Data.Universe.Helpers as U+-- >>> import Data.EqP (eqp)+-- >>> import Data.OrdP (comparep)+-- >>> :set -XTypeApplications -XGADTs ------------------------------------------------------------------------------- -- Type@@ -93,11 +100,52 @@ deriving instance Eq (Fin n) deriving instance Ord (Fin n) +-- |+--+-- >>> eqp FZ FZ+-- True+--+-- >>> eqp FZ (FS FZ)+-- False+--+-- >>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]+-- [True,False,False,False,False,False]+-- [False,True,False,False,False,False]+-- [False,False,True,False,False,False]+-- [False,False,False,True,False,False]+--+-- @since 0.2.2+--+instance EqP Fin where+ eqp FZ FZ = True+ eqp FZ (FS _) = False+ eqp (FS _) FZ = False+ eqp (FS n) (FS m) = eqp n m++-- |+--+-- >>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]+-- [EQ,LT,LT,LT,LT,LT]+-- [GT,EQ,LT,LT,LT,LT]+-- [GT,GT,EQ,LT,LT,LT]+-- [GT,GT,GT,EQ,LT,LT]+--+-- @since 0.2.2+instance OrdP Fin where+ comparep FZ FZ = EQ+ comparep FZ (FS _) = LT+ comparep (FS _) FZ = GT+ comparep (FS n) (FS m) = comparep n m+ -- | 'Fin' is printed as 'Natural'. -- -- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec' instance Show (Fin n) where showsPrec d = showsPrec d . toNatural++-- | @since 0.2.2+instance GShow Fin where+ gshowsPrec = showsPrec -- | Operations module @n@. --
− src/Data/Fin/Enum.hs
@@ -1,177 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE EmptyCase #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE Safe #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}--- |------ This module is designed to be imported qualified:------ @--- import qualified Data.Fin.Enum as E--- @----module Data.Fin.Enum (- Enum (..),- -- * Generic implementation- gfrom, GFrom,- gto, GTo,- GEnumSize,- ) where--import Prelude hiding (Enum (..))--import Data.Bifunctor (bimap)-import Data.Fin (Fin (..))-import Data.Nat (Nat (..))-import Data.Proxy (Proxy (..))-import GHC.Generics (M1 (..), U1 (..), V1, (:+:) (..))--import qualified Data.Fin as F-import qualified Data.Type.Nat as N-import qualified Data.Void as V-import qualified GHC.Generics as G---- $setup--- >>> import qualified Data.Fin as F---- | Generic enumerations.------ /Examples:/------ >>> from ()--- 0------ >>> to 0 :: ()--- ()------ >>> to 0 :: Bool--- False------ >>> map to F.universe :: [Bool]--- [False,True]------ >>> map (to . (+1) . from) [LT, EQ, GT] :: [Ordering] -- Num Fin is modulo arithmetic--- [EQ,GT,LT]----class Enum a where- -- | The size of an enumeration.- type EnumSize a :: Nat- type EnumSize a = GEnumSize a-- -- | Converts a value to its index.- from :: a -> Fin (EnumSize a)- default from :: (G.Generic a, GFrom a, EnumSize a ~ GEnumSize a) => a -> Fin (EnumSize a)- from = gfrom-- -- | Converts from index to the original value.- to :: Fin (EnumSize a) -> a- default to :: (G.Generic a, GTo a, EnumSize a ~ GEnumSize a) => Fin (EnumSize a) -> a- to = gto---- | 'Void' ~ 0-instance Enum V.Void where- -- this should be written by hand to work with all @base@- type EnumSize V.Void = N.Nat0- from = V.absurd- to = F.absurd---- | () ~ 1-instance Enum ()---- | 'Bool' ~ 2-instance Enum Bool---- | 'Ordering' ~ 3-instance Enum Ordering---- | 'Either' ~ @+@-instance (Enum a, Enum b, N.SNatI (EnumSize a)) => Enum (Either a b) where- type EnumSize (Either a b) = N.Plus (EnumSize a) (EnumSize b)-- to = bimap to to . F.split- from = F.append . bimap from from------------------------------------------------------------------------------------ EnumSize------------------------------------------------------------------------------------ | Compute the size from the type.-type GEnumSize a = EnumSizeRep (G.Rep a) N.Nat0--type family EnumSizeRep (a :: * -> *) (n :: Nat) :: Nat where- EnumSizeRep (a :+: b ) n = EnumSizeRep a (EnumSizeRep b n)- EnumSizeRep V1 n = n- EnumSizeRep (M1 _d _c a) n = EnumSizeRep a n- EnumSizeRep U1 n = 'S n- -- No instance for K1 or :*:------------------------------------------------------------------------------------ From------------------------------------------------------------------------------------ | Generic version of 'from'.-gfrom :: (G.Generic a, GFrom a) => a -> Fin (GEnumSize a)-gfrom = \x -> gfromRep (G.from x) (Proxy :: Proxy N.Nat0)---- | Constraint for the class that computes 'gfrom'.-type GFrom a = GFromRep (G.Rep a)--class GFromRep (a :: * -> *) where- gfromRep :: a x -> Proxy n -> Fin (EnumSizeRep a n)- gfromSkip :: Proxy a -> Fin n -> Fin (EnumSizeRep a n)--instance (GFromRep a, GFromRep b) => GFromRep (a :+: b) where- gfromRep (L1 a) n = gfromRep a (prSkip n) where- prSkip :: Proxy n -> Proxy (EnumSizeRep b n)- prSkip _ = Proxy- gfromRep (R1 b) n = gfromSkip (Proxy :: Proxy a) (gfromRep b n)-- gfromSkip _ n = gfromSkip (Proxy :: Proxy a) (gfromSkip (Proxy :: Proxy b) n)--instance GFromRep a => GFromRep (M1 d c a) where- gfromRep (M1 a) n = gfromRep a n- gfromSkip _ n = gfromSkip (Proxy :: Proxy a) n--instance GFromRep V1 where- gfromRep v _ = case v of {}- gfromSkip _ n = n--instance GFromRep U1 where- gfromRep U1 _ = FZ- gfromSkip _ n = FS n------------------------------------------------------------------------------------ To------------------------------------------------------------------------------------ | Generic version of 'to'.-gto :: (G.Generic a, GTo a) => Fin (GEnumSize a) -> a-gto = \x -> G.to $ gtoRep x id F.absurd---- | Constraint for the class that computes 'gto'.-type GTo a = GToRep (G.Rep a)--class GToRep (a :: * -> *) where- gtoRep :: Fin (EnumSizeRep a n) -> (a x -> r) -> (Fin n -> r) -> r--instance (GToRep a, GToRep b) => GToRep (a :+: b) where- gtoRep n s k = gtoRep n (s . L1) $ \r -> gtoRep r (s . R1) k--instance GToRep a => GToRep (M1 d c a) where- gtoRep n s = gtoRep n (s . M1)--instance GToRep V1 where- gtoRep n _ k = k n--instance GToRep U1 where- gtoRep FZ s _ = s U1- gtoRep (FS n) _ k = k n
src/Data/Nat.hs view
@@ -1,11 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE Safe #-}--#if __GLASGOW_HASKELL__ < 710-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE StandaloneDeriving #-}-#endif -- | 'Nat' numbers. -- -- This module is designed to be imported qualified.@@ -44,11 +39,6 @@ -- Better than GHC's built-in 'GHC.TypeLits.Nat' for some use cases. -- data Nat = Z | S Nat deriving (Eq, Typeable, Data)--#if __GLASGOW_HASKELL__ < 710-deriving instance Typeable 'Z-deriving instance Typeable 'S-#endif -- | 'Nat' is printed as 'Natural'. --
src/Data/Type/Nat.hs view
@@ -1,9 +1,9 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}@@ -11,6 +11,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-} -- | 'Nat' numbers. @DataKinds@ stuff. -- -- This module re-exports "Data.Nat", and adds type-level things.@@ -24,7 +25,7 @@ explicitShow, explicitShowsPrec, -- * Singleton- SNat(..),+ SNat(SZ,SS,SS'), snatToNat, snatToNatural, -- * Implicit@@ -67,10 +68,12 @@ import Control.DeepSeq (NFData (..)) import Data.Boring (Boring (..))+import Data.EqP (EqP (..)) import Data.Function (fix)-import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..))+import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..), defaultCompare, defaultEq) import Data.GADT.DeepSeq (GNFData (..)) import Data.GADT.Show (GShow (..))+import Data.OrdP (OrdP (..)) import Data.Proxy (Proxy (..)) import Data.Type.Dec (Dec (..)) import Data.Typeable (Typeable)@@ -177,6 +180,35 @@ snatToNatural SS = unKonst (induction (Konst 0) (kmap succ) :: Konst Natural n) -------------------------------------------------------------------------------+-- Explicit constructor+-------------------------------------------------------------------------------++data SNat_ (n :: Nat) where+ SZ_ :: SNat_ 'Z+ SS_ :: SNat n -> SNat_ ('S n)++snat_ :: SNat n -> SNat_ n+snat_ SZ = SZ_+snat_ SS = SS_ snat++-- | A pattern with explicit argument+--+-- >>> let predSNat :: SNat (S n) -> SNat n; predSNat (SS' n) = n+-- >>> predSNat (SS' (SS' SZ))+-- SS+--+-- >>> reflect $ predSNat (SS' (SS' SZ))+-- 1+--+--+-- @since 0.3.2+pattern SS' :: () => (m ~ 'S n) => SNat n -> SNat m+pattern SS' n <- (snat_ -> SS_ n)+ where SS' n = withSNat n SS++{-# COMPLETE SZ, SS' #-}++------------------------------------------------------------------------------- -- Equality ------------------------------------------------------------------------------- @@ -245,10 +277,6 @@ EqNat ('S n) ('S m) = EqNat n m EqNat n m = 'False -#if !MIN_VERSION_base(4,11,0)-type instance n == m = EqNat n m-#endif- -- | @since 0.2.1 instance SNatI n => Boring (SNat n) where boring = snat@@ -266,6 +294,7 @@ instance GNFData SNat where grnf = rnf + -- | @since 0.2.1 instance GEq SNat where geq = testEquality@@ -276,6 +305,20 @@ gcompare SZ SS = GLT gcompare SS SZ = GGT gcompare SS SS = cmpNat++-- | @since 0.2.2+instance Eq (SNat a) where+ _ == _ = True++-- | @since 0.2.2+instance Ord (SNat a) where+ compare _ _ = EQ++-- | @since 0.2.2+instance EqP SNat where eqp = defaultEq++-- | @since 0.2.2+instance OrdP SNat where comparep = defaultCompare -- | Decide equality of type-level numbers. --
test/Inspection.hs view
@@ -17,7 +17,6 @@ import Test.Inspection import qualified Data.Fin as F-import qualified Data.Fin.Enum as E import qualified Data.Type.Nat as N import Unsafe.Coerce (unsafeCoerce)@@ -51,26 +50,6 @@ inspect $ 'lhsInline === 'rhs inspect $ 'lhsNormal =/= 'rhs------------------------------------------------------------------------------------ Enum------------------------------------------------------------------------------------ | Note: GHC 8.0 (but not GHC 8.2?) seems to be--- so smart, it reuses dictionary value.------ Therefore, we define own local Ordering'-data Ordering' = LT' | EQ' | GT' deriving (Generic)--lhsEnum :: Ordering' -> F.Fin N.Nat3-lhsEnum = E.gfrom--rhsEnum :: Ordering' -> F.Fin N.Nat3-rhsEnum LT' = FZ-rhsEnum EQ' = FS FZ-rhsEnum GT' = FS (FS FZ)--inspect $ 'lhsEnum ==- 'rhsEnum ------------------------------------------------------------------------------- -- Proofs