ghc-typelits-knownnat: Derive KnownNat constraints from other KnownNat constraints
This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.
Warnings:
- 'ghc-options: -O0' is not needed. Use the --disable-optimization configure flag.
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
KnownNatconstraintType-level naturals
Applications of the arithmetic expression: +,-,*,^
Type functions, when there is either:
a matching given
KnownNatconstraint; ora 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, 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.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 && <5), ghc (>=8.0.1 && <8.11), ghc-prim (>=0.4.0.0 && <0.7), ghc-tcplugins-extra (>=0.3.1), ghc-typelits-natnormalise (>=0.7.1 && <0.8), template-haskell (>=2.11.0.0 && <2.17), transformers (>=0.5.2.0 && <0.6) [details] |
| License | BSD-2-Clause |
| Copyright | Copyright © 2016 , University of Twente, 2017-2018, QBayLogic B.V., 2017 , Google Inc. |
| 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 2020-02-06T13:22:21Z |
Modules
[Index] [Quick Jump]
Flags
Manual Flags
| Name | Description | Default |
|---|---|---|
| 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
- ghc-typelits-knownnat-0.7.2.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
Package maintainers
For package maintainers and hackage trustees
Readme for ghc-typelits-knownnat-0.7.2
[back to package description]ghc-typelits-knownnat
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
KnownNatconstraint - Type-level naturals
- Applications of the arithmetic expression:
{+,-,*,^} - Type functions, when there is either:
- a matching given
KnownNatconstraint; or - a corresponding
KnownNat<N>instance for the type function
- a matching given
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.