ghc-typelits-natnormalise-0.4.1: GHC typechecker plugin for types of kind GHC.TypeLits.Nat

Copyright(C) 2015-2016, University of Twente
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellNone
LanguageHaskell2010
Extensions
  • Cpp
  • DisambiguateRecordFields
  • RecordWildCards
  • TupleSections
  • LambdaCase

GHC.TypeLits.Normalise

Description

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.

Synopsis

Documentation

plugin :: Plugin Source

To use the plugin, add

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

To the header of your file.