singleton-typelits: Singletons and induction over GHC TypeLits

[ bsd3, data, library ] [ Propose Tags ]

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.

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.0.0.0, 0.1.0.0
Dependencies base (>=4.9 && <4.12) [details]
License BSD-3-Clause
Author mniip
Maintainer mniip@mniip.com
Category Data
Home page https://github.com/mniip/singleton-typelits
Uploaded by mniip at 2018-07-11T18:33:20Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 1324 total (9 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2018-07-11 [all 1 reports]