diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,11 @@ +Version 0.2.3.0 +=============== + + + +* Added the `GHC.TypeLits.Compare` module for refining bounds and proving + inequalities on `KnownNat`s and associated utility functions. + Version 0.2.2.0 =============== diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,11 +1,11 @@ typelits-witnesses ================== -[![typelits-witnesses on Stackage LTS 2](http://stackage.org/package/typelits-witnesses/badge/lts-2)](http://stackage.org/lts-2/package/typelits-witnesses) -[![typelits-witnesses on Stackage LTS 3](http://stackage.org/package/typelits-witnesses/badge/lts-3)](http://stackage.org/lts-3/package/typelits-witnesses) -[![typelits-witnesses on Stackage LTS 4](http://stackage.org/package/typelits-witnesses/badge/lts-4)](http://stackage.org/lts-4/package/typelits-witnesses) +[![typelits-witnesses on Hackage](https://img.shields.io/hackage/v/lens.svg?maxAge=2592000)](https://hackage.haskell.org/package/typelits-witnesses) [![typelits-witnesses on Stackage LTS](http://stackage.org/package/typelits-witnesses/badge/lts)](http://stackage.org/lts/package/typelits-witnesses) [![typelits-witnesses on Stackage Nightly](http://stackage.org/package/typelits-witnesses/badge/nightly)](http://stackage.org/nightly/package/typelits-witnesses) +[![Build +Status](https://travis-ci.org/mstksg/typelits-witnesses.svg?branch=master)](https://travis-ci.org/mstksg/typelits-witnesses) Provides witnesses for `KnownNat` and `KnownSymbol` instances for various @@ -21,6 +21,16 @@ able to apply analogies of `natVal`/`symbolVal` to lists with analogies for `SomeNat` and `SomeSymbol`. +Note that most of the functionality in this library can be reproduced in a more +generic way using the great [singletons][] library. The versions here are +provided as a "plumbing included" alternative that makes some commonly found +design patterns involving GHC's TypeLits functionality a little smoother, +especially when working with external libraries or GHC TypeLit's `Nat` +comparison API. + +[singletons]: https://hackage.haskell.org/package/singletons + + `GHC.TypeLits.Witnesses` ------------------------ @@ -83,6 +93,65 @@ There are more advanced operations dealing with low-level machinery, as well, in the module. See module documentation for more detail. + +`GHC.TypeLits.Compare` +---------------------- + +Provides tools for refining upper and lower bounds on `KnownNat`s and proving +inequalities involving *GHC.TypeLits*'s comparison API. (Both with `<=?` and +`CmpNat`). + +If a library function requires `1 <= n` constraint, but only `KnownNat n` is +available: + +~~~haskell +foo :: (KnownNat n, 1 <= n) => Proxy n -> Int + +bar :: KnownNat n => Proxy n -> Int +bar n = case (Proxy :: Proxy 1) %<=? n of + LE Refl -> foo n + NLE _ -> 0 +~~~ + +`foo` requires that `1 <= n`, but `bar` has to handle all cases of `n`. `%<=?` +lets you compare the `KnownNat`s in two `Proxy`s and returns a `:<=?`, which +has two constructors, `LE` and `NLE`. + +If you pattern match on the result, in the `LE` branch, the constraint +`1 <= n` will be satisfied according to GHC, so `bar` can safely call +`foo`, and GHC will recognize that `1 <= n`. + +In the `NLE` branch, the constraint that `1 > n` is satisfied, so any +functions that require that constraint would be callable. + +For convenience, `isLE` and `isNLE` are also offered: + +~~~haskell +bar :: KnownNat n => Proxy n -> Int +bar n = case isLE (Proxy :: Proxy 1) n of + Just Refl -> foo n + Nothing -> 0 +~~~ + +Similarly, if a library function requires something involving `CmpNat`, +you can use `cmpNat` and the `SCmpNat` type: + +~~~haskell +foo1 :: (KnownNat n, CmpNat 5 n ~ LT) => Proxy n -> Int +foo2 :: (KnownNat n, CmpNat 5 n ~ GT) => Proxy n -> Int + +bar :: KnownNat n => Proxy n -> Int +bar n = case cmpNat (Proxy :: Proxy 5) n of + CLT Refl -> foo1 n + CEQ Refl -> 0 + CGT Refl -> foo2 n +~~~ + +You can use the `Refl` that `cmpNat` gives you with `flipCmpNat` and +`cmpNatLE` to "flip" the inequality or turn it into something compatible +with `<=?` (useful for when you have to work with libraries that mix the +two methods) or `cmpNatEq` and `eqCmpNat` to get to/from witnesses for +equality of the two `Nat`s. `GHC.TypeLits.List` ------------------- diff --git a/src/GHC/TypeLits/Compare.hs b/src/GHC/TypeLits/Compare.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/Compare.hs @@ -0,0 +1,159 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +-- | +-- Module : GHC.TypeLits.Compare +-- Description : Tools and singletons for proving and refining inequalities +-- and bounds on GHC TypeLits types using '<=' and '<=?' +-- Copyright : (c) Justin Le 2016 +-- License : MIT +-- Maintainer : justin@jle.im +-- Stability : unstable +-- Portability : non-portable +-- +-- +-- This module provides the ability to refine given 'KnownNat' instances +-- using "GHC.TypeLits"'s comparison API, and also the ability to prove +-- inequalities and upper/lower limits. +-- +-- If a library function requires @1 '<=' n@ constraint, but only +-- @'KnownNat' n@ is available: +-- +-- @ +-- foo :: (KnownNat n, 1 '<=' n) => 'Proxy' n -> Int +-- +-- bar :: KnownNat n => Proxy n -> Int +-- bar n = case (Proxy :: Proxy 1) '%<=?' n of +-- 'LE' 'Refl' -> foo n +-- 'NLE' _ -> 0 +-- @ +-- +-- @foo@ requires that @1 <= n@, but @bar@ has to handle all cases of @n@. +-- @%<=?@ lets you compare the 'KnownNat's in two 'Proxy's and returns +-- a @:<=?@, which has two constructors, 'LE' and 'NLE'. +-- +-- If you pattern match on the result, in the 'LE' branch, the constraint +-- @1 <= n@ will be satisfied according to GHC, so @bar@ can safely call +-- @foo@, and GHC will recognize that @1 <= n@. +-- +-- In the 'NLE' branch, the constraint that @1 > n@ is satisfied, so any +-- functions that require that constraint would be callable. +-- +-- For convenience, 'isLE' and 'isNLE' are also offered: +-- +-- @ +-- bar :: KnownNat n => Proxy n -> Int +-- bar n = case 'isLE' (Proxy :: Proxy 1) n of +-- 'Just' Refl -> foo n +-- 'Nothing' -> 0 +-- @ +-- +-- Similarly, if a library function requires something involving 'CmpNat', +-- you can use 'cmpNat' and the 'SCmpNat' type: +-- +-- @ +-- foo1 :: (KnownNat n, 'CmpNat' 5 n ~ LT) => Proxy n -> Int +-- foo2 :: (KnownNat n, CmpNat 5 n ~ GT) => Proxy n -> Int +-- +-- bar :: KnownNat n => Proxy n -> Int +-- bar n = case 'cmpNat' (Proxy :: Proxy 5) n of +-- 'CLT' Refl -> foo1 n +-- 'CEQ' Refl -> 0 +-- 'CGT' Refl -> foo2 n +-- @ +-- +-- You can use the 'Refl' that 'cmpNat' gives you with 'flipCmpNat' and +-- 'cmpNatLE' to "flip" the inequality or turn it into something compatible +-- with '<=?' (useful for when you have to work with libraries that mix the +-- two methods) or 'cmpNatEq' and 'eqCmpNat' to get to/from witnesses for +-- equality of the two 'Nat's. + +module GHC.TypeLits.Compare + ( -- * '<=' and '<=?' + (:<=?)(..) + , (%<=?) + -- ** Convenience functions + , isLE + , isNLE + -- * 'CmpNat' + , SCmpNat(..) + , cmpNat + -- ** Manipulating witnesses + , flipCmpNat + , cmpNatEq + , eqCmpNat + -- ** Interfacing with '<=?' + , cmpNatLE + ) + where + +import Data.Type.Equality +import Data.Proxy +import GHC.TypeLits +import Unsafe.Coerce + +isLE + :: (KnownNat m, KnownNat n) + => Proxy m + -> Proxy n + -> Maybe ((m <=? n) :~: 'True) +isLE m n = case m %<=? n of + LE Refl -> Just Refl + NLE _ -> Nothing + +isNLE + :: (KnownNat m, KnownNat n) + => Proxy m + -> Proxy n + -> Maybe ((m <=? n) :~: 'False) +isNLE m n = case m %<=? n of + NLE Refl -> Just Refl + LE _ -> Nothing + +data (:<=?) :: Nat -> Nat -> * where + LE :: ((m <=? n) :~: 'True) -> (m :<=? n) + NLE :: ((m <=? n) :~: 'False) -> (m :<=? n) + +(%<=?) + :: (KnownNat m, KnownNat n) + => Proxy m + -> Proxy n + -> (m :<=? n) +m %<=? n | natVal m <= natVal n = LE (unsafeCoerce Refl) + | otherwise = NLE (unsafeCoerce Refl) + +data SCmpNat :: Nat -> Nat -> * where + CLT :: (CmpNat m n :~: 'LT) -> SCmpNat m n + CEQ :: (CmpNat m n :~: 'EQ) -> SCmpNat m n + CGT :: (CmpNat m n :~: 'GT) -> SCmpNat m n + +cmpNat + :: (KnownNat m, KnownNat n) + => Proxy m + -> Proxy n + -> SCmpNat m n +cmpNat m n = case compare (natVal m) (natVal n) of + LT -> CLT (unsafeCoerce Refl) + EQ -> CEQ (unsafeCoerce Refl) + GT -> CGT (unsafeCoerce Refl) + +flipCmpNat :: SCmpNat m n -> SCmpNat n m +flipCmpNat = \case CLT Refl -> CGT (unsafeCoerce Refl) + CEQ Refl -> CEQ (unsafeCoerce Refl) + CGT Refl -> CLT (unsafeCoerce Refl) + +cmpNatEq :: (CmpNat m n :~: 'EQ) -> (m :~: n) +cmpNatEq = \case Refl -> unsafeCoerce Refl + +eqCmpNat :: (m :~: n) -> (CmpNat m n :~: 'EQ) +eqCmpNat = \case Refl -> unsafeCoerce Refl + +cmpNatLE :: SCmpNat m n -> (m :<=? n) +cmpNatLE = \case CLT Refl -> LE (unsafeCoerce Refl) + CEQ Refl -> LE (unsafeCoerce Refl) + CGT Refl -> NLE (unsafeCoerce Refl) diff --git a/src/GHC/TypeLits/List.hs b/src/GHC/TypeLits/List.hs --- a/src/GHC/TypeLits/List.hs +++ b/src/GHC/TypeLits/List.hs @@ -172,6 +172,8 @@ -- | The "eliminator" for 'NatList'. You can think of this as -- a dependently typed analogy for a fold. +-- +-- /Since 0.2.1.0/ elimNatList :: forall p ns. () => p '[] @@ -385,6 +387,8 @@ -- | The "eliminator" for 'SymbolList'. You can think of this as -- a dependently typed analogy for a fold. +-- +-- /Since 0.2.1.0/ elimSymbolList :: forall p ss. () => p '[] diff --git a/typelits-witnesses.cabal b/typelits-witnesses.cabal --- a/typelits-witnesses.cabal +++ b/typelits-witnesses.cabal @@ -1,5 +1,5 @@ name: typelits-witnesses -version: 0.2.2.0 +version: 0.2.3.0 synopsis: Existential witnesses, singletons, and classes for operations on GHC TypeLits description: Provides witnesses for 'KnownNat' and 'KnownSymbol' instances for various operations on GHC TypeLits - in @@ -9,7 +9,9 @@ . This is useful for situations where you have @'KnownNat' n@, and you want to prove to GHC - @'KnownNat' (n + 3)@, or @'KnownNat' (2*n + 4)@. + @'KnownNat' (n + 3)@, or @'KnownNat' (2*n + 4)@, or when + constraints on the lower or upper limits of @n@ are + needed. . It's also useful for when you want to work with type level lists of 'KnownNat' or 'KnownSymbol' instances and @@ -17,6 +19,15 @@ analogies of 'natVal' and 'symbolVal' to lists with analogies for 'SomeNat' and 'SomeSymbol'. . + Note that most of the functionality in this library can + be reproduced in a more generic way using the great + + library. The versions here are provided as a "plumbing + included" alternative that makes some commonly found + design patterns involving GHC's TypeLits functionality a + little smoother, especially when working with external + libraries or GHC TypeLit's Nat comparison API. + . See README for more information. homepage: https://github.com/mstksg/typelits-witnesses license: MIT @@ -37,6 +48,7 @@ library exposed-modules: GHC.TypeLits.Witnesses GHC.TypeLits.List + GHC.TypeLits.Compare -- other-modules: -- other-extensions: build-depends: base >=4.7 && <5