The ghc-typelits-knownnat package

[ Tags: bsd2, library, type-system ] [ Propose Tags ]

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:

  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]

Properties

Versions 0.1, 0.1.1, 0.2, 0.2.1, 0.2.2, 0.2.3, 0.2.4, 0.3, 0.3.1
Change log CHANGELOG.md
Dependencies base (>=4.9 && <5), ghc (>=8.0.1 && <8.4), ghc-tcplugins-extra (>=0.2), ghc-typelits-natnormalise (>=0.5.2 && <0.6), singletons (>=2.2 && <2.4), template-haskell (>=2.11.0.0 && <2.13), transformers (>=0.5.2.0 && <0.6) [details]
License BSD2
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 repository head: git clone https://github.com/clash-lang/ghc-typelits-knownnat.git
Uploaded Thu Aug 17 09:25:44 UTC 2017 by ChristiaanBaaij
Distributions LTSHaskell:0.3.1, NixOS:0.3.1, Stackage:0.3.1, Tumbleweed:0.2.4
Downloads 1239 total (356 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2017-08-17 [all 1 reports]
Hackage Matrix CI

Modules

[Index]

Flags

NameDescriptionDefaultType
deverror

Enables -Werror for development mode and TravisCI

DisabledManual

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

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for ghc-typelits-knownnat-0.3.1

[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.