ghc-typelits-knownnat-0.7.9: Derive KnownNat constraints from other KnownNat constraints

Copyright | (C) 2016 University of Twente 2017-2018 QBayLogic B.V. 2017 Google Inc.
License | BSD2 (see the file LICENSE)
Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com>
Safe Haskell | Trustworthy
Language | Haskell2010

Extensions

- Cpp
- ViewPatterns
- TupleSections
- LambdaCase

GHC.TypeLits.KnownNat.Solver

Description

A type checker plugin for GHC that can derive "complex" `KnownNat` constraints from other simple/variable `KnownNat` constraints. i.e. without this plugin, you must have both a `KnownNat n` and a `KnownNat (n+2)` constraint in the type signature of the following function:

    f :: forall n . (KnownNat n, KnownNat (n+2)) => Proxy n -> Integer
    f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))

Using the plugin you can omit the `KnownNat (n+2)` constraint:

    f :: forall n . KnownNat n => Proxy n -> Integer
    f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))

The plugin can derive `KnownNat` constraints for types consisting of:

- Type variables, when there is a corresponding `KnownNat` constraint
- Type-level naturals
- Applications of the arithmetic expression: `{+,-,*,^}`
- Type functions, when there is either:
- a matching given `KnownNat` constraint; or
- a corresponding `KnownNat<N>` instance for the type function

To elaborate the latter points, given the type family `Min`:

    type family Min (a :: Nat) (b :: Nat) :: Nat where
      Min 0 b = 0
      Min a b = If (a <=? b) a b

the plugin can derive a `KnownNat (Min x y + 1)` constraint given only a `KnownNat (Min x y)` constraint:

    g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer
    g _ _ = natVal (Proxy :: Proxy (Min x y + 1))

And, given the type family `Max`:

    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max 0 b = b
      Max a b = If (a <=? b) b a

and corresponding `KnownNat2` instance:

    instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where
      natSing2 = let x = natVal (Proxy a)
                     y = natVal (Proxy b)
                     z = max x y
                 in  SNatKn z
      {-# INLINE natSing2 #-}

the plugin can derive a `KnownNat (Max x y + 1)` constraint given only a `KnownNat x` and `KnownNat y` constraint:

    h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer
    h _ _ = natVal (Proxy :: Proxy (Max x y + 1))

To use the plugin, add the

    OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver

Pragma to the header of your file.

Synopsis

- plugin :: Plugin

# Documentation

plugin :: Plugin Source #

A type checker plugin for GHC that can derive "complex" `KnownNat` constraints from other simple/variable `KnownNat` constraints. i.e. without this plugin, you must have both a `KnownNat n` and a `KnownNat (n+2)` constraint in the type signature of the following function:

    f :: forall n . (KnownNat n, KnownNat (n+2)) => Proxy n -> Integer
    f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))

Using the plugin you can omit the `KnownNat (n+2)` constraint:

    f :: forall n . KnownNat n => Proxy n -> Integer
    f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))

The plugin can derive `KnownNat` constraints for types consisting of:

- Type variables, when there is a corresponding `KnownNat` constraint
- Type-level naturals
- Applications of the arithmetic expression: `{+,-,*,^}`
- Type functions, when there is either:
- a matching given `KnownNat` constraint; or
- a corresponding `KnownNat<N>` instance for the type function

To elaborate the latter points, given the type family `Min`:

    type family Min (a :: Nat) (b :: Nat) :: Nat where
      Min 0 b = 0
      Min a b = If (a <=? b) a b

the plugin can derive a `KnownNat (Min x y + 1)` constraint given only a `KnownNat (Min x y)` constraint:

    g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer
    g _ _ = natVal (Proxy :: Proxy (Min x y + 1))

And, given the type family `Max`:

    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max 0 b = b
      Max a b = If (a <=? b) b a

    $(genDefunSymbols [''Max]) -- creates the MaxSym0 symbol

and corresponding `KnownNat2` instance:

    instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where
      type KnownNatF2 "TestFunctions.Max" = MaxSym0
      natSing2 = let x = natVal (Proxy  a)
                     y = natVal (Proxy  b)
                     z = max x y
                 in  SNatKn z
      {-# INLINE natSing2 #-}

the plugin can derive a `KnownNat (Max x y + 1)` constraint given only a `KnownNat x` and `KnownNat y` constraint:

    h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer
    h _ _ = natVal (Proxy :: Proxy (Max x y + 1))

To use the plugin, add the

    OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver

Pragma to the header of your file.