fin 0 → 0.0.1
raw patch · 5 files changed
+58/−17 lines, 5 filesdep ~basedep ~hashabledep ~inspection-testingPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: base, hashable, inspection-testing, nats, semigroups
API changes (from Hackage documentation)
- Data.Fin.Enum: instance (Data.Fin.Enum.GFromRep a, Data.Fin.Enum.GFromRep b) => Data.Fin.Enum.GFromRep (a GHC.Generics.:+: b)
- Data.Fin.Enum: instance (Data.Fin.Enum.GToRep a, Data.Fin.Enum.GToRep b) => Data.Fin.Enum.GToRep (a GHC.Generics.:+: b)
- Data.Fin.Enum: instance Data.Fin.Enum.GFromRep GHC.Generics.U1
- Data.Fin.Enum: instance Data.Fin.Enum.GFromRep GHC.Generics.V1
- Data.Fin.Enum: instance Data.Fin.Enum.GFromRep a => Data.Fin.Enum.GFromRep (GHC.Generics.M1 d c a)
- Data.Fin.Enum: instance Data.Fin.Enum.GToRep GHC.Generics.U1
- Data.Fin.Enum: instance Data.Fin.Enum.GToRep GHC.Generics.V1
- Data.Fin.Enum: instance Data.Fin.Enum.GToRep a => Data.Fin.Enum.GToRep (GHC.Generics.M1 d c a)
+ Data.Fin.Enum: instance (Data.Fin.Enum.GFromRep a, Data.Fin.Enum.GFromRep b) => Data.Fin.Enum.GFromRep ((GHC.Generics.:+:) * a b)
+ Data.Fin.Enum: instance (Data.Fin.Enum.GToRep a, Data.Fin.Enum.GToRep b) => Data.Fin.Enum.GToRep ((GHC.Generics.:+:) * a b)
+ Data.Fin.Enum: instance Data.Fin.Enum.GFromRep (GHC.Generics.U1 *)
+ Data.Fin.Enum: instance Data.Fin.Enum.GFromRep (GHC.Generics.V1 *)
+ Data.Fin.Enum: instance Data.Fin.Enum.GFromRep a => Data.Fin.Enum.GFromRep (GHC.Generics.M1 * d c a)
+ Data.Fin.Enum: instance Data.Fin.Enum.GToRep (GHC.Generics.U1 *)
+ Data.Fin.Enum: instance Data.Fin.Enum.GToRep (GHC.Generics.V1 *)
+ Data.Fin.Enum: instance Data.Fin.Enum.GToRep a => Data.Fin.Enum.GToRep (GHC.Generics.M1 * d c a)
- Data.Fin: [S] :: Fin n -> Fin (S n)
+ Data.Fin: [S] :: Fin n -> Fin ( 'S n)
- Data.Fin: [Z] :: Fin (S n)
+ Data.Fin: [Z] :: Fin ( 'S n)
- Data.Fin: fin0 :: Fin (Plus Nat0 (S n))
+ Data.Fin: fin0 :: Fin (Plus Nat0 ( 'S n))
- Data.Fin: fin1 :: Fin (Plus Nat1 (S n))
+ Data.Fin: fin1 :: Fin (Plus Nat1 ( 'S n))
- Data.Fin: fin2 :: Fin (Plus Nat2 (S n))
+ Data.Fin: fin2 :: Fin (Plus Nat2 ( 'S n))
- Data.Fin: fin3 :: Fin (Plus Nat3 (S n))
+ Data.Fin: fin3 :: Fin (Plus Nat3 ( 'S n))
- Data.Fin: fin4 :: Fin (Plus Nat4 (S n))
+ Data.Fin: fin4 :: Fin (Plus Nat4 ( 'S n))
- Data.Fin: fin5 :: Fin (Plus Nat5 (S n))
+ Data.Fin: fin5 :: Fin (Plus Nat5 ( 'S n))
- Data.Fin: fin6 :: Fin (Plus Nat6 (S n))
+ Data.Fin: fin6 :: Fin (Plus Nat6 ( 'S n))
- Data.Fin: fin7 :: Fin (Plus Nat7 (S n))
+ Data.Fin: fin7 :: Fin (Plus Nat7 ( 'S n))
- Data.Fin: fin8 :: Fin (Plus Nat8 (S n))
+ Data.Fin: fin8 :: Fin (Plus Nat8 ( 'S n))
- Data.Fin: fin9 :: Fin (Plus Nat9 (S n))
+ Data.Fin: fin9 :: Fin (Plus Nat9 ( 'S n))
- Data.Fin: inlineUniverse1 :: InlineInduction n => NonEmpty (Fin (S n))
+ Data.Fin: inlineUniverse1 :: InlineInduction n => NonEmpty (Fin ( 'S n))
- Data.Fin: universe1 :: SNatI n => NonEmpty (Fin (S n))
+ Data.Fin: universe1 :: SNatI n => NonEmpty (Fin ( 'S n))
- Data.Fin.Enum: class Enum a where type EnumSize a :: Nat type EnumSize a = GEnumSize a from = gfrom to = gto where {
+ Data.Fin.Enum: class Enum a where {
- Data.Type.Nat: [SS] :: SNatI n => SNat (S n)
+ Data.Type.Nat: [SS] :: SNatI n => SNat ( 'S n)
- Data.Type.Nat: [SZ] :: SNat Z
+ Data.Type.Nat: [SZ] :: SNat 'Z
- Data.Type.Nat: induction :: forall n f. SNatI n => f Z -> (forall m. SNatI m => f m -> f (S m)) -> f n
+ Data.Type.Nat: induction :: forall n f. SNatI n => f 'Z -> (forall m. SNatI m => f m -> f ( 'S m)) -> f n
- Data.Type.Nat: induction1 :: forall n f a. SNatI n => f Z a -> (forall m. SNatI m => f m a -> f (S m) a) -> f n a
+ Data.Type.Nat: induction1 :: forall n f a. SNatI n => f 'Z a -> (forall m. SNatI m => f m a -> f ( 'S m) a) -> f n a
- Data.Type.Nat: inlineInduction :: forall n f. InlineInduction n => f Z -> (forall m. InlineInduction m => f m -> f (S m)) -> f n
+ Data.Type.Nat: inlineInduction :: forall n f. InlineInduction n => f 'Z -> (forall m. InlineInduction m => f m -> f ( 'S m)) -> f n
- Data.Type.Nat: inlineInduction1 :: InlineInduction n => f Z a -> (forall m. InlineInduction m => f m a -> f (S m) a) -> f n a
+ Data.Type.Nat: inlineInduction1 :: InlineInduction n => f 'Z a -> (forall m. InlineInduction m => f m a -> f ( 'S m) a) -> f n a
- Data.Type.Nat: type Nat0 = Z
+ Data.Type.Nat: type Nat0 = 'Z
- Data.Type.Nat: type Nat1 = S Nat0
+ Data.Type.Nat: type Nat1 = 'S Nat0
- Data.Type.Nat: type Nat2 = S Nat1
+ Data.Type.Nat: type Nat2 = 'S Nat1
- Data.Type.Nat: type Nat3 = S Nat2
+ Data.Type.Nat: type Nat3 = 'S Nat2
- Data.Type.Nat: type Nat4 = S Nat3
+ Data.Type.Nat: type Nat4 = 'S Nat3
- Data.Type.Nat: type Nat5 = S Nat4
+ Data.Type.Nat: type Nat5 = 'S Nat4
- Data.Type.Nat: type Nat6 = S Nat5
+ Data.Type.Nat: type Nat6 = 'S Nat5
- Data.Type.Nat: type Nat7 = S Nat6
+ Data.Type.Nat: type Nat7 = 'S Nat6
- Data.Type.Nat: type Nat8 = S Nat7
+ Data.Type.Nat: type Nat8 = 'S Nat7
- Data.Type.Nat: type Nat9 = S Nat8
+ Data.Type.Nat: type Nat9 = 'S Nat8
Files
- ChangeLog.md +5/−0
- fin.cabal +32/−16
- src/Data/Fin.hs +1/−1
- src/Data/Type/Nat.hs +3/−0
- test/Inspection.hs +17/−0
ChangeLog.md view
@@ -1,4 +1,9 @@ # Revision history for boring++## 0.0.1++- GHC-8.4.1 / base-4.11 support+ ## 0 - First version. Released on an unsuspecting world.
fin.cabal view
@@ -1,34 +1,49 @@ name: fin-version: 0-synopsis: Nat and Fin+version: 0.0.1+synopsis: Nat and Fin: peano naturals and finite numbers description: This package provides two simple types, and some tools to work with them. Also on type level as @DataKinds@. . @+ \-- Peano naturals data Nat = Z | S Nat+ .+ \-- Finite naturals data Fin (n :: Nat) where- Z :: Fin n- S :: Fin n -> Fin ('Nat.S n)+ \ Z :: Fin ('S n)+ \ S :: Fin n -> Fin ('Nat.S n) @ .+ [vec](https://hackage.haskell.org/package/vec) implements length-indexed+ (sized) lists using this package for indexes.+ . The "Data.Fin.Enum" module let's work generically with enumerations. .- Differences to other packages:+ See [Hasochism: the pleasure and pain of dependently typed haskell programming](https://doi.org/10.1145/2503778.2503786)+ by Sam Lindley and Conor McBride for answers to /how/ and /why/.+ Read [APLicative Programming with Naperian Functors](https://doi.org/10.1007/978-3-662-54434-1_21)+ by Jeremy Gibbons for (not so) different ones. .- * [type-natural](http://hackage.haskell.org/package/type-natural) depends- on @singletons@ package. `fin` will try to stay light on the dependencies,+ === Similar packages+ .+ * [finite-typelits](https://hackage.haskell.org/package/finite-typelits)+ . Is a great package, but uses @GHC.TypeLits@.+ .+ * [type-natural](https://hackage.haskell.org/package/type-natural) depends+ on @singletons@ package. @fin@ will try to stay light on the dependencies, and support as many GHC versions as practical. .- * [peano](http://hackage.haskell.org/package/peano) is very incomplete+ * [peano](https://hackage.haskell.org/package/peano) is very incomplete .- * [nat](http://hackage.haskell.org/package/nat) as well.+ * [nat](https://hackage.haskell.org/package/nat) as well. . * [PeanoWitnesses](https://hackage.haskell.org/package/PeanoWitnesses) doesn't use @DataKinds@. .- * [type-combinators](http://hackage.haskell.org/package/type-combinators)+ * [type-combinators](https://hackage.haskell.org/package/type-combinators) is big package too.+ homepage: https://github.com/phadej/vec bug-reports: https://github.com/phadej/vec/issues license: BSD3@@ -44,7 +59,8 @@ GHC==7.8.4, GHC==7.10.3, GHC==8.0.2,- GHC==8.2.1+ GHC==8.2.2,+ GHC==8.4.1 source-repository head type: git@@ -57,17 +73,17 @@ Data.Nat Data.Type.Nat build-depends:- base >=4.7 && <4.11,+ base >=4.7 && <4.12, deepseq >=1.3.0.2 && <1.5,- hashable >=1.2.6.1 && <1.3+ hashable >=1.2.7.0 && <1.3 if !impl(ghc >= 8.0) build-depends:- semigroups >=0.18.3 && <0.18.4+ semigroups >=0.18.4 && <0.19 if !impl(ghc >= 7.10) build-depends:- nats >=1 && <1.2,+ nats >=1.1.2 && <1.2, void >=0.7.2 && <0.8 ghc-options: -Wall -fprint-explicit-kinds@@ -89,7 +105,7 @@ base, fin, tagged,- inspection-testing >= 0.1.2 && <0.2+ inspection-testing >= 0.2.0.1 && <0.3 if !impl(ghc >= 8.0) buildable: False
src/Data/Fin.hs view
@@ -43,7 +43,7 @@ import qualified Data.List.NonEmpty as NE import qualified Data.Type.Nat as N --- | Finite Numbers up to 'n'.+-- | Finite numbers: @[0..n-1]@. data Fin (n :: N.Nat) where Z :: Fin ('N.S n) S :: Fin n -> Fin ('N.S n)
src/Data/Type/Nat.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}@@ -164,7 +165,9 @@ 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 ------------------------------------------------------------------------------- -- Induction
test/Inspection.hs view
@@ -106,6 +106,23 @@ inspect $ 'lhsUnfold === 'rhsUnfold -------------------------------------------------------------------------------+-- Power+-------------------------------------------------------------------------------++power :: forall n. N.InlineInduction n => Proxy n -> Int -> Int+power _ k = unTagged impl where+ impl :: Tagged n Int+ impl = N.inlineInduction1 (Tagged 1) $ \(Tagged rec') -> Tagged (rec' * k)++lhsPower5 :: Int -> Int+lhsPower5 = power (Proxy :: Proxy N.Nat5)++rhsPower5 :: Int -> Int+rhsPower5 k = k * k * k * k * k++inspect $ 'lhsPower5 === 'rhsPower5++------------------------------------------------------------------------------- -- Main to make GHC happy -------------------------------------------------------------------------------