ghc-typelits-natnormalise

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

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

LTS Haskell 22.42:0.7.10
Stackage Nightly 2024-11-24:0.7.10
Latest on Hackage:0.7.10

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.7.10@sha256:8e519fe832b4ff5bb7f9348d79c2850799cffe58db6ff175d7c0997f07b30313,3979

Module documentation for 0.7.10

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.

Changes

Changelog for the ghc-typelits-natnormalise package

0.7.10 May 22nd 2024

  • Support for GHC 9.10.1

0.7.9 October 10th 2023

  • Support for GHC 9.8.1

0.7.8 February 20th 2023

  • Try and outright solve substituted constraints, the same as is done with the unsubstituted constraint. Partially Fixes #65.
  • Support for GHC-9.6.0.20230210

0.7.7 October 10th 2022

0.7.6 June 20th 2021

0.7.5 June 17th 2021

  • Fixes #52 Plugin doesn’t solve inside arbitrary class constraints
  • Build on GHC 9.2.0.20210422

0.7.4 February 12th 2021

  • Fixes #50 x ^ C ~ y erroneously deemed hard insoluable, a contradiction, when C is some type family other than +,-,*,^

0.7.3 January 1st 2021

  • Build on GHC 9.0.1-rc1

0.7.2 March 9 2020

  • Fixes #44 infinite loop due to boxed equality

0.7.1 February 6th 2020

  • Add support for GHC 8.10.1-alpha2
  • Fixes #23: Can’t figure out + commutes in some contexts on GHC 8.6.3
  • Fixes #28: Using the solver seems to break GHC
  • Fixes #34: inequality solver mishandles subtraction

0.7 August 26th 2019

  • Require KnownNat constraints when solving with constants

0.6.2 July 10th 2018

  • Add support for GHC 8.6.1-alpha1
  • Solve larger inequalities from smaller inequalities, e.g.
    • a <= n implies a <= n + 1

0.6.1 May 9th 2018

  • Stop solving x + y ~ a + b by asking GHC to solve x ~ a and y ~ b as this leads to a situation where we find a solution that is not the most general.
  • Stop using the smallest solution to an inequality to solve an equality, as this leads to finding solutions that are not the most general.
  • Solve smaller inequalities from larger inequalities, e.g.
    • 1 <= 2*x implies 1 <= x
    • x + 2 <= y implies x <= y and 2 <= y

0.6 April 23rd 2018

  • Solving constraints with a-b will emit b <= a constraints. e.g. solving n-1+1 ~ n will emit a 1 <= n constraint.
    • If you need subtraction to be treated as addition with a negated operarand run with -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers, and the b <= a constraint won’t be emitted. Note that doing so can lead to unsound behaviour.
  • Try to solve equalities using smallest solution of inequalities:
    • Solve x + 1 ~ y using 1 <= y => x + 1 ~ 1 => x ~ 0
  • Solve inequalities using simple transitivity rules:
    • 2 <= x implies 1 <= x
    • x <= 9 implies x <= 10
  • Solve inequalities using simple monotonicity of addition rules:
    • 2 <= x implies 2 + 2*x <= 3*x
  • Solve inequalities using simple monotonicity of multiplication rules:
    • 1 <= x implies 1 <= 3*x
  • Solve inequalities using simple monotonicity of exponentiation rules:
    • 1 <= x implies 2 <= 2^x
  • Solve inequalities using powers of 2 and monotonicity of exponentiation:
    • 2 <= x implies 2^(2 + 2*x) <= 2^(3*x)

0.5.10 April 15th 2018

  • Add support for GHC 8.5.20180306

0.5.9 March 17th 2018

  • Add support for GHC 8.4.1

0.5.8 January 4th 2018

  • Add support for GHC 8.4.1-alpha1

0.5.7 November 7th 2017

  • Solve inequalities such as: 1 <= a + 3

0.5.6 October 31st 2017

  • Fixes bugs:
    • (x + 1) ~ (2 * y) no longer implies ((2 * (y - 1)) + 1) ~ x

0.5.5 October 22nd 2017

  • Solve inequalities when their normal forms are the same, i.e.
    • (2 <= (2 ^ (n + d))) implies (2 <= (2 ^ (d + n)))
  • Find more unifications:
    • 8^x - 2*4^x ~ 8^y - 2*4^y ==> [x := y]

0.5.4 October 14th 2017

  • Perform normalisations such as: 2^x * 4^x ==> 8^x

0.5.3 May 15th 2017

  • Add support for GHC 8.2

0.5.2 January 15th 2017

  • Fixes bugs:
    • Reification from SOP to Type sometimes loses product terms

0.5.1 September 29th 2016

  • Fixes bugs:
    • Cannot solve an equality for the second time in a definition group

0.5 August 17th 2016

  • Solve simple inequalities, i.e.:
    • a <= a + 1
    • 2a <= 3a
    • 1 <= a^b

0.4.6 July 21th 2016

  • Reduce “x^(-y) * x^y” to 1
  • Fixes bugs:
    • Subtraction in exponent induces infinite loop

0.4.5 July 20th 2016

  • Fixes bugs:
    • Reifying negative exponent causes GHC panic

0.4.4 July 19th 2016

  • Fixes bugs:
    • Rounding error in logBase calculation

0.4.3 July 18th 2016

  • Fixes bugs:
    • False positive: “f :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)”

0.4.2 July 8th 2016

  • Find more unifications:
    • (2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]
    • a^d * a^e ~ a^c ==> [c := d + e]
    • x+5 ~ y ==> [x := y - 5], but only when x+5 ~ y is a given constraint

0.4.1 February 4th 2016

  • Find more unifications:
    • F x y k z ~ F x y (k-1+1) z ==> [k := k], where F can be any type function

0.4 January 19th 2016

  • Stop using ‘provenance’ hack to create conditional evidence (GHC 8.0+ only)
  • Find more unifications:
    • F x + 2 - 1 - 1 ~ F x ==> [F x := F x], where F can be any type function with result Nat.

0.3.2

  • Find more unifications:
    • (z ^ a) ~ (z ^ b) ==> [a := b]
    • (i ^ a) ~ j ==> [a := round (logBase i j)], when i and j are integers, and ceiling (logBase i j) == floor (logBase i j).

0.3.1 October 19th 2015

  • Find more unifications:
    • (i * a) ~ j ==> [a := div j i], when i and j are integers, and mod j i == 0.
    • (i * a) + j ~ k ==> [a := div (k-j) i], when i, j, and k are integers, and k-j >= 0 and mod (k-j) i == 0.

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