ghc-typelits-natnormalise

GHC typechecker plugin for types of kind GHC.TypeLits.Nat

http://www.clash-lang.org/

Version on this page:0.3
LTS Haskell 22.14:0.7.9
Stackage Nightly 2024-03-28:0.7.9
Latest on Hackage:0.7.9

See all snapshots ghc-typelits-natnormalise appears in

BSD-2-Clause licensed by Christiaan Baaij
Maintained by [email protected]
This version can be pinned in stack with:ghc-typelits-natnormalise-0.3@sha256:b37ecee475e69dc1685c16d0ddf37283500072be9373a94a6f427ddd55df74ba,2570

Module documentation for 0.3

Used by 2 packages in nightly-2015-08-26(full list with versions):

ghc-tynat-normalise

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.

Changes

Changelog for the ghc-typelits-natnormalise package

0.3 June 3rd 2015

  • Find more unifications:
    • <TyApp xs> + x ~ 2 + x ==> [<TyApp xs> ~ 2]
  • Fixes bugs:
    • Unifying a*b ~ b now returns [a ~ 1]; before it erroneously returned [a ~ ], which is interpred as [a ~ 0]
    • Unifying a+b ~ b now returns [a ~ 0]; before it returned the undesirable, though equal, [a ~ ]

0.2.1 May 6th 2015

  • Update Eq instance of SOP: Empty SOP is equal to 0

0.2 April 22nd 2015

  • Finds more unifications:
    • (2 + a) ~ 5 ==> [a := 3]
    • (3 * a) ~ 0 ==> [a := 0]

0.1.2 April 21st 2015

  • Don’t simplify expressions with negative exponents

0.1.1 April 17th 2015

0.1 March 30th 2015

  • Initial release