name:                singleton-typelits
version:             0.1.0.0
synopsis:            Singletons and induction over GHC TypeLits
description:
  Singletons and induction schemes over 'GHC.TypeLits.Nat'.
  .
  While the TypeLits interface provided by GHC does allow case-analysing the
  values of the naturals ('GHC.TypeLits.natVal'), it does not facilitate writing
  type-safe programs involving that AP, if one were to write:
  .
  > case natVal (x :: Proxy n) of 0 -> foo x
  .
  In the RHS of this pattern match @n@ is equal to @0@ but this isn't something
  GHC can reason about, as this is an ordinary pattern match on an 'Integer'.
  If the type of @foo@ was @Proxy 0 -> ...@ this wouldn't typecheck and one
  would have to resort to @unsafeCoerce@. In order to make GHC infer something
  like this, @natVal@ needs to return a GADT that includes proofs about the
  natural number it refers to, such that when pattern matching on that GADT the
  proofs become available to the typechecker.
  .
  This package provides a handful of variants of such GADTs for overcoming this
  type of issue, as well as functions to do typesafe induction on naturals
  without resorting to manual GADT unpacking. The most basic form of induction -
  Peano-style induction (P(0) and P(n) implies P(n + 1)) can be inefficient in
  practice on large numbers, so this package also provides more efficient binary
  and arbitrary-base induction schemes.
homepage:            https://github.com/mniip/singleton-typelits
license:             BSD3
license-file:        LICENSE
author:              mniip
maintainer:          mniip@mniip.com
category:            Data
build-type:          Simple
cabal-version:       >=1.10

library
  exposed-modules:     GHC.TypeLits.Singletons, GHC.TypeLits.Induction
  build-depends:       base >=4.9 && <4.12
  default-language:    Haskell2010