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 GHC.TypeLits.Nat, where these types are either:

It solves these equalities by normalising them to sort-of GHC.TypeLits.Normalise.SOP.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 GHC.TypeLits.Normalise.SOP.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 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 (info)
Change log CHANGELOG.md
Dependencies base (>=4.8 && <5), ghc (>=7.10 && <7.12) [details]
License BSD-2-Clause
Copyright Copyright © 2015 University of Twente
Author Christiaan Baaij
Maintainer christiaan.baaij@gmail.com
Category Type System
Home page http://www.clash-lang.org/
Bug tracker http://github.com/christiaanb/ghc-typelits-natnormalise/issues
Source repo head: git clone https://github.com/christiaanb/ghc-typelits-natnormalise.git
Uploaded by ChristiaanBaaij at Mon Mar 30 11:49:00 UTC 2015
Distributions LTSHaskell:0.5.10, NixOS:0.6.1, Stackage:0.6.1, openSUSE:0.5.10
Downloads 5891 total (140 in the last 30 days)
Rating 2.25 (votes: 2) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2015-10-09 [all 3 reports]
Hackage Matrix CI

Modules

[Index]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for ghc-typelits-natnormalise-0.1

[back to package description]

ghc-tynat-normalise

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.