fin 0.1.1 → 0.2

raw patch · 11 files changed

+255/−151 lines, 11 filesdep +universe-basedep ~basedep ~decdep ~semigroupsPVP ok

version bump matches the API change (PVP)

Dependencies added: universe-base

Dependency ranges changed: base, dec, semigroups, void

API changes (from Hackage documentation)

Files

• ChangeLog.md +10/−1
• fin.cabal +21/−13
• src/Data/Fin.hs +52/−22
• src/Data/Fin/Enum.hs +14/−7
• src/Data/Nat.hs +48/−3
• src/Data/Type/Nat.hs +58/−93
• src/Data/Type/Nat/LE.hs +5/−1
• src/Data/Type/Nat/LE/ReflStep.hs +15/−6
• src/Data/Type/Nat/LT.hs +4/−0
• src/TrustworthyCompat.hs +9/−0
• test/Inspection.hs +19/−5

@@ -1,4 +1,13 @@-# Revision history for fin+## 0.2++- `SNat` is now what was called `InlineInduction`.+  To migrate code from `fin-0.1` to `fin-0.2` it's often enough to+  replace `InlineInduction` with `SNatI`, and `inlineInduction` with `induction`. +- Explicitly mark all modules as Safe or Trustworthy.++## 0.1.2++- Add `universe-base` `Universe` and `Finite` instances  ## 0.1.1 

@@ -1,6 +1,6 @@ cabal-version:      >=1.10 name:               fin-version:            0.1.1+version:            0.2 synopsis:           Nat and Fin: peano naturals and finite numbers category:           Data, Dependent Types, Singletons, Math description:@@ -52,7 +52,7 @@ license-file:       LICENSE author:             Oleg Grenrus <oleg.grenrus@iki.fi> maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>-copyright:          (c) 2017-2019 Oleg Grenrus+copyright:          (c) 2017-2021 Oleg Grenrus build-type:         Simple extra-source-files: ChangeLog.md tested-with:@@ -62,7 +62,9 @@    || ==8.2.2    || ==8.4.4    || ==8.6.5-   || ==8.8.1+   || ==8.8.4+   || ==8.10.4+   || ==9.0.1  source-repository head   type:     git@@ -70,6 +72,9 @@   subdir:   fin  library+  default-language: Haskell2010+  ghc-options:      -Wall -fprint-explicit-kinds+  hs-source-dirs:   src   exposed-modules:     Data.Fin     Data.Fin.Enum@@ -79,27 +84,30 @@     Data.Type.Nat.LE.ReflStep     Data.Type.Nat.LT +  other-modules:    TrustworthyCompat   build-depends:-      base        >=4.7     && <4.14-    , dec         >=0.0.3   && <0.1-    , deepseq     >=1.3.0.2 && <1.5-    , hashable    >=1.2.7.0 && <1.4-    , QuickCheck  >=2.13.2  && <2.14+      base           >=4.7     && <4.16+    , dec            >=0.0.4   && <0.1+    , deepseq        >=1.3.0.2 && <1.5+    , hashable       >=1.2.7.0 && <1.4+    , QuickCheck     >=2.13.2  && <2.15+    , universe-base  >=1.1.2   && <1.2    if !impl(ghc >=8.2)     build-depends: bifunctors >=5.5.3 && <5.6    if !impl(ghc >=8.0)-    build-depends: semigroups >=0.18.4 && <0.20+    build-depends: semigroups >=0.18.5 && <0.20    if !impl(ghc >=7.10)     build-depends:         nats  >=1.1.2 && <1.2-      , void  >=0.7.2 && <0.8+      , void  >=0.7.3 && <0.8 -  ghc-options:      -Wall -fprint-explicit-kinds-  hs-source-dirs:   src-  default-language: Haskell2010+  if impl(ghc >=9.0)+    -- these flags may abort compilation with GHC-8.10+    -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295+    ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode  -- dump-core -- if impl(ghc >= 8.0)

