fin-0.1: fin.cabal
cabal-version: >=1.10
name: fin
version: 0.1
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 <oleg.grenrus@iki.fi>
maintainer: Oleg.Grenrus <oleg.grenrus@iki.fi>
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: