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:

  • 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 the

OPTIONS_GHC -fplugin GHC.TypeLits.Normalise

Pragma to the header of your file.


[Skip to Readme]

Flags

Manual Flags

NameDescriptionDefault
deverror

Enables `-Werror` for development mode and TravisCI

Disabled

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

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 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, 0.7.7, 0.7.8, 0.7.9, 0.7.10 (info)
Change log CHANGELOG.md
Dependencies base (>=4.9 && <5), containers (>=0.5.7.1 && <0.8), ghc (>=8.0.1 && <9.12), ghc-bignum (>=1.0 && <1.4), ghc-tcplugins-extra (>=0.3.1), integer-gmp (>=1.0 && <1.1), template-haskell (>=2.17 && <2.23), transformers (>=0.5.2.0 && <0.7) [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
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 2024-05-22T14:22:36Z
Distributions Arch:0.7.8, LTSHaskell:0.7.10, NixOS:0.7.10, Stackage:0.7.10
Reverse Dependencies 32 direct, 48 indirect [details]
Downloads 30354 total (237 in the last 30 days)
Rating 2.5 (votes: 3) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2024-05-22 [all 1 reports]

Readme for ghc-typelits-natnormalise-0.7.10

[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.