41 lines
1.9 KiB
Text
41 lines
1.9 KiB
Text
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.21
|
|
default-language: Haskell2010
|
|
if impl(ghc >= 8.6.1)
|
|
default-extensions: NoStarIsType
|