fin 0.1.1 → 0.3.2
raw patch · 11 files changed
Files
- ChangeLog.md +34/−1
- fin.cabal +35/−33
- src/Data/Fin.hs +111/−24
- src/Data/Fin/Enum.hs +0/−170
- src/Data/Nat.hs +45/−13
- src/Data/Type/Nat.hs +179/−109
- src/Data/Type/Nat/LE.hs +20/−4
- src/Data/Type/Nat/LE/ReflStep.hs +27/−6
- src/Data/Type/Nat/LT.hs +4/−0
- src/TrustworthyCompat.hs +11/−0
- test/Inspection.hs +19/−26
ChangeLog.md view
@@ -1,4 +1,37 @@-# Revision history for fin+# 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+- Explicitly implement `>=` and `>` for `Nat`.+- `<=`, `>=` and `min` for `Nat` are lazier+- Add `NFData (SNat n)` instance+- Add `GEq`, `GCompare`, `GNFData`, `GShow` (from `some` package) instances for `SNat`.++## 0.2++- `SNat` is now what was called `InlineInduction`.+ To migrate code from `fin-0.1` to `fin-0.2` it's often enough to+ replace `InlineInduction` with `SNatI`, and `inlineInduction` with `induction`. +- Explicitly mark all modules as Safe or Trustworthy.++## 0.1.2++- Add `universe-base` `Universe` and `Finite` instances ## 0.1.1
fin.cabal view
@@ -1,6 +1,6 @@-cabal-version: >=1.10+cabal-version: 2.2 name: fin-version: 0.1.1+version: 0.3.2 synopsis: Nat and Fin: peano naturals and finite numbers category: Data, Dependent Types, Singletons, Math description:@@ -48,21 +48,23 @@ 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>-copyright: (c) 2017-2019 Oleg Grenrus+copyright: (c) 2017-2021 Oleg Grenrus 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- || ==8.8.1+ GHC ==8.6.5+ || ==8.8.4+ || ==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@@ -70,39 +72,39 @@ subdir: fin library+ default-language: Haskell2010+ ghc-options: -Wall -fprint-explicit-kinds+ hs-source-dirs: src exposed-modules: Data.Fin- Data.Fin.Enum Data.Nat Data.Type.Nat Data.Type.Nat.LE Data.Type.Nat.LE.ReflStep Data.Type.Nat.LT - build-depends:- base >=4.7 && <4.14- , dec >=0.0.3 && <0.1- , deepseq >=1.3.0.2 && <1.5- , hashable >=1.2.7.0 && <1.4- , QuickCheck >=2.13.2 && <2.14-- if !impl(ghc >=8.2)- build-depends: bifunctors >=5.5.3 && <5.6+ other-modules: TrustworthyCompat - if !impl(ghc >=8.0)- build-depends: semigroups >=0.18.4 && <0.20+ -- 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.2 && <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 - ghc-options: -Wall -fprint-explicit-kinds- hs-source-dirs: src- default-language: Haskell2010+ if impl(ghc >=9.0)+ -- these flags may abort compilation with GHC-8.10+ -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295+ 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 @@ -113,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
@@ -3,6 +3,7 @@ {-# LANGUAGE EmptyCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeOperators #-}@@ -52,18 +53,36 @@ 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) import GHC.Exception (ArithException (..), throw) import Numeric.Natural (Natural) -import qualified Data.List.NonEmpty as NE-import qualified Data.Type.Nat as N-import qualified Test.QuickCheck as QC+import qualified Data.Boring as Boring+import qualified Data.List.NonEmpty as NE+import qualified Data.Type.Nat as N+import qualified Data.Universe.Class as U+import qualified Data.Universe.Helpers as U+import qualified Test.QuickCheck as QC +-- $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 -------------------------------------------------------------------------------@@ -81,12 +100,53 @@ 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@. -- -- >>> map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3]@@ -143,14 +203,14 @@ -- -- @since 0.1.1 ---mirror :: forall n. N.InlineInduction n => Fin n -> Fin n-mirror = getMirror (N.inlineInduction start step) where+mirror :: forall n. N.SNatI n => Fin n -> Fin n+mirror = getMirror (N.induction start step) where start :: Mirror 'Z start = Mirror id - step :: forall m. N.InlineInduction m => Mirror m -> Mirror ('S m)+ step :: forall m. N.SNatI m => Mirror m -> Mirror ('S m) step (Mirror rec) = Mirror $ \n -> case n of- FZ -> getMaxBound (N.inlineInduction (MaxBound FZ) (MaxBound . FS . getMaxBound))+ FZ -> getMaxBound (N.induction (MaxBound FZ) (MaxBound . FS . getMaxBound)) FS m -> weakenLeft1 (rec m) newtype Mirror n = Mirror { getMirror :: Fin n -> Fin n }@@ -202,6 +262,14 @@ hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ -------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.2.1+instance n ~ 'Z => Boring.Absurd (Fin n) where+ absurd = absurd++------------------------------------------------------------------------------- -- QuickCheck ------------------------------------------------------------------------------- @@ -228,13 +296,32 @@ instance (n ~ 'S m, N.SNatI m) => QC.Function (Fin n) where function = case N.snat :: N.SNat m of- N.SZ -> QC.functionMap (\FZ -> ()) (\() -> FZ)- N.SS -> QC.functionMap isMin (maybe FZ FS)+ N.SZ -> QC.functionMap (\_ -> ()) (\() -> FZ)+ N.SS -> QC.functionMap isMin (maybe FZ FS) -- TODO: https://github.com/nick8325/quickcheck/pull/283 -- newtype Fun b m = Fun { getFun :: (Fin ('S m) -> b) -> Fin ('S m) QC.:-> b } -------------------------------------------------------------------------------+-- universe-base+-------------------------------------------------------------------------------++-- | @since 0.1.2+instance N.SNatI n => U.Universe (Fin n) where+ universe = universe++-- |+--+-- >>> (U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))+-- True+--+-- @since 0.1.2+--+instance N.SNatI n => U.Finite (Fin n) where+ universeF = U.universe+ cardinality = U.Tagged $ N.reflectToNum (Proxy :: Proxy n)++------------------------------------------------------------------------------- -- Showing ------------------------------------------------------------------------------- @@ -338,15 +425,15 @@ -- -- >>> inlineUniverse :: [Fin N.Nat3] -- [0,1,2]-inlineUniverse :: N.InlineInduction n => [Fin n]-inlineUniverse = getUniverse $ N.inlineInduction (Universe []) step where+inlineUniverse :: N.SNatI n => [Fin n]+inlineUniverse = getUniverse $ N.induction (Universe []) step where step :: Universe n -> Universe ('S n) step (Universe xs) = Universe (FZ : map FS xs) -- | >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3) -- 0 :| [1,2]-inlineUniverse1 :: N.InlineInduction n => NonEmpty (Fin ('S n))-inlineUniverse1 = getUniverse1 $ N.inlineInduction (Universe1 (FZ :| [])) step where+inlineUniverse1 :: N.SNatI n => NonEmpty (Fin ('S n))+inlineUniverse1 = getUniverse1 $ N.induction (Universe1 (FZ :| [])) step where step :: Universe1 n -> Universe1 ('S n) step (Universe1 xs) = Universe1 (NE.cons FZ (fmap FS xs)) @@ -392,8 +479,8 @@ -- -- @since 0.1.1 ---isMax :: forall n. N.InlineInduction n => Fin ('S n) -> Maybe (Fin n)-isMax = getIsMax (N.inlineInduction start step) where+isMax :: forall n. N.SNatI n => Fin ('S n) -> Maybe (Fin n)+isMax = getIsMax (N.induction start step) where start :: IsMax 'Z start = IsMax $ \_ -> Nothing @@ -419,8 +506,8 @@ -- [0,1,2,3] -- -- @since 0.1.1-weakenLeft1 :: N.InlineInduction n => Fin n -> Fin ('S n)-weakenLeft1 = getWeaken1 (N.inlineInduction start step) where+weakenLeft1 :: N.SNatI n => Fin n -> Fin ('S n)+weakenLeft1 = getWeaken1 (N.induction start step) where start :: Weaken1 'Z start = Weaken1 absurd @@ -433,8 +520,8 @@ -- | >>> map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3]) -- [0,1,2]-weakenLeft :: forall n m. N.InlineInduction n => Proxy m -> Fin n -> Fin (N.Plus n m)-weakenLeft _ = getWeakenLeft (N.inlineInduction start step :: WeakenLeft m n) where+weakenLeft :: forall n m. N.SNatI n => Proxy m -> Fin n -> Fin (N.Plus n m)+weakenLeft _ = getWeakenLeft (N.induction start step :: WeakenLeft m n) where start :: WeakenLeft m 'Z start = WeakenLeft absurd @@ -447,8 +534,8 @@ -- | >>> map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3]) -- [2,3,4]-weakenRight :: forall n m. N.InlineInduction n => Proxy n -> Fin m -> Fin (N.Plus n m)-weakenRight _ = getWeakenRight (N.inlineInduction start step :: WeakenRight m n) where+weakenRight :: forall n m. N.SNatI n => Proxy n -> Fin m -> Fin (N.Plus n m)+weakenRight _ = getWeakenRight (N.induction start step :: WeakenRight m n) where start = WeakenRight id step (WeakenRight go) = WeakenRight $ \x -> FS $ go x @@ -462,7 +549,7 @@ -- >>> append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4)) -- 7 ---append :: forall n m. N.InlineInduction n => Either (Fin n) (Fin m) -> Fin (N.Plus n m)+append :: forall n m. N.SNatI n => Either (Fin n) (Fin m) -> Fin (N.Plus n m) append (Left n) = weakenLeft (Proxy :: Proxy m) n append (Right m) = weakenRight (Proxy :: Proxy n) m @@ -477,8 +564,8 @@ -- >>> map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)] -- [Left 0,Left 1,Right 0,Right 1,Right 2] ---split :: forall n m. N.InlineInduction n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)-split = getSplit (N.inlineInduction start step) where+split :: forall n m. N.SNatI n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)+split = getSplit (N.induction start step) where start :: Split m 'Z start = Split Right
− src/Data/Fin/Enum.hs
@@ -1,170 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-}-{-# 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---- | 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.InlineInduction (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) (error "gfrom: internal error" :: Fin N.Nat0)---- | Constraint for the class that computes 'gfrom'.-type GFrom a = GFromRep (G.Rep a)--class GFromRep (a :: * -> *) where- gfromRep :: a x -> Fin 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 (gfromSkip (Proxy :: Proxy b) n)- 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 _ n = n- 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,10 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-}--#if __GLASGOW_HASKELL__ < 710-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE StandaloneDeriving #-}-#endif+{-# LANGUAGE Safe #-} -- | 'Nat' numbers. -- -- This module is designed to be imported qualified.@@ -29,8 +25,11 @@ import GHC.Exception (ArithException (..), throw) import Numeric.Natural (Natural) -import qualified Test.QuickCheck as QC+import qualified Data.Universe.Class as U+import qualified Test.QuickCheck as QC +-- $setup+ ------------------------------------------------------------------------------- -- Nat -------------------------------------------------------------------------------@@ -39,12 +38,7 @@ -- -- Better than GHC's built-in 'GHC.TypeLits.Nat' for some use cases. ---data Nat = Z | S Nat deriving (Eq, Ord, Typeable, Data)--#if __GLASGOW_HASKELL__ < 710-deriving instance Typeable 'Z-deriving instance Typeable 'S-#endif+data Nat = Z | S Nat deriving (Eq, Typeable, Data) -- | 'Nat' is printed as 'Natural'. --@@ -53,6 +47,29 @@ instance Show Nat where showsPrec d = showsPrec d . toNatural +instance Ord Nat where+ compare Z Z = EQ+ compare Z (S _) = LT+ compare (S _) Z = GT+ compare (S n) (S m) = compare n m++ Z <= _ = True+ S _ <= Z = False+ S n <= S m = n <= m++ n < m = not (m <= n)+ n > m = not (n <= m)+ n >= m = m <= n++ min Z _ = Z+ min (S _) Z = Z+ min (S n) (S m) = S (min n m)++ max Z Z = Z+ max Z m@(S _) = m+ max n@(S _) Z = n+ max (S n) (S m) = S (max n m)+ instance Num Nat where fromInteger = fromNatural . fromInteger @@ -114,11 +131,26 @@ shrink (S n) = n : QC.shrink n instance QC.CoArbitrary Nat where- coarbitrary Z = QC.variant (0 :: Int) + coarbitrary Z = QC.variant (0 :: Int) coarbitrary (S n) = QC.variant (1 :: Int) . QC.coarbitrary n instance QC.Function Nat where function = QC.functionIntegral++-------------------------------------------------------------------------------+-- universe-base+-------------------------------------------------------------------------------++-- |+--+-- >>> import qualified Data.Universe.Class as U+-- >>> take 10 (U.universe :: [Nat])+-- [0,1,2,3,4,5,6,7,8,9]+--+-- @since 0.1.2+instance U.Universe Nat where+ universe = go Z where+ go n = n : go (S n) ------------------------------------------------------------------------------- -- Showing
src/Data/Type/Nat.hs view
@@ -1,15 +1,17 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-} -- | 'Nat' numbers. @DataKinds@ stuff. -- -- This module re-exports "Data.Nat", and adds type-level things.@@ -23,11 +25,12 @@ explicitShow, explicitShowsPrec, -- * Singleton- SNat(..),+ SNat(SZ,SS,SS'), snatToNat, snatToNatural, -- * Implicit SNatI(..),+ snat, withSNat, reify, reflect,@@ -36,11 +39,9 @@ eqNat, EqNat, discreteNat,+ cmpNat, -- * Induction- induction, induction1,- InlineInduction (..),- inlineInduction, -- ** Example: unfoldedFix unfoldedFix, -- * Arithmetic@@ -65,26 +66,34 @@ proofMultNOne, ) where -import Data.Function (fix)-import Data.Proxy (Proxy (..))-import Data.Type.Dec (Dec (..))-import Data.Type.Equality ((:~:) (..), TestEquality (..))-import Data.Typeable (Typeable)-import Numeric.Natural (Natural)+import Control.DeepSeq (NFData (..))+import Data.Boring (Boring (..))+import Data.EqP (EqP (..))+import Data.Function (fix)+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)+import Numeric.Natural (Natural) import qualified GHC.TypeLits as GHC import Unsafe.Coerce (unsafeCoerce) -#if !MIN_VERSION_base(4,11,0)-import Data.Type.Equality (type (==))-#endif- import Data.Nat+import TrustworthyCompat -- $setup -- >>> :set -XTypeOperators -XDataKinds--- >>> import Data.Type.Dec (decShow)+-- >>> import qualified GHC.TypeLits as GHC+-- >>> import Data.Type.Dec (Dec (..), decShow)+-- >>> import Data.Type.Equality+-- >>> import Control.Applicative (Const (..))+-- >>> import Data.Coerce (coerce)+-- >>> import Data.GADT.Compare (GOrdering (..)) ------------------------------------------------------------------------------- -- SNat@@ -98,11 +107,34 @@ deriving instance Show (SNat p) --- | Convenience class to get 'SNat'.-class SNatI (n :: Nat) where snat :: SNat n-instance SNatI 'Z where snat = SZ-instance SNatI n => SNatI ('S n) where snat = SS+-- | Implicit 'SNat'.+--+-- In an unorthodox singleton way, it actually provides an induction function.+--+-- The induction should often be fully inlined.+-- See @test/Inspection.hs@.+--+-- >>> :set -XPolyKinds+-- >>> newtype Const a b = Const a deriving (Show)+-- >>> induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3+-- Const 6+--+class SNatI (n :: Nat) where+ induction+ :: f 'Z -- ^ zero case+ -> (forall m. SNatI m => f m -> f ('S m)) -- ^ induction step+ -> f n +instance SNatI 'Z where+ induction n _c = n++instance SNatI n => SNatI ('S n) where+ induction n c = c (induction n c)++-- | Construct explicit 'SNat' value.+snat :: SNatI n => SNat n+snat = induction SZ (\_ -> SS)+ -- | Constructor 'SNatI' dictionary from 'SNat'. -- -- @since 0.0.3@@ -112,11 +144,11 @@ -- | Reflect type-level 'Nat' to the term level. reflect :: forall n proxy. SNatI n => proxy n -> Nat-reflect _ = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)+reflect _ = unKonst (induction (Konst Z) (kmap S) :: Konst Nat n) -- | As 'reflect' but with any 'Num'. reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m-reflectToNum _ = unTagged (induction1 (Tagged 0) (retagMap (1+)) :: Tagged n m)+reflectToNum _ = unKonst (induction (Konst 0) (kmap (1+)) :: Konst m n) -- | Reify 'Nat'. --@@ -133,7 +165,7 @@ -- snatToNat :: forall n. SNat n -> Nat snatToNat SZ = Z-snatToNat SS = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)+snatToNat SS = unKonst (induction (Konst Z) (kmap S) :: Konst Nat n) -- | Convert 'SNat' to 'Natural' --@@ -145,9 +177,38 @@ -- snatToNatural :: forall n. SNat n -> Natural snatToNatural SZ = 0-snatToNatural SS = unTagged (induction1 (Tagged 0) (retagMap succ) :: Tagged n Natural)+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 ------------------------------------------------------------------------------- @@ -216,76 +277,100 @@ 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 +-- | @since 0.2.1+instance GShow SNat where+ gshowsPrec = showsPrec++-- | @since 0.2.1+instance NFData (SNat n) where+ rnf SZ = ()+ rnf SS = ()++-- | @since 0.2.1+instance GNFData SNat where+ grnf = rnf+++-- | @since 0.2.1+instance GEq SNat where+ geq = testEquality++-- | @since 0.2.1+instance GCompare SNat where+ gcompare SZ SZ = GEQ+ 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.+--+-- >>> cmpNat :: GOrdering Nat3 (Plus Nat1 Nat2)+-- GEQ+--+-- >>> cmpNat :: GOrdering Nat3 (Mult Nat2 Nat2)+-- GLT+--+-- >>> cmpNat :: GOrdering Nat5 (Mult Nat2 Nat2)+-- GGT+--+cmpNat :: forall n m. (SNatI n, SNatI m) => GOrdering n m+cmpNat = getNatCmp $ induction (NatCmp start) (\p -> NatCmp (step p)) where+ start :: forall p. SNatI p => GOrdering 'Z p+ start = case snat :: SNat p of+ SZ -> GEQ+ SS -> GLT++ step :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) q+ step hind = case snat :: SNat q of+ SZ -> GGT+ SS -> step' hind++ step' :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) ('S q)+ step' (NatCmp hind) = case hind :: GOrdering p q of+ GEQ -> GEQ+ GLT -> GLT+ GGT -> GGT++newtype NatCmp n = NatCmp { getNatCmp :: forall m. SNatI m => GOrdering n m }+ ------------------------------------------------------------------------------- -- Induction ------------------------------------------------------------------------------- +newtype Konst a (n :: Nat) = Konst { unKonst :: a }++kmap :: (a -> b) -> Konst a n -> Konst b m+kmap = coerce++newtype Flipped f a (b :: Nat) = Flip { unflip :: f b a }+ -- | Induction on 'Nat', functor form. Useful for computation. ----- >>> induction1 (Tagged 0) $ retagMap (+2) :: Tagged Nat3 Int--- Tagged 6--- induction1 :: forall n f a. SNatI n => f 'Z a -- ^ zero case -> (forall m. SNatI m => f m a -> f ('S m) a) -- ^ induction step -> f n a-induction1 z f = go where- go :: forall m. SNatI m => f m a- go = case snat :: SNat m of- SZ -> z- SS -> f go---- | Induction on 'Nat'.------ Useful in proofs or with GADTs, see source of 'proofPlusNZero'.-induction- :: forall n f. SNatI n- => f 'Z -- ^ zero case- -> (forall m. SNatI m => f m -> f ('S m)) -- ^ induction step- -> f n-induction z f = go where- go :: forall m. SNatI m => f m- go = case snat :: SNat m of- SZ -> z- SS -> f go---- | The induction will be fully inlined.------ See @test/Inspection.hs@.-class SNatI n => InlineInduction (n :: Nat) where- inlineInduction1 :: f 'Z a -> (forall m. InlineInduction m => f m a -> f ('S m) a) -> f n a--instance InlineInduction 'Z where- inlineInduction1 z _ = z--instance InlineInduction n => InlineInduction ('S n) where- inlineInduction1 z f = f (inlineInduction1 z f)-- -- Specialise this to few first numerals.- {-# SPECIALIZE instance InlineInduction ('S 'Z) #-}- {-# SPECIALIZE instance InlineInduction ('S ('S 'Z)) #-}- {-# SPECIALIZE instance InlineInduction ('S ('S ('S 'Z))) #-}- {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S 'Z)))) #-}- {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S 'Z))))) #-}- {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S 'Z)))))) #-}- {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S 'Z))))))) #-}- {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) #-}- {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) #-}---- | See 'InlineInduction'.-inlineInduction- :: forall n f. InlineInduction n- => f 'Z -- ^ zero case- -> (forall m. InlineInduction m => f m -> f ('S m)) -- ^ induction step- -> f n-inlineInduction z f = unConst' $ inlineInduction1 (Const' z) (Const' . f . unConst')--newtype Const' (f :: Nat -> *) (n :: Nat) a = Const' { unConst' :: f n }+induction1 z f = unflip (induction (Flip z) (\(Flip x) -> Flip (f x)))+{-# INLINE induction1 #-} -- | Unfold @n@ steps of a general recursion. --@@ -298,15 +383,15 @@ -- 'unfoldedFix' ('Proxy' :: 'Proxy' 'Nat3') f = f (f (f (fix f))) -- @ ---unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a-unfoldedFix _ = getFix (inlineInduction1 start step :: Fix n a) where- start :: Fix 'Z a+unfoldedFix :: forall n a proxy. SNatI n => proxy n -> (a -> a) -> a+unfoldedFix _ = getFix (induction start step :: Fix a n) where+ start :: Fix a 'Z start = Fix fix - step :: Fix m a -> Fix ('S m) a+ step :: Fix a m -> Fix a ('S m) step (Fix go) = Fix $ \f -> f (go f) -newtype Fix (n :: Nat) a = Fix { getFix :: (a -> a) -> a }+newtype Fix a (n :: Nat) = Fix { getFix :: (a -> a) -> a } ------------------------------------------------------------------------------- -- Conversion to GHC Nat@@ -315,7 +400,7 @@ -- | Convert to GHC 'GHC.Nat'. -- -- >>> :kind! ToGHC Nat5--- ToGHC Nat5 :: GHC.Nat+-- ToGHC Nat5 :: GHC.Nat... -- = 5 -- type family ToGHC (n :: Nat) :: GHC.Nat where@@ -363,13 +448,13 @@ -- | Division by two. 'False' is 0 and 'True' is 1 as a remainder. ----- >>> :kind! DivMod2 Nat7--- DivMod2 Nat7 :: (Nat, Bool)--- = '( 'S ('S ('S 'Z)), 'True)+-- >>> :kind! DivMod2 Nat7 == '(Nat3, True)+-- DivMod2 Nat7 == '(Nat3, True) :: Bool+-- = 'True ----- >>> :kind! DivMod2 Nat4--- DivMod2 Nat4 :: (Nat, Bool)--- = '( 'S ('S 'Z), 'False)+-- >>> :kind! DivMod2 Nat4 == '(Nat2, False)+-- DivMod2 Nat4 == '(Nat2, False) :: Bool+-- = 'True -- type family DivMod2 (n :: Nat) :: (Nat, Bool) where DivMod2 'Z = '( 'Z, 'False)@@ -451,18 +536,3 @@ newtype ProofMultNOne n = ProofMultNOne { getProofMultNOne :: Mult n Nat1 :~: n } -- TODO: multAssoc------------------------------------------------------------------------------------ Tagged------------------------------------------------------------------------------------ Own 'Tagged', to not depend on @tagged@------ We shouldn't export this in public interface.-newtype Tagged (n :: Nat) a = Tagged a deriving Show--unTagged :: Tagged n a -> a-unTagged (Tagged a) = a--retagMap :: (a -> b) -> Tagged n a -> Tagged m b-retagMap f = Tagged . f . unTagged
src/Data/Type/Nat/LE.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeOperators #-}@@ -48,13 +49,16 @@ proofZeroLEZero, ) where -import Data.Type.Dec (Dec (..), Decidable (..), Neg)-import Data.Type.Equality ((:~:) (..))-import Data.Typeable (Typeable)-import Data.Void (absurd)+import Data.Boring (Boring (..), Absurd (..))+import Data.Type.Dec (Dec (..), Decidable (..), Neg)+import Data.Typeable (Typeable) import Data.Type.Nat+import TrustworthyCompat +-- $setup+-- >>> import Data.Type.Nat+ ------------------------------------------------------------------------------- -- Proof -------------------------------------------------------------------------------@@ -158,6 +162,18 @@ -- leSwap' :: LEProof n m -> LEProof ('S m) n -> void leSwap' p (LESucc q) = case p of LESucc p' -> leSwap' p' q++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.2.1+instance LE n m => Boring (LEProof n m) where+ boring = leProof++-- | @since 0.2.1+instance (LE m n, n' ~ 'S n) => Absurd (LEProof n' m) where+ absurd = leSwap' leProof ------------------------------------------------------------------------------- -- Dedidablity
src/Data/Type/Nat/LE/ReflStep.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeOperators #-}@@ -35,14 +36,16 @@ proofZeroLEZero, ) where -import Data.Type.Dec (Dec (..), Decidable (..), Neg)-import Data.Type.Equality ((:~:) (..))-import Data.Typeable (Typeable)-import Data.Void (absurd)+import Data.Boring (Absurd (..), Boring (..))+import Data.Type.Dec (Dec (..), Decidable (..), Neg)+import Data.Typeable (Typeable) -import Data.Type.Nat-import qualified Data.Type.Nat.LE as ZeroSucc+import qualified Control.Category as C +import Data.Type.Nat+import qualified Data.Type.Nat.LE as ZeroSucc+import TrustworthyCompat+ ------------------------------------------------------------------------------- -- Proof -------------------------------------------------------------------------------@@ -62,6 +65,12 @@ instance Ord (LEProof n m) where compare _ _ = EQ +-- | The other variant ('Data.Type.Nat.LE.LEPRoof') isn't 'C.Category',+-- because 'Data.Type.Nat.LE.leRefl` requires 'SNat' evidence.+instance C.Category LEProof where+ id = leRefl+ (.) = flip leTrans+ ------------------------------------------------------------------------------- -- Conversion -------------------------------------------------------------------------------@@ -141,6 +150,18 @@ leSwap' :: LEProof n m -> LEProof ('S m) n -> void leSwap' p LERefl = case p of LEStep p' -> leSwap' (leStepL p') LERefl leSwap' p (LEStep q) = leSwap' (leStepL p) q++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.2.1+instance (ZeroSucc.LE n m, SNatI m) => Boring (LEProof n m) where+ boring = fromZeroSucc ZeroSucc.leProof++-- | @since 0.2.1+instance (ZeroSucc.LE m n, n' ~ 'S n, SNatI n) => Absurd (LEProof n' m) where+ absurd = ZeroSucc.leSwap' ZeroSucc.leProof . toZeroSucc ------------------------------------------------------------------------------- -- Decidability
src/Data/Type/Nat/LT.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}@@ -19,6 +20,9 @@ import Data.Type.Nat import Data.Type.Nat.LE++-- $setup+-- >>> import Data.Type.Nat -- | An evidence \(n < m\) which is the same as (\1 + n \le m\). type LTProof n m = LEProof ('S n) m
+ src/TrustworthyCompat.hs view
@@ -0,0 +1,11 @@+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE Trustworthy #-}+module TrustworthyCompat (+ (:~:) (..),+ TestEquality (..),+ coerce,+ type (==),+) where++import Data.Coerce (coerce)+import Data.Type.Equality (TestEquality (..), type (==), (:~:) (..))
test/Inspection.hs view
@@ -1,5 +1,7 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeOperators #-}@@ -15,23 +17,34 @@ 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) ---------------------------------------------------------------------------------- InlineInduction+-- SNatI ------------------------------------------------------------------------------- -- | This doesn't evaluate compile time. lhsInline :: Int-lhsInline = unTagged (N.inlineInduction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)+lhsInline = unTagged (N.induction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int) -- | This doesn't evaluate compile time. lhsNormal :: Int-lhsNormal = unTagged (N.induction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)+lhsNormal = unTagged (manualInduction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int) +--- | Induction on 'Nat'.+manualInduction1+ :: forall n f a. N.SNatI n+ => f 'N.Z a -- ^ zero case+ -> (forall m. N.SNatI m => f m a -> f ('N.S m) a) -- ^ induction step+ -> f n a+manualInduction1 z f = go where+ go :: forall m. N.SNatI m => f m a+ go = case N.snat :: N.SNat m of+ N.SZ -> z+ N.SS -> f go+ rhs :: Int rhs = 5 @@ -39,26 +52,6 @@ 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 ------------------------------------------------------------------------------- @@ -110,10 +103,10 @@ -- Power ------------------------------------------------------------------------------- -power :: forall n. N.InlineInduction n => Proxy n -> Int -> Int+power :: forall n. N.SNatI n => Proxy n -> Int -> Int power _ k = unTagged impl where impl :: Tagged n Int- impl = N.inlineInduction1 (Tagged 1) $ \(Tagged rec') -> Tagged (rec' * k)+ impl = N.induction1 (Tagged 1) $ \(Tagged rec') -> Tagged (rec' * k) lhsPower5 :: Int -> Int lhsPower5 = power (Proxy :: Proxy N.Nat5)