@@ -3,6 +3,7 @@ {-# LANGUAGE EmptyCase            #-} {-# LANGUAGE GADTs                #-} {-# LANGUAGE KindSignatures       #-}+{-# LANGUAGE Safe                 #-} {-# LANGUAGE ScopedTypeVariables  #-} {-# LANGUAGE StandaloneDeriving   #-} {-# LANGUAGE TypeOperators        #-}@@ -60,10 +61,20 @@ import GHC.Exception      (ArithException (..), throw) import Numeric.Natural    (Natural) -import qualified Data.List.NonEmpty as NE-import qualified Data.Type.Nat      as N-import qualified Test.QuickCheck    as QC+import qualified Data.List.NonEmpty    as NE+import qualified Data.Type.Nat         as N+import qualified Data.Universe.Class   as U+import qualified Data.Universe.Helpers as U+import qualified Test.QuickCheck       as QC +-- $setup+-- >>> import Data.List (genericLength)+-- >>> import Data.List.NonEmpty (NonEmpty (..))+-- >>> import Numeric.Natural (Natural)+-- >>> import qualified Data.Type.Nat as N+-- >>> import qualified Data.Universe.Class as U+-- >>> import qualified Data.Universe.Helpers as U+ ------------------------------------------------------------------------------- -- Type -------------------------------------------------------------------------------@@ -143,14 +154,14 @@ -- -- @since 0.1.1 ---mirror :: forall n. N.InlineInduction n => Fin n -> Fin n-mirror = getMirror (N.inlineInduction start step) where+mirror :: forall n. N.SNatI n => Fin n -> Fin n+mirror = getMirror (N.induction start step) where     start :: Mirror 'Z     start = Mirror id -    step :: forall m. N.InlineInduction m => Mirror m -> Mirror ('S m)+    step :: forall m. N.SNatI m => Mirror m -> Mirror ('S m)     step (Mirror rec) = Mirror $ \n -> case n of-        FZ   -> getMaxBound (N.inlineInduction (MaxBound FZ) (MaxBound . FS . getMaxBound))+        FZ   -> getMaxBound (N.induction (MaxBound FZ) (MaxBound . FS . getMaxBound))         FS m -> weakenLeft1 (rec m)  newtype Mirror n = Mirror { getMirror :: Fin n -> Fin n }@@ -235,6 +246,25 @@ -- newtype Fun b m = Fun { getFun :: (Fin ('S m) -> b) -> Fin ('S m) QC.:-> b }  -------------------------------------------------------------------------------+-- universe-base+-------------------------------------------------------------------------------++-- | @since 0.1.2+instance N.SNatI n => U.Universe (Fin n) where+    universe = universe++-- |+--+-- >>> (U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))+-- True+--+-- @since 0.1.2+--+instance N.SNatI n => U.Finite   (Fin n) where+    universeF   = U.universe+    cardinality = U.Tagged $ N.reflectToNum (Proxy :: Proxy n)++------------------------------------------------------------------------------- -- Showing ------------------------------------------------------------------------------- @@ -338,15 +368,15 @@ -- -- >>> inlineUniverse :: [Fin N.Nat3] -- [0,1,2]-inlineUniverse :: N.InlineInduction n => [Fin n]-inlineUniverse = getUniverse $ N.inlineInduction (Universe []) step where+inlineUniverse :: N.SNatI n => [Fin n]+inlineUniverse = getUniverse $ N.induction (Universe []) step where     step :: Universe n -> Universe ('S n)     step (Universe xs) = Universe (FZ : map FS xs)  -- | >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3) -- 0 :| [1,2]-inlineUniverse1 :: N.InlineInduction n => NonEmpty (Fin ('S n))-inlineUniverse1 = getUniverse1 $ N.inlineInduction (Universe1 (FZ :| [])) step where+inlineUniverse1 :: N.SNatI n => NonEmpty (Fin ('S n))+inlineUniverse1 = getUniverse1 $ N.induction (Universe1 (FZ :| [])) step where     step :: Universe1 n -> Universe1 ('S n)     step (Universe1 xs) = Universe1 (NE.cons FZ (fmap FS xs)) @@ -392,8 +422,8 @@ -- -- @since 0.1.1 ---isMax :: forall n. N.InlineInduction n => Fin ('S n) -> Maybe (Fin n)-isMax = getIsMax (N.inlineInduction start step) where+isMax :: forall n. N.SNatI n => Fin ('S n) -> Maybe (Fin n)+isMax = getIsMax (N.induction start step) where     start :: IsMax 'Z     start = IsMax $ \_ -> Nothing @@ -419,8 +449,8 @@ -- [0,1,2,3] -- -- @since 0.1.1-weakenLeft1 :: N.InlineInduction n => Fin n -> Fin ('S n)-weakenLeft1 = getWeaken1 (N.inlineInduction start step) where+weakenLeft1 :: N.SNatI n => Fin n -> Fin ('S n)+weakenLeft1 = getWeaken1 (N.induction start step) where     start :: Weaken1 'Z     start = Weaken1 absurd @@ -433,8 +463,8 @@  -- | >>> map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3]) -- [0,1,2]-weakenLeft :: forall n m. N.InlineInduction n => Proxy m -> Fin n -> Fin (N.Plus n m)-weakenLeft _ = getWeakenLeft (N.inlineInduction start step :: WeakenLeft m n) where+weakenLeft :: forall n m. N.SNatI n => Proxy m -> Fin n -> Fin (N.Plus n m)+weakenLeft _ = getWeakenLeft (N.induction start step :: WeakenLeft m n) where     start :: WeakenLeft m 'Z     start = WeakenLeft absurd @@ -447,8 +477,8 @@  -- | >>> map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3]) -- [2,3,4]-weakenRight :: forall n m. N.InlineInduction n => Proxy n -> Fin m -> Fin (N.Plus n m)-weakenRight _ = getWeakenRight (N.inlineInduction start step :: WeakenRight m n) where+weakenRight :: forall n m. N.SNatI n => Proxy n -> Fin m -> Fin (N.Plus n m)+weakenRight _ = getWeakenRight (N.induction start step :: WeakenRight m n) where     start = WeakenRight id     step (WeakenRight go) = WeakenRight $ \x -> FS $ go x @@ -462,7 +492,7 @@ -- >>> append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4)) -- 7 ---append :: forall n m. N.InlineInduction n => Either (Fin n) (Fin m) -> Fin (N.Plus n m)+append :: forall n m. N.SNatI n => Either (Fin n) (Fin m) -> Fin (N.Plus n m) append (Left n)  = weakenLeft (Proxy :: Proxy m) n append (Right m) = weakenRight (Proxy :: Proxy n) m @@ -477,8 +507,8 @@ -- >>> map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)] -- [Left 0,Left 1,Right 0,Right 1,Right 2] ---split :: forall n m. N.InlineInduction n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)-split = getSplit (N.inlineInduction start step) where+split :: forall n m. N.SNatI n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)+split = getSplit (N.induction start step) where     start :: Split m 'Z     start = Split Right 

@@ -1,10 +1,12 @@ {-# LANGUAGE ConstraintKinds       #-} {-# LANGUAGE DataKinds             #-} {-# LANGUAGE DefaultSignatures     #-}+{-# LANGUAGE EmptyCase             #-} {-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE Safe                  #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE TypeFamilies          #-} {-# LANGUAGE TypeOperators         #-}@@ -31,13 +33,16 @@ import Data.Fin       (Fin (..)) import Data.Nat       (Nat (..)) import Data.Proxy     (Proxy (..))-import GHC.Generics   ((:+:) (..), M1 (..), U1 (..), V1)+import GHC.Generics   (M1 (..), U1 (..), V1, (:+:) (..))  import qualified Data.Fin      as F import qualified Data.Type.Nat as N import qualified Data.Void     as V import qualified GHC.Generics  as G +-- $setup+-- >>> import qualified Data.Fin as F+ -- | Generic enumerations. -- -- /Examples:/@@ -89,7 +94,7 @@ instance Enum Ordering  -- | 'Either' ~ @+@-instance (Enum a, Enum b, N.InlineInduction (EnumSize a)) => Enum (Either a b) where+instance (Enum a, Enum b, N.SNatI (EnumSize a)) => Enum (Either a b) where     type EnumSize (Either a b) = N.Plus (EnumSize a) (EnumSize b)      to   = bimap to to . F.split@@ -115,17 +120,19 @@  -- | Generic version of 'from'. gfrom :: (G.Generic a, GFrom a) => a -> Fin (GEnumSize a)-gfrom = \x -> gfromRep (G.from x) (error "gfrom: internal error" :: Fin N.Nat0)+gfrom = \x -> gfromRep (G.from x) (Proxy :: Proxy N.Nat0)  -- | Constraint for the class that computes 'gfrom'. type GFrom a = GFromRep (G.Rep a)  class GFromRep (a :: * -> *)  where-    gfromRep  :: a x     -> Fin n -> Fin (EnumSizeRep a n)-    gfromSkip :: Proxy a -> Fin n -> Fin (EnumSizeRep a n)+    gfromRep  :: a x     -> Proxy n -> Fin (EnumSizeRep a n)+    gfromSkip :: Proxy a -> Fin n   -> Fin (EnumSizeRep a n)  instance (GFromRep a, GFromRep b) => GFromRep (a :+: b) where-    gfromRep (L1 a) n = gfromRep a (gfromSkip (Proxy :: Proxy b) n)+    gfromRep (L1 a) n = gfromRep a (prSkip n) where+        prSkip :: Proxy n -> Proxy (EnumSizeRep b n)+        prSkip  _ = Proxy     gfromRep (R1 b) n = gfromSkip (Proxy :: Proxy a) (gfromRep b n)      gfromSkip _ n = gfromSkip (Proxy :: Proxy a) (gfromSkip (Proxy :: Proxy b) n)@@ -135,7 +142,7 @@     gfromSkip _     n = gfromSkip (Proxy :: Proxy a) n  instance GFromRep V1 where-    gfromRep  _ n = n+    gfromRep  v _ = case v of {}     gfromSkip _ n = n  instance GFromRep U1 where

@@ -1,5 +1,6 @@ {-# LANGUAGE CPP                #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE Safe               #-}  #if __GLASGOW_HASKELL__ < 710 {-# LANGUAGE DataKinds          #-}@@ -29,8 +30,11 @@ import GHC.Exception   (ArithException (..), throw) import Numeric.Natural (Natural) -import qualified Test.QuickCheck as QC+import qualified Data.Universe.Class as U+import qualified Test.QuickCheck     as QC +-- $setup+ ------------------------------------------------------------------------------- -- Nat -------------------------------------------------------------------------------@@ -39,7 +43,7 @@ -- -- Better than GHC's built-in 'GHC.TypeLits.Nat' for some use cases. ---data Nat = Z | S Nat deriving (Eq, Ord, Typeable, Data)+data Nat = Z | S Nat deriving (Eq, Typeable, Data)  #if __GLASGOW_HASKELL__ < 710 deriving instance Typeable 'Z@@ -53,6 +57,32 @@ instance Show Nat where     showsPrec d = showsPrec d . toNatural +instance Ord Nat where+    compare Z     Z     = EQ+    compare Z     (S _) = LT+    compare (S _) Z     = GT+    compare (S n) (S m) = compare n m++    Z   < Z   = False+    Z   < S _ = True+    S _ < Z   = False+    S n < S m = n < m++    Z   <= Z   = True+    Z   <= S _ = True+    S _ <= Z   = False+    S n <= S m = n <= m++    min Z     Z     = Z+    min Z     (S _) = Z+    min (S _) Z     = Z+    min (S n) (S m) = S (min n m)++    max Z       Z       = Z+    max Z       m@(S _) = m+    max n@(S _) Z       = n+    max (S n)   (S m)   = S (max n m)+ instance Num Nat where     fromInteger = fromNatural . fromInteger @@ -114,11 +144,26 @@     shrink (S n) = n : QC.shrink n  instance QC.CoArbitrary Nat where-    coarbitrary Z     = QC.variant (0 :: Int) +    coarbitrary Z     = QC.variant (0 :: Int)     coarbitrary (S n) = QC.variant (1 :: Int) . QC.coarbitrary n  instance QC.Function Nat where     function = QC.functionIntegral++-------------------------------------------------------------------------------+-- universe-base+-------------------------------------------------------------------------------++-- |+--+-- >>> import qualified Data.Universe.Class as U+-- >>> take 10 (U.universe :: [Nat])+-- [0,1,2,3,4,5,6,7,8,9]+--+-- @since 0.1.2+instance U.Universe Nat where+    universe = go Z where+        go n = n : go (S n)  ------------------------------------------------------------------------------- -- Showing

@@ -7,6 +7,7 @@ {-# LANGUAGE RankNTypes           #-} {-# LANGUAGE ScopedTypeVariables  #-} {-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE Trustworthy          #-} {-# LANGUAGE TypeFamilies         #-} {-# LANGUAGE TypeOperators        #-} {-# LANGUAGE UndecidableInstances #-}@@ -28,6 +29,7 @@     snatToNatural,     -- * Implicit     SNatI(..),+    snat,     withSNat,     reify,     reflect,@@ -37,10 +39,7 @@     EqNat,     discreteNat,     -- * Induction-    induction,     induction1,-    InlineInduction (..),-    inlineInduction,     -- ** Example: unfoldedFix     unfoldedFix,     -- * Arithmetic@@ -65,12 +64,11 @@     proofMultNOne,     )  where -import Data.Function      (fix)-import Data.Proxy         (Proxy (..))-import Data.Type.Dec      (Dec (..))-import Data.Type.Equality ((:~:) (..), TestEquality (..))-import Data.Typeable      (Typeable)-import Numeric.Natural    (Natural)+import Data.Function   (fix)+import Data.Proxy      (Proxy (..))+import Data.Type.Dec   (Dec (..))+import Data.Typeable   (Typeable)+import Numeric.Natural (Natural)  import qualified GHC.TypeLits as GHC @@ -81,10 +79,15 @@ #endif  import Data.Nat+import TrustworthyCompat  -- $setup -- >>> :set -XTypeOperators -XDataKinds--- >>> import Data.Type.Dec (decShow)+-- >>> import qualified GHC.TypeLits as GHC+-- >>> import Data.Type.Dec (Dec (..), decShow)+-- >>> import Data.Type.Equality+-- >>> import Control.Applicative (Const (..))+-- >>> import Data.Coerce (coerce)  ------------------------------------------------------------------------------- -- SNat@@ -98,11 +101,34 @@  deriving instance Show (SNat p) --- | Convenience class to get 'SNat'.-class               SNatI (n :: Nat) where snat :: SNat n-instance            SNatI 'Z         where snat = SZ-instance SNatI n => SNatI ('S n)     where snat = SS+-- | Implicit 'SNat'.+--+-- In an unorthodox singleton way, it actually provides an induction function.+--+-- The induction should often be fully inlined.+-- See @test/Inspection.hs@.+--+-- >>> :set -XPolyKinds+-- >>> newtype Const a b = Const a deriving (Show)+-- >>> induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3+-- Const 6+--+class SNatI (n :: Nat) where+    induction+        :: f 'Z                                    -- ^ zero case+        -> (forall m. SNatI m => f m -> f ('S m))  -- ^ induction step+        -> f n +instance SNatI 'Z where+    induction n _c = n++instance SNatI n => SNatI ('S n) where+    induction n c = c (induction n c)++-- | Construct explicit 'SNat' value.+snat :: SNatI n => SNat n+snat = induction SZ (\_ -> SS)+ -- | Constructor 'SNatI' dictionary from 'SNat'. -- -- @since 0.0.3@@ -112,11 +138,11 @@  -- | Reflect type-level 'Nat' to the term level. reflect :: forall n proxy. SNatI n => proxy n -> Nat-reflect _ = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)+reflect _ = unKonst (induction (Konst Z) (kmap S) :: Konst Nat n)  -- | As 'reflect' but with any 'Num'. reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m-reflectToNum _ = unTagged (induction1 (Tagged 0) (retagMap (1+)) :: Tagged n m)+reflectToNum _ = unKonst (induction (Konst 0) (kmap (1+)) :: Konst m n)  -- | Reify 'Nat'. --@@ -133,7 +159,7 @@ -- snatToNat :: forall n. SNat n -> Nat snatToNat SZ = Z-snatToNat SS = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)+snatToNat SS = unKonst (induction (Konst Z) (kmap S) :: Konst Nat n)  -- | Convert 'SNat' to 'Natural' --@@ -145,7 +171,7 @@ -- snatToNatural :: forall n. SNat n -> Natural snatToNatural SZ = 0-snatToNatural SS = unTagged (induction1 (Tagged 0) (retagMap succ) :: Tagged n Natural)+snatToNatural SS = unKonst (induction (Konst 0) (kmap succ) :: Konst Natural n)  ------------------------------------------------------------------------------- -- Equality@@ -224,68 +250,22 @@ -- Induction ------------------------------------------------------------------------------- +newtype Konst a (n :: Nat) = Konst { unKonst :: a }++kmap :: (a -> b) -> Konst a n -> Konst b m+kmap = coerce++newtype Flipped f a (b :: Nat) = Flip { unflip :: f b a }+ -- | Induction on 'Nat', functor form. Useful for computation. ----- >>> induction1 (Tagged 0) $ retagMap (+2) :: Tagged Nat3 Int--- Tagged 6--- induction1     :: forall n f a. SNatI n     => f 'Z a                                      -- ^ zero case     -> (forall m. SNatI m => f m a -> f ('S m) a)  -- ^ induction step     -> f n a-induction1 z f = go where-    go :: forall m. SNatI m => f m a-    go = case snat :: SNat m of-        SZ -> z-        SS -> f go---- | Induction on 'Nat'.------ Useful in proofs or with GADTs, see source of 'proofPlusNZero'.-induction-    :: forall n f. SNatI n-    => f 'Z                                    -- ^ zero case-    -> (forall m. SNatI m => f m -> f ('S m))  -- ^ induction step-    -> f n-induction z f = go where-    go :: forall m. SNatI m => f m-    go = case snat :: SNat m of-        SZ -> z-        SS -> f go---- | The induction will be fully inlined.------ See @test/Inspection.hs@.-class SNatI n => InlineInduction (n :: Nat) where-    inlineInduction1 :: f 'Z a -> (forall m. InlineInduction m => f m a -> f ('S m) a) -> f n a--instance InlineInduction 'Z where-    inlineInduction1 z _ = z--instance InlineInduction n => InlineInduction ('S n) where-    inlineInduction1 z f = f (inlineInduction1 z f)--    -- Specialise this to few first numerals.-    {-# SPECIALIZE instance InlineInduction ('S 'Z) #-}-    {-# SPECIALIZE instance InlineInduction ('S ('S 'Z)) #-}-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S 'Z))) #-}-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S 'Z)))) #-}-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S 'Z))))) #-}-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S 'Z)))))) #-}-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S 'Z))))))) #-}-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) #-}-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) #-}---- | See 'InlineInduction'.-inlineInduction-    :: forall n f. InlineInduction n-    => f 'Z                                              -- ^ zero case-    -> (forall m. InlineInduction m => f m -> f ('S m))  -- ^ induction step-    -> f n-inlineInduction z f = unConst' $ inlineInduction1 (Const' z) (Const' . f . unConst')--newtype Const' (f :: Nat -> *) (n :: Nat) a = Const' { unConst' :: f n }+induction1 z f = unflip (induction (Flip z) (\(Flip x) -> Flip (f x)))+{-# INLINE induction1 #-}  -- | Unfold @n@ steps of a general recursion. --@@ -298,15 +278,15 @@ -- 'unfoldedFix' ('Proxy' :: 'Proxy' 'Nat3') f = f (f (f (fix f))) -- @ ---unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a-unfoldedFix _ = getFix (inlineInduction1 start step :: Fix n a) where-    start :: Fix 'Z a+unfoldedFix :: forall n a proxy. SNatI n => proxy n -> (a -> a) -> a+unfoldedFix _ = getFix (induction start step :: Fix a n) where+    start :: Fix a 'Z     start = Fix fix -    step :: Fix m a -> Fix ('S m) a+    step :: Fix a m -> Fix a ('S m)     step (Fix go) = Fix $ \f -> f (go f) -newtype Fix (n :: Nat) a = Fix { getFix :: (a -> a) -> a }+newtype Fix a (n :: Nat) = Fix { getFix :: (a -> a) -> a }  ------------------------------------------------------------------------------- -- Conversion to GHC Nat@@ -451,18 +431,3 @@ newtype ProofMultNOne n = ProofMultNOne { getProofMultNOne :: Mult n Nat1 :~: n }  -- TODO: multAssoc------------------------------------------------------------------------------------ Tagged------------------------------------------------------------------------------------ Own 'Tagged', to not depend on @tagged@------ We shouldn't export this in public interface.-newtype Tagged (n :: Nat) a = Tagged a deriving Show--unTagged :: Tagged n a -> a-unTagged (Tagged a) = a--retagMap :: (a -> b) -> Tagged n a -> Tagged m b-retagMap f = Tagged . f . unTagged

@@ -6,6 +6,7 @@ {-# LANGUAGE GADTs                 #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE Safe                  #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE StandaloneDeriving    #-} {-# LANGUAGE TypeOperators         #-}@@ -49,11 +50,14 @@     ) where  import Data.Type.Dec      (Dec (..), Decidable (..), Neg)-import Data.Type.Equality ((:~:) (..)) import Data.Typeable      (Typeable) import Data.Void          (absurd)  import Data.Type.Nat+import TrustworthyCompat++-- $setup+-- >>> import Data.Type.Nat  ------------------------------------------------------------------------------- -- Proof

@@ -5,6 +5,7 @@ {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE GADTs                 #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe                  #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE StandaloneDeriving    #-} {-# LANGUAGE TypeOperators         #-}@@ -35,14 +36,16 @@     proofZeroLEZero,     ) where -import Data.Type.Dec      (Dec (..), Decidable (..), Neg)-import Data.Type.Equality ((:~:) (..))-import Data.Typeable      (Typeable)-import Data.Void          (absurd)+import Data.Type.Dec (Dec (..), Decidable (..), Neg)+import Data.Typeable (Typeable)+import Data.Void     (absurd) -import Data.Type.Nat-import qualified Data.Type.Nat.LE as ZeroSucc+import qualified Control.Category as C +import           Data.Type.Nat+import qualified Data.Type.Nat.LE  as ZeroSucc+import           TrustworthyCompat+ ------------------------------------------------------------------------------- -- Proof -------------------------------------------------------------------------------@@ -61,6 +64,12 @@  instance Ord (LEProof n m) where     compare _ _ = EQ++-- | The other variant ('Data.Type.Nat.LE.LEPRoof') isn't 'C.Category',+-- because 'Data.Type.Nat.LE.leRefl` requires 'SNat' evidence.+instance C.Category LEProof where+    id  = leRefl+    (.) = flip leTrans  ------------------------------------------------------------------------------- -- Conversion

@@ -4,6 +4,7 @@ {-# LANGUAGE GADTs                 #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE Safe                  #-} {-# LANGUAGE TypeFamilies          #-} {-# LANGUAGE TypeOperators         #-} {-# LANGUAGE UndecidableInstances  #-}@@ -19,6 +20,9 @@  import Data.Type.Nat import Data.Type.Nat.LE++-- $setup+-- >>> import Data.Type.Nat  -- | An evidence \(n < m\) which is the same as (\1 + n \le m\). type LTProof n m = LEProof ('S n) m

@@ -0,0 +1,9 @@+{-# LANGUAGE Trustworthy #-}+module TrustworthyCompat (+    (:~:) (..),+    TestEquality (..),+    coerce,+) where++import Data.Coerce        (coerce)+import Data.Type.Equality (TestEquality (..), (:~:) (..))

@@ -1,5 +1,7 @@+{-# LANGUAGE DataKinds           #-} {-# LANGUAGE DeriveGeneric       #-} {-# LANGUAGE GADTs               #-}+{-# LANGUAGE RankNTypes          #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell     #-} {-# LANGUAGE TypeOperators       #-}@@ -21,17 +23,29 @@ import Unsafe.Coerce (unsafeCoerce)  ---------------------------------------------------------------------------------- InlineInduction+-- SNatI -------------------------------------------------------------------------------  -- | This doesn't evaluate compile time. lhsInline :: Int-lhsInline = unTagged (N.inlineInduction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)+lhsInline = unTagged (N.induction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)  -- | This doesn't evaluate compile time. lhsNormal :: Int-lhsNormal = unTagged (N.induction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)+lhsNormal = unTagged (manualInduction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int) +--- | Induction on 'Nat'.+manualInduction1+     :: forall n f a. N.SNatI n+     => f 'N.Z a                                        -- ^ zero case+     -> (forall m. N.SNatI m => f m a -> f ('N.S m) a)  -- ^ induction step+     -> f n a+manualInduction1 z f = go where+    go :: forall m. N.SNatI m => f m a+    go = case N.snat :: N.SNat m of+        N.SZ -> z+        N.SS -> f go+ rhs :: Int rhs = 5 @@ -110,10 +124,10 @@ -- Power ------------------------------------------------------------------------------- -power :: forall n. N.InlineInduction n => Proxy n -> Int -> Int+power :: forall n. N.SNatI n => Proxy n -> Int -> Int power _ k = unTagged impl where     impl :: Tagged n Int-    impl = N.inlineInduction1 (Tagged 1) $ \(Tagged rec') -> Tagged (rec' * k)+    impl = N.induction1 (Tagged 1) $ \(Tagged rec') -> Tagged (rec' * k)  lhsPower5 :: Int -> Int lhsPower5 = power (Proxy :: Proxy N.Nat5)