h*3U.      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~0.3.2Safe7NfinNat natural numbers.Better than GHC's built-in   for some use cases.fin displaying a structure of .explicitShow 0"Z"explicitShow 2 "S (S Z)"fin displaying a structure of .finFold .cata [] ('x' :) 2"xx"finConvert  to  toNatural 00 toNatural 22toNatural $ S $ S $ Z2finConvert  to  fromNatural 44explicitShow (fromNatural 4)"S (S (S (S Z)))"fin)import qualified Data.Universe.Class as Utake 10 (U.universe :: [Nat])[0,1,2,3,4,5,6,7,8,9]fin is printed as .To see explicit structure, use  or     Trustworthy Trustworthy()*167Z&+finDivision by two.  is 0 and  is 1 as a remainder.$:kind! DivMod2 Nat7 == '(Nat3, True)%DivMod2 Nat7 == '(Nat3, True) :: Bool= 'True%:kind! DivMod2 Nat4 == '(Nat2, False)&DivMod2 Nat4 == '(Nat2, False) :: Bool= 'True,fin Multiplication by two. Doubling.#reflect (snat :: SNat (Mult2 Nat4))8-finMultiplication.'reflect (snat :: SNat (Mult Nat2 Nat3))6.fin Addition.'reflect (snat :: SNat (Plus Nat1 Nat2))3/finConvert from GHC .:kind! FromGHC 7FromGHC 7 :: Nat%= 'S ('S ('S ('S ('S ('S ('S 'Z))))))0finConvert to GHC .:kind! ToGHC Nat5ToGHC Nat5 :: GHC.Nat...= 51finType family used to implement   from Data.Type.Equality module.2fin Implicit 4.In an unorthodox singleton way, it actually provides an induction function.2The 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 Nat3Const 64fin Singleton of .7fin A pattern with explicit argument:let predSNat :: SNat (S n) -> SNat n; predSNat (SS' n) = npredSNat (SS' (SS' SZ))SS!reflect $ predSNat (SS' (SS' SZ))18finConstruct explicit 4 value.9fin Constructor 2 dictionary from 4.:finReflect type-level  to the term level.;finAs : but with any .<finReify .reify nat3 reflect3=finConvert 4 to .snatToNat (snat :: SNat Nat1)1>finConvert 4 to !snatToNatural (snat :: SNat Nat0)0!snatToNatural (snat :: SNat Nat2)2?fin&Decide equality of type-level numbers.(eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2) Just Refl(eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)Nothing@fin&Decide equality of type-level numbers.6decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2)) "Yes Refl"Afin&Decide equality of type-level numbers.)cmpNat :: GOrdering Nat3 (Plus Nat1 Nat2)GEQ)cmpNat :: GOrdering Nat3 (Mult Nat2 Nat2)GLT)cmpNat :: GOrdering Nat5 (Mult Nat2 Nat2)GGTBfin Induction on ', functor form. Useful for computation.CfinUnfold n steps of a general recursion.Note: Always  benchmark". This function may give you both bad properties: a lot of code (increased binary size), and worse performance. For known n C# will unfold recursion, for example C ( ::  ') f = f (f (f (fix f))) Dfin  0 + n = nEfin  n + 0 = nFfin  0 * n = 0Gfin  n * 0 = 0Hfin  1 * n = nIfin  n * 1 = nLfinMfinNfinOfinPfinQfinRfinSfinTfinUfin3fin zero casefininduction stepBfin zero casefininduction step;4567=>2389<:;?1@ABC.-,+0/ *)('&%$#"!DEFGHI<45677=>2389<:;?1@ABC.-,+0/ *)('&%$#"!DEFGHISafe)*167XfinTotal order of , less-than-or-Equal-to,  \le .ZfinAn evidence of n \le m.  zero+succ definition.]fin Constructor X dictionary from Z.^fin \forall n : \mathbb{N}, 0 \le n _fin8\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m `fin8\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m afin \forall n : \mathbb{N}, n \le n bfin4\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m cfin4\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m dfin?\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m efin\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p ffin;\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n gfin;\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n) leProof :: LEProof Nat2 Nat3LESucc (LESucc LEZero)/leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))LESucc (LESucc (LESucc LEZero))8lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))LESucc (LESucc LEZero)hfin Find the Z n m, i.e. compare numbers.ifin0\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0 lfinZ values are unique (not  though!).mfinnfinXYZ[\]h^_abdefgc`iXYZ[\]h^_abdefgc`iSafe)*17rfinLess-Than-or. <. Well-founded relation on .GHC can solve this for us!ltProof :: LTProof Nat0 Nat4 LESucc LEZeroltProof :: LTProof Nat2 Nat4LESucc (LESucc (LESucc LEZero))ltProof :: LTProof Nat3 Nat3... ...error......tfin An evidence n < m# which is the same as (1 + n le m).vfin'\forall n : \mathbb{N}, n < n \to \bot wfin5\forall n\, m : \mathbb{N}, n < m \to m < n \to \bot xfin:\forall n\, m\, p : \mathbb{N}, n < m \to m < p \to n < p rstuvwxrstuvwxSafe)*167!zfinAn evidence of n \le m.  refl+step definition.}fin Convert from  zero+succ to  refl+step definition. Inverse of ~.~finConvert  refl+step to  zero+succ definition. Inverse of }.fin \forall n : \mathbb{N}, 0 \le n fin8\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m fin8\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m fin \forall n : \mathbb{N}, n \le n fin4\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m fin4\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m fin?\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m fin\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p fin;\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n fin;\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n) fin Find the z n m, i.e. compare numbers.fin0\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0 finfinfinThe other variant ( ) isn't  , because  requires 4 evidence.finz values are unique (not  though!).z{|}~z{|}~Safe )*167.!finFinite numbers: [0..n-1].finMirror the values,  becomes , etc.#map mirror universe :: [Fin N.Nat4] [3,2,1,0] reverse universe :: [Fin N.Nat4] [3,2,1,0]finMultiplicative inverse. Works for  n where n3 is coprime with an argument, i.e. in general when n is prime.$map inverse universe :: [Fin N.Nat5] [0,1,3,2,4];zipWith (*) universe (map inverse universe) :: [Fin N.Nat5] [0,1,1,1,1]Adaptation of https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm#Modular_integerspseudo-code in Wikipediafin displaying a structure of .explicitShow (0 :: Fin N.Nat1)"FZ"explicitShow (2 :: Fin N.Nat3) "FS (FS FZ)"fin displaying a structure of .finFold .fin Convert to .fin Convert from .$fromNat N.nat1 :: Maybe (Fin N.Nat2)Just 1$fromNat N.nat1 :: Maybe (Fin N.Nat1)Nothingfin Convert to .finConvert from any  .fin All values. [minBound .. maxBound] won't work for  *.universe :: [Fin N.Nat3][0,1,2]finLike  but ."universe1 :: NonEmpty (Fin N.Nat3) 0 :| [1,2]fin! which will be fully inlined, if n is known at compile time.inlineUniverse :: [Fin N.Nat3][0,1,2]fin(inlineUniverse1 :: NonEmpty (Fin N.Nat3) 0 :| [1,2]fin * is not inhabited.finCounting to one is boring.boring0finReturn a one less.isMin (FZ :: Fin N.Nat1)Nothing*map isMin universe :: [Maybe (Fin N.Nat3)][Nothing,Just 0,Just 1,Just 2]finReturn a one less.isMax (FZ :: Fin N.Nat1)Nothing*map isMax universe :: [Maybe (Fin N.Nat3)][Just 0,Just 1,Just 2,Nothing]fin)map weakenRight1 universe :: [Fin N.Nat5] [1,2,3,4]fin(map weakenLeft1 universe :: [Fin N.Nat5] [0,1,2,3]finmap (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])[0,1,2]finmap (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])[2,3,4]fin Append two  s together.6append (Left fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))27append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))7fin Inverse of ..split fin2 :: Either (Fin N.Nat2) (Fin N.Nat3)Right 0.split fin1 :: Either (Fin N.Nat2) (Fin N.Nat3)Left 18map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)]'[Left 0,Left 1,Right 0,Right 1,Right 2]fin(U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))Truefinfinfin works only on  n where n is prime.finOperations module n.3map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3] [0,1,2,0,1,1]fromInteger 42 :: Fin N.Nat0*** Exception: divide by zero...signum (FZ :: Fin N.Nat1)0signum (3 :: Fin N.Nat4)12 + 3 :: Fin N.Nat412 * 3 :: Fin N.Nat42finfin is printed as .To see explicit structure, use  or finlet xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ][EQ,LT,LT,LT,LT,LT][GT,EQ,LT,LT,LT,LT][GT,GT,EQ,LT,LT,LT][GT,GT,GT,EQ,LT,LT]fin eqp FZ FZTrueeqp FZ (FS FZ)Falselet xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]$[True,False,False,False,False,False]$[False,True,False,False,False,False]$[False,False,True,False,False,False]$[False,False,False,True,False,False]$$  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~jnopqrstuvwxy|}z{        fin-0.3.2-5D8WPhLouk8EigGnsDPub5Data.FinData.Nat Data.Type.NatData.Type.Nat.LEData.Type.Nat.LTData.Type.Nat.LE.ReflStepfin GHC.TypeLitsNatTrustworthyCompatData.Type.Equality==LEPRoofleReflbaseGHC.Real toIntegerZS explicitShowexplicitShowsPreccata toNatural fromNaturalnat0nat1nat2nat3nat4nat5nat6nat7nat8nat9 $fUniverseNat $fFunctionNat$fCoArbitraryNat$fArbitraryNat $fHashableNat $fNFDataNat $fEnumNat $fIntegralNat $fRealNat$fNumNat$fOrdNat $fShowNat$fEqNat $fDataNatNat9Nat8Nat7Nat6Nat5Nat4Nat3Nat2Nat1Nat0DivMod2Mult2MultPlusFromGHCToGHCEqNatSNatI inductionSNatSZSSSS'snatwithSNatreflect reflectToNumreify snatToNat snatToNaturaleqNat discreteNatcmpNat induction1 unfoldedFixproofPlusZeroNproofPlusNZeroproofMultZeroNproofMultNZero proofMultOneN proofMultNOne$fSNatIS$fSNatIZ $fOrdPNatSNat $fEqPNatSNat $fOrdSNat$fEqSNat$fGCompareNatSNat $fGEqNatSNat$fGNFDataNatSNat $fNFDataSNat$fGShowNatSNat $fBoringSNat$fTestEqualityNatSNat $fShowSNatLEleProofLEProofLEZeroLESucc withLEProofleZeroleSucclePredleStepleStepLleAsymleTransleSwapleSwap'decideLEproofZeroLEZero$fDecidableLEProof $fOrdLEProof $fEqLEProof$fAbsurdLEProof$fBoringLEProof$fLESm$fLEZm $fShowLEProofLTltProofLTProof withLTProof ltReflAbsurd ltSymAbsurdltTrans$fLTnmLEReflLEStep fromZeroSucc toZeroSucc$fCategoryNatLEProofFinFZFSmirrorinversetoNatfromNatuniverse universe1inlineUniverseinlineUniverse1absurdboringisMinisMax weakenRight1 weakenLeft1 weakenLeft weakenRightappendsplitfin0fin1fin2fin3fin4fin5fin6fin7fin8fin9 $fFiniteFin $fUniverseFin $fFunctionFin$fCoArbitraryFin $fAbsurdFin $fHashableFin $fNFDataFin $fEnumFin $fIntegralFin $fRealFin$fNumFin $fGShowNatFin $fShowFin $fOrdPNatFin $fEqPNatFin $fBoundedFin$fArbitraryFin$fOrdFin$fEqFinGHC.Showshow showsPrec ghc-bignumGHC.Num.NaturalNatural:~:Refl TestEquality testEqualityghc-primGHC.Primcoerce GHC.TypesFalseTrue GHC.TypeNatsGHC.NumNum Data.ProxyProxy#boring-0.2.2-8XvgXnwRdSSAXF9IJSJwMz Data.BoringBoringControl.CategoryCategoryGHC.EnumminBoundmaxBound unsafeFromNum GHC.ClassesOrdGHC.BaseNonEmptyquot