cabal-version: >=1.10 name: fin version: 0.0.3 synopsis: Nat and Fin: peano naturals and finite numbers category: Data, Dependent Types, Singletons 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 ('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. . 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. . === 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](https://hackage.haskell.org/package/peano) is very incomplete . * [nat](https://hackage.haskell.org/package/nat) as well. . * [PeanoWitnesses](https://hackage.haskell.org/package/PeanoWitnesses) doesn't use @DataKinds@. . * [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 license-file: LICENSE author: Oleg Grenrus maintainer: Oleg.Grenrus copyright: (c) 2017-2019 Oleg Grenrus build-type: Simple extra-source-files: ChangeLog.md tested-with: GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4 source-repository head type: git location: https://github.com/phadej/vec.git library 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.13 , dec >=0.0.3 && <0.1 , deepseq >=1.3.0.2 && <1.5 , hashable >=1.2.7.0 && <1.4 if !impl(ghc >=8.2) build-depends: bifunctors >=5.5.3 && <5.6 if !impl(ghc >=8.0) build-depends: semigroups >=0.18.4 && <0.20 if !impl(ghc >=7.10) build-depends: nats >=1.1.2 && <1.2 , void >=0.7.2 && <0.8 ghc-options: -Wall -fprint-explicit-kinds hs-source-dirs: src default-language: Haskell2010 -- dump-core -- if impl(ghc >= 8.0) -- build-depends: dump-core -- ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html test-suite inspection type: exitcode-stdio-1.0 main-is: Inspection.hs ghc-options: -Wall -fprint-explicit-kinds hs-source-dirs: test default-language: Haskell2010 build-depends: base , fin , inspection-testing >=0.2.0.1 && <0.5 , tagged if !impl(ghc >=8.0) buildable: False -- useful for development ghc-options: