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

[ bsd2, library, type-system ] [ Propose Tags ] [ Report a vulnerability ]

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:

  1. a matching given KnownNat constraint; or

  2. a corresponding KnownNat<N> instance for the type function

To use the plugin, add the

OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver

Pragma to the header of your file.


[Skip to Readme]

Flags

Manual Flags

NameDescriptionDefault
deverror

Enables `-Werror` for development mode and TravisCI

Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.1, 0.1.1, 0.2, 0.2.1, 0.2.2, 0.2.3, 0.2.4, 0.3, 0.3.1, 0.4, 0.4.1, 0.4.2, 0.5, 0.5.1, 0.6, 0.7, 0.7.1, 0.7.2, 0.7.3, 0.7.4, 0.7.5, 0.7.6, 0.7.7, 0.7.8, 0.7.9, 0.7.10, 0.7.12
Change log CHANGELOG.md
Dependencies base (>=4.9 && <4.10), ghc (>=8.0.1 && <8.2), ghc-tcplugins-extra (>=0.2), ghc-typelits-natnormalise (>=0.5.2 && <0.6), singletons (>=2.2 && <3.0), template-haskell (>=2.11.0.0 && <2.13), transformers (>=0.5.2.0 && <0.6) [details]
License BSD-2-Clause
Copyright Copyright © 2016, University of Twente, 2017 QBayLogic
Author Christiaan Baaij
Maintainer christiaan.baaij@gmail.com
Category Type System
Home page http://clash-lang.org/
Source repo head: git clone https://github.com/clash-lang/ghc-typelits-knownnat.git
Uploaded by ChristiaanBaaij at 2017-04-10T15:36:06Z
Distributions Arch:0.7.8, LTSHaskell:0.7.12, NixOS:0.7.12, Stackage:0.7.12
Reverse Dependencies 32 direct, 31 indirect [details]
Downloads 22081 total (174 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2017-04-10 [all 1 reports]

Readme for ghc-typelits-knownnat-0.2.4

[back to package description]

ghc-typelits-knownnat

Build Status Hackage Hackage Dependencies

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.