fin-0.3: fin.cabal
cabal-version: >=1.10
name: fin
version: 0.3
synopsis: Nat and Fin: peano naturals and finite numbers
category: Data, Dependent Types, Singletons, Math
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 <oleg.grenrus@iki.fi>
maintainer: Oleg.Grenrus <oleg.grenrus@iki.fi>
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.4
|| ==8.10.7
|| ==9.0.2
|| ==9.2.7
|| ==9.4.4
|| ==9.6.1
source-repository head
type: git
location: https://github.com/phadej/vec.git
subdir: fin
library
default-language: Haskell2010
ghc-options: -Wall -fprint-explicit-kinds
hs-source-dirs: src
exposed-modules:
Data.Fin
Data.Nat
Data.Type.Nat
Data.Type.Nat.LE
Data.Type.Nat.LE.ReflStep
Data.Type.Nat.LT
other-modules: TrustworthyCompat
build-depends:
base >=4.7 && <4.19
, 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.4 && <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
if !impl(ghc >=7.10)
build-depends:
nats >=1.1.2 && <1.2
, void >=0.7.3 && <0.8
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
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.6
, tagged
if !impl(ghc >=8.0)
buildable: False