lean-peano (empty) → 0.1.0.0

raw patch · 9 files changed

+575/−0 lines, 9 filesdep +QuickCheckdep +basedep +base-compatbuild-type:Customsetup-changed

Dependencies added: QuickCheck, base, base-compat, deepseq, doctest, hedgehog, lean-peano, template-haskell

Files

ChangeLog.md +3/−0
LICENSE +30/−0
README.md +1/−0
Setup.hs +7/−0
doctest/doctests.hs +14/−0
lean-peano.cabal +73/−0
src/Numeric/Peano.hs +246/−0
src/Numeric/Peano/Typelevel.hs +91/−0
test/Spec.hs +110/−0

+ ChangeLog.md view

@@ -0,0 +1,3 @@+# Changelog for lean-peano++## Unreleased changes

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright Author name here (c) 2020++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Author name here nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,1 @@+# lean-peano

+ Setup.hs view

@@ -0,0 +1,7 @@+{-# LANGUAGE CPP #-}+{-# OPTIONS_GHC -Wall #-}+module Main (main) where++import Distribution.Extra.Doctest ( defaultMainWithDoctests )+main :: IO ()+main = defaultMainWithDoctests "doctests"

+ doctest/doctests.hs view

@@ -0,0 +1,14 @@+module Main where++import Build_doctests (flags, pkgs, module_sources)+import Data.Foldable (traverse_)+import System.Environment.Compat (unsetEnv)+import Test.DocTest (doctest)++main :: IO ()+main = do+    traverse_ putStrLn args+    unsetEnv "GHC_ENVIRONMENT"+    doctest args+  where+    args = flags ++ pkgs ++ module_sources

+ lean-peano.cabal view

@@ -0,0 +1,73 @@+cabal-version: >= 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 64e91e616abbba7139ad4f000d8a6a1505b2a315175f0489493a319d6a76ac89++name:           lean-peano+version:        0.1.0.0+description:    Please see the README on GitHub at <https://github.com/githubuser/lean-peano#readme>+homepage:       https://github.com/oisdk/lean-peano#readme+bug-reports:    https://github.com/oisdk/lean-peano/issues+author:         Donnacha Oisín Kidney+maintainer:     mail@doisinkidney.com+copyright:      2020 Donnacha Oisín Kidney+license:        MIT+license-file:   LICENSE+build-type:     Custom+extra-source-files:+    README.md+    ChangeLog.md++source-repository head+  type: git+  location: https://github.com/oisdk/lean-peano++custom-setup+  setup-depends:+      base+    , Cabal+    , cabal-doctest  >=1.0.6 && <1.1++library+  exposed-modules:+      Numeric.Peano+      Numeric.Peano.Typelevel+  hs-source-dirs:+      src+  ghc-options: -Wall -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns -fwarn-redundant-constraints -Wcompat+  build-depends:+      base >=4.7 && <5+    , deepseq+  default-language: Haskell2010++test-suite doctests+  type: exitcode-stdio-1.0+  main-is: doctests.hs+  hs-source-dirs:+      doctest+  ghc-options: -Wall -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns -fwarn-redundant-constraints -Wcompat -threaded+  build-depends:+      QuickCheck+    , base+    , base-compat+    , deepseq+    , doctest+    , lean-peano+    , template-haskell+  default-language: Haskell2010++test-suite lean-peano-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  hs-source-dirs:+      test+  ghc-options: -Wall -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns -fwarn-redundant-constraints -Wcompat -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base+    , deepseq+    , hedgehog+    , lean-peano+  default-language: Haskell2010

+ src/Numeric/Peano.hs view

@@ -0,0 +1,246 @@+{-# LANGUAGE BangPatterns         #-}+{-# LANGUAGE DeriveDataTypeable   #-}+{-# LANGUAGE DeriveGeneric        #-}++-- | Peano numerals. Effort is made to make them as efficient as+-- possible, and as lazy as possible, but they are many orders of+-- magnitude less efficient than machine integers. They are primarily+-- used for type-level programming, and occasionally for calculations+-- which can be short-circuited.+--+-- For instance, to check if two lists are the same length, you could+-- write:+--+-- @+-- 'length' xs == 'length' ys+-- @+--+-- But this unnecessarily traverses both lists. The more efficient+-- version, on the other hand, is less clear:+--+-- @+-- sameLength [] [] = True+-- sameLength (_:xs) (_:ys) = sameLength xs ys+-- sameLength _ _ = False+-- @+--+-- Using @'Data.List.genericLength'@, on the other hand, the laziness of+-- @'Nat'@ will indeed short-circuit:+--+-- >>> genericLength [1,2,3] == genericLength [1..]+-- False+module Numeric.Peano where++import           Data.List                   (unfoldr)++import           Control.DeepSeq             (NFData (rnf))++import           Data.Data                   (Data, Typeable)+import           GHC.Generics                (Generic)++import           Numeric.Natural++import           Data.Ix++import           Data.Function+import           Text.Read++-- $setup+-- >>> import Test.QuickCheck+-- >>> import Data.List (genericLength)+-- >>> default (Nat)+-- >>> :{+-- instance Arbitrary Nat where+--     arbitrary = fmap (fromInteger . getNonNegative) arbitrary+-- :}++-- | Peano numbers. Care is taken to make operations as lazy as+-- possible:+--+-- >>> 1 > S (S undefined)+-- False+-- >>> Z > undefined+-- False+-- >>> 3 + undefined >= 3+-- True+data Nat+    = Z+    | S Nat+    deriving (Eq,Generic,Data,Typeable)++foldrNat :: (a -> a) -> a -> Nat -> a+foldrNat f k = go+  where+    go Z     = k+    go (S n) = f (go n)+{-# INLINE foldrNat #-}++foldlNat :: (a -> a) -> a -> Nat -> a+foldlNat f = go+  where+    go !b Z = b+    go !b (S n) = go (f b) n+{-# INLINE foldlNat #-}++-- | As lazy as possible+instance Ord Nat where+    compare Z Z         = EQ+    compare (S n) (S m) = compare n m+    compare Z (S _)     = LT+    compare (S _) Z     = GT++    Z   <= _   = True+    S _ <= Z   = False+    S n <= S m = n <= m++    _ < Z = False+    n < S m = n <= m++    (>=) = flip (<=)+    (>) = flip (<)++    min Z _ = Z+    min _ Z = Z+    min (S n) (S m) = S (min n m)++    max Z m = m+    max n Z = n+    max (S n) (S m) = S (max n m)++-- | Subtraction stops at zero.+--+-- prop> n >= m ==> m - n == Z+instance Num Nat where+    n + m = foldrNat S m n+    n * m = foldrNat (m+) Z n+    abs = id+    signum Z = Z+    signum (S _) = S Z+    fromInteger n+        | n < 0 = error "cannot convert negative integers to Peano numbers"+        | otherwise = go n where+            go 0 = Z+            go m = S (go (m-1))+    n   - Z   = n+    S n - S m = n - m+    Z   - S _ = Z++-- | The maximum bound here is infinity.+--+-- prop> maxBound > (n :: Nat)+instance Bounded Nat where+    minBound = Z+    maxBound = fix S++-- | Shows integer representation.+instance Show Nat where+    showsPrec n = showsPrec n . toInteger++-- | Reads the integer representation.+instance Read Nat where+    readPrec = fmap (fromIntegral :: Natural -> Nat) readPrec++-- | Will obviously diverge for values like `maxBound`.+instance NFData Nat where+    rnf Z     = ()+    rnf (S n) = rnf n++instance Real Nat where+    toRational = toRational . toInteger++-- | Uses custom 'enumFrom', 'enumFromThen', 'enumFromThenTo' to avoid+-- expensive conversions to and from 'Int'.+--+-- >>> [1..3]+-- [1,2,3]+-- >>> [1..1]+-- [1]+-- >>> [2..1]+-- []+-- >>> take 3 [1,2..]+-- [1,2,3]+-- >>> take 3 [5,4..]+-- [5,4,3]+-- >>> [1,3..7]+-- [1,3,5,7]+-- >>> [5,4..1]+-- [5,4,3,2,1]+-- >>> [5,3..1]+-- [5,3,1]+instance Enum Nat where+    succ = S+    pred (S n) = n+    pred Z = error "pred called on zero nat"+    fromEnum = foldlNat succ 0+    toEnum m+      | m < 0 = error "cannot convert negative number to Peano"+      | otherwise = go m+      where+        go 0 = Z+        go n = S (go (n - 1))+    enumFrom = iterate S+    enumFromTo n m = unfoldr f (n, S m - n)+      where+        f (_,Z) = Nothing+        f (e,S l) = Just (e, (S e, l))+    enumFromThen n m = iterate t n+      where+        ts Z mm = (+) mm+        ts (S nn) (S mm) = ts nn mm+        ts nn Z = subtract nn+        t = ts n m+    enumFromThenTo n m t = unfoldr f (n, jm)+      where+        ts (S nn) (S mm) = ts nn mm+        ts Z mm = (S t - n, (+) mm, mm)+        ts nn Z = (S n - t, subtract nn, nn)+        (jm,tf,tt) = ts n m+        td = subtract tt+        f (_,Z) = Nothing+        f (e,l@(S _)) = Just (e, (tf e, td l))+++-- | Errors on zero.+--+-- >>> 5 `div` 2+-- 2+instance Integral Nat where+    toInteger = foldlNat succ 0+    quotRem _ Z = (maxBound, error "divide by zero")+    quotRem x y = qr Z x y+      where+        qr q n m = go n m+          where+            go nn Z          = qr (S q) nn m+            go (S nn) (S mm) = go nn mm+            go Z (S _)       = (q, n)+    quot n m = go n where+      go = subt m where+        subt Z nn          = S (go nn)+        subt (S mm) (S nn) = subt mm nn+        subt (S _) Z       = Z+    rem _ Z = error "divide by zero"+    rem nn mm = r nn mm where+      r n m = go n m where+        go nnn Z           = r nnn m+        go (S nnn) (S mmm) = go nnn mmm+        go Z (S _)         = n+    div = quot+    mod = rem+    divMod = quotRem++instance Ix Nat where+    range = uncurry enumFromTo+    inRange = uncurry go where+      go (S _) _ Z         = False+      go Z y x             = x <= y+      go (S x) (S y) (S z) = go x y z+      go (S _) Z (S _)     = False+    index = uncurry go where+      go Z h i             = lim 0 h i+      go (S _) _ Z         = error "out of range"+      go (S l) (S h) (S i) = go l h i+      go (S _) Z (S _)     = error "out of range"+      lim _ Z (S _)      = error "out of range"+      lim !a (S n) (S m) = lim (a + 1) n m+      lim !a _ Z         = a

+ src/Numeric/Peano/Typelevel.hs view

@@ -0,0 +1,91 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE KindSignatures       #-}+{-# LANGUAGE NoStarIsType         #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}++module Numeric.Peano.Typelevel where++import           GHC.TypeLits  (ErrorMessage (..), TypeError)+import qualified GHC.TypeLits  as Lit+import           Numeric.Peano++type family (==) (n :: Nat) (m :: Nat) :: Bool where+    Z == Z = True+    S n == S m = n == m+    Z == S _ = False+    S _ == Z = False++type family FromLit (n :: Lit.Nat) :: Nat where+    FromLit 0 = Z+    FromLit n = FromLit2 (Lit.Mod n 2) (FromLit (Lit.Div n 2))++type family FromLit2 (odd :: Lit.Nat) (rest :: Nat) :: Nat where+    FromLit2 0 n = n+    FromLit2 1 n = S n++type family ToLit (n :: Nat) :: Lit.Nat where+    ToLit Z = 0+    ToLit (S n) = 1 Lit.+ (ToLit n)++type family Compare (n :: Nat) (m :: Nat) :: Ordering where+    Compare Z Z         = EQ+    Compare (S n) (S m) = Compare n m+    Compare Z (S _)     = LT+    Compare (S _) Z     = GT++type family (<=) (n :: Nat) (m :: Nat) :: Bool where+    Z   <= _   = True+    S _ <= Z   = False+    S n <= S m = n <= m++type family (<) (n :: Nat) (m :: Nat) :: Bool where+    _ < Z = False+    n < S m = n <= m++type family Min (n :: Nat) (m :: Nat) :: Nat where+    Min Z _ = Z+    Min _ Z = Z+    Min (S n) (S m) = S (Min n m)++type family Max (n :: Nat) (m :: Nat) :: Nat where+    Max Z m = m+    Max n Z = n+    Max (S n) (S m) = S (Max n m)++infixl 6 ++type family (+) (n :: Nat) (m :: Nat) :: Nat where+    Z + m = m+    S n + m = S (n + m)++infixl 7 *+type family (*) (n :: Nat) (m :: Nat) :: Nat where+    Z   * _ = Z+    S n * m = m + n * m++infixl 6 -+type family (-) (n :: Nat) (m :: Nat) :: Nat where+    n   - Z   = n+    S n - S m = n - m+    Z   - S _ = Z++type family (%) (n :: Nat) (m :: Nat) :: Nat where+    _ % Z = TypeError (Text "divide by zero")+    n % m = Rem' n m n m++type family Rem' (n :: Nat) (m :: Nat) (n' :: Nat) (m' :: Nat) :: Nat where+    Rem' n m n' Z = Rem' n' m n' m+    Rem' n m (S n') (S m') = Rem' n m n' m'+    Rem' n m Z (S _) = n++type family (/) (n :: Nat) (m :: Nat) :: Nat where+    _ / Z = TypeError (Text "divide by zero")+    n / m = Div' m n m++type family Div' (m :: Nat) (n' :: Nat) (m' :: Nat) :: Nat where+    Div' m n' Z = S (Div' m n' m)+    Div' m (S n') (S m') = Div' m n' m'+    Div' m Z (S _) = Z

+ test/Spec.hs view

@@ -0,0 +1,110 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell     #-}+{-# LANGUAGE TypeApplications    #-}++import           Hedgehog+import qualified Hedgehog.Gen        as Gen+import qualified Hedgehog.Range      as Range++import           Numeric.Peano++import           Control.Monad+import           Data.Ix++binaryProp+    :: forall a.+       Integral a+    => (forall t. Integral t => t -> t -> t)+    -> Integer+    -> Integer+    -> (Integer -> Integer -> Bool)+    -> Property+binaryProp op lb ub cond = property $ do+    x <- forAll (Gen.integral (Range.linear lb ub))+    y <- forAll (Gen.integral (Range.linear lb ub))+    guard (cond x y)+    let zb = op x y+    let zt = op (fromInteger @a x) (fromInteger y)+    zb === toInteger zt++holdsForLength :: Foldable f => (a -> Bool) -> f a -> Int+holdsForLength p = flip (foldr f id) 0 where+  f e a i | p e = a (i + 1)+          | otherwise = i++enumProps+    :: forall a.+       (Enum a, Show a, Ord a)+    => (Int -> Bool) -> Gen Int -> Gen a -> Property+enumProps p ig eg = property $ do+    x <- forAll ig+    annotate "from . to"+    (fromEnum . toEnum @a) x === x+    annotate "to . from"+    n <- forAll eg+    (toEnum . fromEnum) n === n+    annotate "[n..]"+    let lhs1 = take 100 $ map fromEnum [n..]+        rhs1 = take 100 [fromEnum n..]+        len1 = min (holdsForLength p lhs1) (holdsForLength p rhs1)+    take len1 lhs1 === take len1 rhs1+    annotate "[n,m..]"+    m <- forAll eg+    let lhs2 = take 100 $ map fromEnum [n,m..]+        rhs2 = take 100 [fromEnum n, fromEnum m..]+        len2 = min (holdsForLength p lhs2) (holdsForLength p rhs2)+    take len2 lhs2 === take len2 rhs2+    when (m >= n) $ do+        annotate "[n..m]"+        map fromEnum [n..m] === [fromEnum n..fromEnum m]+    l <- forAll eg+    when (((l > n) == (n > m)) && (l /= n)) $ do+        annotate "[l,n..m]"+        map fromEnum [l,n..m] === [fromEnum l, fromEnum n..fromEnum m]+++prop_PeanoAdd :: Property+prop_PeanoAdd = binaryProp @Nat (+) 0 1000 (\_ _ -> True)++prop_PeanoMul :: Property+prop_PeanoMul = binaryProp @Nat (*) 0 1000 (\_ _ -> True)++prop_PeanoSub :: Property+prop_PeanoSub = withDiscards 1000 $ binaryProp @Nat (-) 0 1000 (>=)++prop_PeanoRem :: Property+prop_PeanoRem = binaryProp @Nat rem 0 1000 (\_ y -> y > 0)++prop_PeanoQuot :: Property+prop_PeanoQuot = binaryProp @Nat quot 0 1000 (\_ y -> y > 0)++-- prop_PeanoOrd :: Property+-- prop_PeanoOrd = property $ ord (Gen.integral (Range.linear @Nat 0 1000))(\n -> Gen.integral (Range.linear n (n+5)))++prop_PeanoEnum :: Property+prop_PeanoEnum =+    enumProps+        (>= 0)+        (Gen.integral (Range.linear 0 1000))+        (Gen.integral (Range.linear @Nat 0 1000))++prop_PeanoInRange :: Property+prop_PeanoInRange = property $ do+    l <- forAll (Gen.integral (Range.linear Z 100))+    u <- forAll (Gen.integral (Range.linear l (l+100)))+    i <- forAll (Gen.integral (Range.linear 0 300))+    inRange (l,u) i === (l <= i &&  i <= u)++prop_PeanoIndex :: Property+prop_PeanoIndex = property $ do+    l <- forAll (Gen.integral (Range.linear Z 100))+    u <- forAll (Gen.integral (Range.linear l (l+100)))+    i <- forAll (Gen.integral (Range.linear l u))+    unless (inRange (l,u) i) discard+    index (l,u) i === fromEnum (i - l)++main :: IO Bool+main = checkParallel $$(discover)