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 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 [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 (info)
Change log CHANGELOG.md
Dependencies base (>=4.9 && <5), ghc (>=8.0.1 && <8.6), ghc-tcplugins-extra (>=0.2.5 && <0.3), integer-gmp (==1.0.*) [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 ChristiaanBaaij at Fri May 11 20:43:30 UTC 2018
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 Sun Apr 15 08:35:29 UTC 2018
Distributions Arch:0.6.2, LTSHaskell:0.6.2, NixOS:0.6.2, Stackage:0.6.2
Downloads 8166 total (484 in the last 30 days)
Rating 2.25 (votes: 2) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs uploaded by user
Build status unknown [no reports yet]

Modules

[Index]

Flags

NameDescriptionDefaultType
deverror

Enables -Werror for development mode and TravisCI

DisabledManual

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


Readme for ghc-typelits-natnormalise-0.5.10

[back to package description]

ghc-typelits-natnormalise

Build Status Hackage Hackage Dependencies

A type checker plugin for GHC that can solve equalities 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.