ghc-typelits-natnormalise-0.7.4: GHC typechecker plugin for types of kind GHC.TypeLits.Nat
Copyright (C) 2015-2016 University of Twente2017 QBayLogic B.V. BSD2 (see the file LICENSE) Christiaan Baaij None Haskell2010 CppDisambiguateRecordFieldsRecordWildCardsRecordPunsViewPatternsTupleSectionsLambdaCase

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.

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


## Treating subtraction as addition with a negated number

{-# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers #-}


to the header of your file, thereby allowing to use associativity and commutativity rules when proving constraints involving subtractions. Note that this option can lead to unsound behaviour and should be handled with extreme care.

### When it leads to unsound behaviour

For example, enabling the allow-negated-numbers feature would allow you to prove:

(n - 1) + 1 ~ n


without a (1 <= n) constraint, even though when n is set to 0 the subtraction n-1 would be locally negative and hence not be a natural number.

This would allow the following erroneous definition:

data Fin (n :: Nat) where
FZ :: Fin (n + 1)
FS :: Fin n -> Fin (n + 1)

f :: forall n . Natural -> Fin n
f n = case of
0 -> FZ
x -> FS (f @(n-1) (x - 1))

fs :: [Fin 0]
fs = f <\$> [0..]


### When it might be Okay

This example is taken from the mezzo library.

When you have:

-- | Singleton type for the number of repetitions of an element.
data Times (n :: Nat) where
T :: Times n

-- | An element of a "run-length encoded" vector, containing the value and
-- the number of repetitions
data Elem :: Type -> Nat -> Type where
(:*) :: t -> Times n -> Elem t n

-- | A length-indexed vector, optimised for repetitions.
data OptVector :: Type -> Nat -> Type where
End  :: OptVector t 0
(:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n


And you want to define:

-- | Append two optimised vectors.
type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where
ys        ++ End = ys
End       ++ ys = ys
(x :- xs) ++ ys = x :- (xs ++ ys)


then the last line will give rise to the constraint:

(n-l)+m ~ (n+m)-l


because:

x  :: Elem t l
xs :: OptVector t (n-l)
ys :: OptVector t m


In this case it's okay to add

{-# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers #-}


if you can convince yourself you will never be able to construct a:

xs :: OptVector t (n-l)


where n-l is a negative number.

Synopsis

# Documentation

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