BSD-2-Clause licensed by Christiaan Baaij
This version can be pinned in stack with:ghc-typelits-natnormalise-0.4.1@sha256:ab6dcd5bc7287adcd78a6c46c2c4dfa8ea73924410fb30f55e064cae370a18fb,2968
Module documentation for 0.4.1
ghc-typelits-natnormalise
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.
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