cabal-version:      2.2
name:               fin
version:            0.3.1
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:            BSD-3-Clause
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 ==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
  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

  -- GHC boot libs
  build-depends:
    , base     >=4.12.0.0 && <4.21
    , deepseq  >=1.4.4.0  && <1.6

  -- other dependencies
  build-depends:
    , boring         ^>=0.2.2
    , dec            ^>=0.0.6
    , hashable       ^>=1.4.4.0
    , QuickCheck     ^>=2.14.2  || ^>=2.15
    , some           ^>=1.0.6
    , universe-base  ^>=1.1.4

  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
--  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