ghc-typelits-natnormalise: GHC typechecker plugin for types of kind GHC.TypeLits.Nat

[ bsd2, library, type-system ] [ Propose Tags ]

A type checker plugin for GHC that can solve equalities and inequalities of types of kind Nat, where these types are either:

It solves these equalities by normalising them to sort-of SOP (Sum-of-Products) form, and then perform a simple syntactic equality.

For example, this solver can prove the equality between:

(x + 2)^(y + 2)

and

4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2

Because the latter is actually the SOP normal form of the former.

To use the plugin, add the

OPTIONS_GHC -fplugin GHC.TypeLits.Normalise

Pragma to the header of your file.


[Skip to Readme]
Versions [RSS] [faq] 0.1, 0.1.1, 0.1.2, 0.2, 0.2.1, 0.3, 0.3.1, 0.4, 0.4.1, 0.4.2, 0.4.3, 0.4.4, 0.4.5, 0.4.6, 0.5, 0.5.1, 0.5.2, 0.5.3, 0.5.4, 0.5.5, 0.5.6, 0.5.7, 0.5.8, 0.5.9, 0.5.10, 0.6, 0.6.1, 0.6.2, 0.7, 0.7.1, 0.7.2, 0.7.3, 0.7.4, 0.7.5, 0.7.6 (info)
Change log CHANGELOG.md
Dependencies base (>=4.9 && <5), containers (>=0.5.7.1 && <0.7), ghc (>=8.0.1 && <9.4), ghc-bignum (>=1.0 && <1.3), ghc-tcplugins-extra (>=0.3.1), integer-gmp (==1.0.*), transformers (>=0.5.2.0 && <0.6) [details]
License BSD-2-Clause
Copyright Copyright © 2015-2016, University of Twente, 2017-2018, QBayLogic B.V.
Author Christiaan Baaij
Maintainer christiaan.baaij@gmail.com
Revised Revision 1 made by QBayLogic at 2022-01-13T12:20:38Z
Category Type System
Home page http://www.clash-lang.org/
Bug tracker http://github.com/clash-lang/ghc-typelits-natnormalise/issues
Source repo head: git clone https://github.com/clash-lang/ghc-typelits-natnormalise.git
Uploaded by ChristiaanBaaij at 2021-06-20T10:55:31Z
Distributions Arch:0.7.6, LTSHaskell:0.7.6, NixOS:0.7.6
Downloads 25168 total (190 in the last 30 days)
Rating 2.25 (votes: 2) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs uploaded by user
Build status unknown [no reports yet]

Modules

[Index] [Quick Jump]

Manual Flags

NameDescriptionDefault
deverror

Enables `-Werror` for development mode and TravisCI

Disabled
Automatic Flags
NameDescriptionDefault

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

For package maintainers and hackage trustees

Candidates


Readme for ghc-typelits-natnormalise-0.7.6

[back to package description]

ghc-typelits-natnormalise

Build Status Hackage Hackage Dependencies

A type checker plugin for GHC that can solve equalities and inequalities of types of kind Nat, where these types are either:

  • Type-level naturals
  • Type variables
  • Applications of the arithmetic expressions (+,-,*,^).

It solves these equalities by normalising them to sort-of SOP (Sum-of-Products) form, and then perform a simple syntactic equality.

For example, this solver can prove the equality between:

(x + 2)^(y + 2)

and

4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2

Because the latter is actually the SOP normal form of the former.

To use the plugin, add

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

To the header of your file.