typelits-witnesses 0.2.2.0 → 0.2.3.0

raw patch · 5 files changed

+257/−5 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• README.md +72/−3
• src/GHC/TypeLits/Compare.hs +159/−0
• src/GHC/TypeLits/List.hs +4/−0
• typelits-witnesses.cabal +14/−2

@@ -1,3 +1,11 @@+Version 0.2.3.0+===============++<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.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 =============== 

@@ -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` -------------------

@@ -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)

@@ -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 '[]

@@ -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+                     <https://hackage.haskell.org/package/singletons 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.+                     .                      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