!}      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Safe2 bin Non-zero binary natural numbers.We could have called this type Bin1., but that's used as type alias for promoted BP  in  Data.Type.Bin.binonebinmult2bin mult2 plus 1bin displaying a structure of .explicitShow 11"B1 (B1 (B0 BE))"bin displaying a structure of .bin for .bin for .Throws when given 0. binFold . bin Convert from  to .binNOTE: , ,  and 4 are __NOT_ implemented. They may make number zero.binsort [1 .. 9 :: BinP][1,2,3,4,5,6,7,8,9] bin1bin2xbin2x + 1    Safe2&:"binBinary natural numbers.NNumbers are represented in little-endian order, the representation is unique.)mapM_ (putStrLn . explicitShow) [0 .. 7]BZBP BE BP (B0 BE) BP (B1 BE)BP (B0 (B0 BE))BP (B1 (B0 BE))BP (B0 (B1 BE))BP (B1 (B1 BE))#binzero$binnon-zero%binThis is a total function.map predP [1..10][0,1,2,3,4,5,6,7,8,9](bin displaying a structure of ".explicitShow 0"BZ"explicitShow 2 "BP (B0 BE)")bin displaying a structure of "..binFold "./bin Convert from " to .toNat 55N.explicitShow (toNat 5)"S (S (S (S (S Z))))"0bin Convert from  to ". fromNat 55explicitShow (fromNat 5)"BP (B1 (B0 BE))"1binConvert " to  toNatural 00 toNatural 22toNatural $ BP $ B0 $ B1 $ BE62binConvert  to  fromNatural 44explicitShow (fromNatural 4)"BP (B0 (B0 BE))"Cbintake 10 $ iterate succ BZ[0,1,2,3,4,5,6,7,8,9]take 10 [BZ ..][0,1,2,3,4,5,6,7,8,9]Fbin 0 + 2 :: Bin2 1 + 2 :: Bin3 4 * 8 :: Bin32 7 * 7 :: Bin49Gbin" is printed as .To see explicit structure, use ( or ).bin0bin1bin2xbin2x + 1"$#%&'()*+,-./0123456789:;<"$#12/0.()%&'*+-,3456789:;<None&'.2>HSUVX/) bin:kind! GhcDivMod2 13 GhcDivMod2 13 :: (GHC.Nat, Bool) = '(6, 'True)Ybin Let constraint solver construct [.[bin Singleton of ._bin Construct Y dictionary from [.`binReify .abinReflect type-level  to the term level.bbinReflect type-level  to the term level .cbin Cconvert [ to .dbinConvert [ to .%sbinpToNatural (sbinp :: SBinP BinP8)8gbin Induction on .gbinP(1)bin\forall b. P(b) \to P(2b)bin\forall b. P(b) \to P(2b + 1)KLMNOPQRSTUVWXYZ[\]^_`abcdefg[\]^cdYZ_`abegUfTXWVSRQPONMLKNone&'.2>HSUVXJLvbin Addition.:kind! Plus Bin7 Bin7Plus Bin7 Bin7 :: Bin= 'BP ('B0 ('B1 ('B1 'BE))):kind! Mult2 Bin7Mult2 Bin7 :: Bin= 'BP ('B0 ('B1 BinP3))wbinPredecessor type family..:kind! Pred BP.BinP1Pred BP.BinP1 :: Bin= 'BZ:kind! Pred BP.BinP5Pred BP.BinP5 :: Bin= 'BP ('B0 ('B0 BP.BinP1)):kind! Pred BP.BinP8Pred BP.BinP8 :: Bin= 'BP ('B1 ('B1 'BE)):kind! Pred BP.BinP6Pred BP.BinP6 :: Bin= 'BP ('B1 ('B0 'BE))zbinSuccessor type family.:kind! Succ Bin5Succ Bin5 :: Bin= 'BP ('B0 ('B1 'BE)) z :: " -> " y :: " ->  x ::  -> " {binMultiply by two and add one.:kind! Mult2Plus1 Bin0Mult2Plus1 Bin0 :: BinP= 'BE:kind! Mult2Plus1 Bin5Mult2Plus1 Bin5 :: BinP= 'B1 ('B1 BinP2)|binMultiply by two.:kind! Mult2 Bin0Mult2 Bin0 :: Bin= 'BZ:kind! Mult2 Bin7Mult2 Bin7 :: Bin= 'BP ('B0 ('B1 BinP3))}bin Convert from fin .:kind! FromNat N.Nat5FromNat N.Nat5 :: Bin= 'BP ('B1 ('B0 'BE))~bin Convert to fin .:kind! ToNat Bin5ToNat Bin5 :: Nat= 'S ('S ('S ('S ('S 'Z))))bin:kind! GhcDivMod2 13 GhcDivMod2 13 :: (GHC.Nat, Bool) = '(6, 'True)binConvert from GHC .:kind! FromGHC 7FromGHC 7 :: Bin= 'BP ('B1 ('B1 'BE))binConvert to GHC .:kind! ToGHC Bin5ToGHC Bin5 :: GHC.Nat= 5bin Let constraint solver construct .bin Singleton of ".bin Construct  dictionary from .binReify "reify bin3 reflect3binReflect type-level " to the term level.binReflect type-level " to the term level .binConvert  to ".binConvert  to .!sbinToNatural (sbin :: SBin Bin9)9bin Induction on ".binP(0)binP(1)bin\forall b. P(b) \to P(2b)bin\forall b. P(b) \to P(2b + 1),YZ[\]^_cdlmnopqrstuvwxyz{|}~,[\]^cdYZ_zyxwv|{~}utsrqponmlNone &'.12HX^binFixed-width unsigned integers,  s for short.sThe number is thought to be stored in big-endian format, i.e. most-significant bit first. (as in binary literals).bin  w =  w + 1bin displaying a structure of  nexplicitShow WE"WE"explicitShow $ W0 WE"W0 WE"#explicitShow $ W1 $ W0 $ W1 $ W0 WE"W1 $ W0 $ W1 $ W0 WE"bin displaying a structure of  n.explicitShowsPrec 0 (W0 WE) """W0 WE"explicitShowsPrec 1 (W0 WE) "" "(W0 WE)"bin Convert to  number+let u = W0 $ W1 $ W1 $ W1 $ W0 $ W1 $ W0 WEu 0b0111010 toNatural u58(map toNatural (universe :: [Wrd N.Nat3])[0,1,2,3,4,5,6,7]binAll values, i.e. universe of  .universe :: [Wrd 'Z][WE]universe :: [Wrd N.Nat3]1[0b000,0b001,0b010,0b011,0b100,0b101,0b110,0b111]binlet u = W0 $ W0 $ W1 $ W1 WElet v = W0 $ W1 $ W0 $ W1 WE(u, v)(0b0011,0b0101)(complement u, complement v)(0b1100,0b1010)(u .&. v, u .|. v, u `xor` v)(0b0001,0b0111,0b0110)(shiftR v 1, shiftL v 1)(0b0010,0b1010)(rotateR u 1, rotateL u 3)(0b1001,0b1001) popCount u2bin is printed as a binary literal.let i = W1 $ W0 $ W1 $ W0 WEi0b1010explicitShow i"W1 $ W0 $ W1 $ W0 WE"At the time being, there is no  instance.None&'.12=>?@ACHXfj bin is a structure inside .bin is to  is what Fin is to , when n is .binConvert  to .binConvert  to .binCounting to one is boringboring0bin and  serve as FZ and FSJ, with types specified so type-inference works backwards from the result.top :: PosP BinP40pop (pop top) :: PosP BinP42pop (pop top) :: PosP BinP92binSee .binuniverse :: [PosP BinP9][0,1,2,3,4,5,6,7,8]binThis gives a hint, what the n parameter means in .!universe' :: [PosP' N.Nat2 BinP2][0,1,2,3,4,5,6,7]bin%position is either at the last digit;binsomewhere herebinor there, if the bit is one;binor only there if it is none.None&'.12=>?@ACHXf}t bin is to " is what Fin is to Nat.7The name is picked, as sthe lack of beter alternatives.binConvert  to &map toNatural (universe :: [Pos Bin7])[0,1,2,3,4,5,6]bin # is not inhabited.binCounting to one is boringboring0bin and  serve as FZ and FSJ, with types specified so type-inference works backwards from the result.top :: Pos Bin40pop (pop top) :: Pos Bin42pop (pop top) :: Pos Bin92binSee .binLike FS for Fin. Some tests:+map weakenRight1 $ (universe :: [Pos Bin2])[1,2]+map weakenRight1 $ (universe :: [Pos Bin3])[1,2,3]+map weakenRight1 $ (universe :: [Pos Bin4]) [1,2,3,4]+map weakenRight1 $ (universe :: [Pos Bin5]) [1,2,3,4,5]+map weakenRight1 $ (universe :: [Pos Bin6]) [1,2,3,4,5,6]binUniverse, i.e. all [Pos b]universe :: [Pos Bin9][0,1,2,3,4,5,6,7,8]<traverse_ (putStrLn . explicitShow) (universe :: [Pos Bin5])Pos (PosP (Here WE)))Pos (PosP (There1 (There0 (AtEnd 0b00)))))Pos (PosP (There1 (There0 (AtEnd 0b01)))))Pos (PosP (There1 (There0 (AtEnd 0b10)))))Pos (PosP (There1 (There0 (AtEnd 0b11))))bin!minBound < (maxBound :: Pos Bin5)True       !"#$%&'()*+,-./ 0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwVxyzW{|}XYZ~bcdih   bin-0.1-1VmEg7qlTVO1si1D9V7wEC Data.BinPData.BinData.Type.BinP Data.Type.BinData.WrdData.BinP.PosP Data.Bin.PosBinPBEB0B1 predMaybe explicitShowexplicitShowsPrec toNatural fromNaturalcatatoNatbinP1binP2binP3binP4binP5binP6binP7binP8binP9$fFunctionBinP$fCoArbitraryBinP$fArbitraryBinP $fBitsBinP$fHashableBinP $fNFDataBinP $fEnumBinP$fIntegralBinP $fRealBinP $fNumBinP $fShowBinP $fOrdBinP$fEqBinP $fDataBinPBinBZBPpredPmult2 mult2Plus1andPxorP clearBitPcomplementBitPfromNatbin0bin1bin2bin3bin4bin5bin6bin7bin8bin9 $fBitsBin $fFunctionBin$fCoArbitraryBin$fArbitraryBin $fHashableBin $fNFDataBin $fEnumBin $fIntegralBin $fRealBin$fNumBin $fShowBin$fEqBin$fOrdBin $fDataBinBinP9BinP8BinP7BinP6BinP5BinP4BinP3BinP2BinP1PlusSuccToNatFromGHCToGHCSBinPIsbinpSBinPSBESB0SB1 withSBinPreifyreflect reflectToNum sbinpToBinPsbinpToNaturaleqBinPwithSucc induction$fTestEqualityBinPSBinP $fSBinPIB1 $fSBinPIB0 $fSBinPIBEBin9Bin8Bin7Bin6Bin5Bin4Bin3Bin2Bin1Bin0PredSucc''Succ' Mult2Plus1Mult2FromNatSBinIsbinSBinSBZSBPwithSBin sbinToBin sbinToNaturaleqBin$fTestEqualityBinSBin $fSBinIBP $fSBinIBZWrdWEW0W1testBitclearBitsetBit complementBit complement complement2.&..|.xorshiftRshiftLrotateRrotateLpopCountshiftL1shiftR1rotateL1rotateR1universe $fFunctionWrd$fCoArbitraryWrd$fArbitraryWrd$fFiniteBitsWrd $fBitsWrd$fNumWrd $fBoundedWrd $fHashableWrd $fNFDataWrd $fShowWrd$fOrdWrd$fEqWrdPosP'AtEndHereThere1There0PosPunPosP explicitShow'explicitShowsPrec' toNatural'boringtoppop weakenRight1 weakenRight1' universe'$fFunctionPosP'$fCoArbitraryPosP'$fBoundedPosP' $fShowPosP' $fOrdPosP'$fFunctionPosP$fCoArbitraryPosP$fArbitraryPosP $fBoundedPosP $fShowPosP$fArbitraryPosP'$fEqPosP $fOrdPosP $fEqPosP'Posabsurd $fFunctionPos$fCoArbitraryPos$fArbitraryPos $fBoundedPos $fShowPos$fOrdPos$fEqPosbaseGHC.Showshow showsPrec fin-0.1.1-CmlKX4I25sbDg8chH2xNz3Data.NatNat Data.Bits GHC.NaturalNatural GhcDivMod2GHC.NumNumghc-prim GHC.TypesZ