h$.(      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Safe3 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]!sort $ reverse [ 1 .. 9 :: BinP ][1,2,3,4,5,6,7,8,9]'sort $ [ 1 .. 9 ] ++ [ 1 .. 9 :: BinP ]%[1,1,2,2,3,3,4,4,5,5,6,6,7,7,8,8,9,9] bin1bin2xbin2x + 1    Safe3 a"binBinary natural numbers.Numbers 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:;<Safe '(/23KbinFixed-width unsigned integers, K s for short.The number is thought to be stored in big-endian format, i.e. most-significant bit first. (as in binary literals).Tbin T w = S w + 1abin displaying a structure of K nexplicitShow WE"WE"explicitShow $ W0 WE"W0 WE"#explicitShow $ W1 $ W0 $ W1 $ W0 WE"W1 $ W0 $ W1 $ W0 WE"bbin displaying a structure of K n.explicitShowsPrec 0 (W0 WE) """W0 WE"explicitShowsPrec 1 (W0 WE) "" "(W0 WE)"cbin 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]dbinAll values, i.e. universe of K .universe :: [Wrd 'Z][WE]universe :: [Wrd N.Nat3]1[0b000,0b001,0b010,0b011,0b100,0b101,0b110,0b111]ibinlet 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 u2nbinK 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.KLMNOPQRSTUVWXYZ[\]^_`abcdKLMNabcdWUVSTXY[Z\QPRO]^_` TrustworthytSafe'(/23?binbin Let constraint solver construct .bin Singleton of .bin Construct  dictionary from .binReify .binReflect type-level  to the term level.binReflect type-level  to the term level .bin Cconvert  to .binConvert  to .%sbinpToNatural (sbinp :: SBinP BinP8)8bin Induction on .binbinbinbinbinbinP(1)bin\forall b. P(b) \to P(2b)bin\forall b. P(b) \to P(2b + 1)qrstuvwxyz{|}~{z~}|yxwvutsrqSafe'(/23?bin Addition.:kind! Plus Bin3 Bin3 == Bin6Plus Bin3 Bin3 == Bin6 :: Bool= 'True:kind! Mult2 Bin3 == Bin6Mult2 Bin3 == Bin6 :: Bool= 'TruebinPredecessor type family..:kind! Pred BP.BinP1Pred BP.BinP1 :: Bin= 'BZ:kind! Pred BP.BinP5 == Bin4Pred BP.BinP5 == Bin4 :: Bool= 'True:kind! Pred BP.BinP8 == Bin7Pred BP.BinP8 == Bin7 :: Bool= 'True:kind! Pred BP.BinP6 == Bin5Pred BP.BinP6 == Bin5 :: Bool= 'TruebinSuccessor type family.:kind! Succ Bin5Succ Bin5 :: Bin= 'BP ('B0 ('B1 'BE))  :: " -> " ` :: " ->  ` ::  -> " binMultiply by two and add one.:kind! Mult2Plus1 Bin0Mult2Plus1 Bin0 :: BinP= 'BE:kind! Mult2Plus1 Bin4 == BinP9 Mult2Plus1 Bin4 == BinP9 :: Bool= 'TruebinMultiply by two.:kind! Mult2 Bin0 == Bin0Mult2 Bin0 == Bin0 :: Bool= 'True:kind! Mult2 Bin3 == Bin6Mult2 Bin3 == Bin6 :: Bool= 'Truebin 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))))binConvert from GHC .:kind! FromGHC 7FromGHC 7 :: Bin= 'BP ('B1 ('B1 'BE))binConvert to GHC .:kind! ToGHC Bin5ToGHC Bin5 :: GHC.Nat...= 5binbin 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 ".binbinbinbinbinbinP(0)binP(1)bin\forall b. P(b) \to P(2b)bin\forall b. P(b) \to P(2b + 1)--Safe'(/23>?# 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 FS, 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]binbinbinbin%position is either at the last digit;binsomewhere herebinor there, if the bit is one;binor only there if it is none.Safe'(/23>?( bin is to " is what Fin is to Nat.7The name is picked, as the lack of better 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 FS, 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]?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~z{|}~ddXZ[] bin-0.1.2-5ApLNRqvUQQ8M7x7E9aHxI Data.BinPData.BinData.WrdData.Type.BinP Data.Type.BinData.BinP.PosP Data.Bin.PosTrustworthyCompatBinPBEB0B1 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 $fDataBinWrdWEW0W1testBitclearBitsetBit complementBit complement complement2.&..|.xorshiftRshiftLrotateRrotateLpopCountshiftL1shiftR1rotateL1rotateR1universe $fFunctionWrd$fCoArbitraryWrd$fArbitraryWrd$fFiniteBitsWrd $fBitsWrd$fNumWrd $fBoundedWrd $fHashableWrd $fNFDataWrd $fShowWrd$fOrdWrd$fEqWrdBinP9BinP8BinP7BinP6BinP5BinP4BinP3BinP2BinP1PlusSuccToNatFromGHCToGHCEqBinPSBinPIsbinpSBinPSBESB0SB1 withSBinPreifyreflect reflectToNum sbinpToBinPsbinpToNaturaleqBinPwithSucc induction$fGEqBinPSBinP$fGNFDataBinPSBinP $fNFDataSBinP$fGShowBinPSBinP $fBoringSBinP$fTestEqualityBinPSBinP $fSBinPIB1 $fSBinPIB0 $fSBinPIBE $fShowSBinPBin9Bin8Bin7Bin6Bin5Bin4Bin3Bin2Bin1Bin0PredSucc''Succ' Mult2Plus1Mult2FromNatEqBinSBinIsbinSBinSBZSBPwithSBin sbinToBin sbinToNaturaleqBin $fGEqBinSBin$fGNFDataBinSBin $fNFDataSBin$fGShowBinSBin$fTestEqualityBinSBin $fBoringSBin $fSBinIBP $fSBinIBZ $fShowSBinPosP'AtEndHereThere1There0PosPunPosP explicitShow'explicitShowsPrec' toNatural'boringtoppop weakenRight1 weakenRight1' universe'$fFunctionPosP'$fCoArbitraryPosP' $fNFDataPosP'$fBoundedPosP' $fShowPosP' $fOrdPosP' $fBoringPosP$fFunctionPosP$fCoArbitraryPosP$fArbitraryPosP $fNFDataPosP $fBoundedPosP $fShowPosP$fArbitraryPosP'$fEqPosP $fOrdPosP $fEqPosP'Posabsurd $fAbsurdPos $fBoringPos $fFunctionPos$fCoArbitraryPos$fArbitraryPos $fNFDataPos $fBoundedPos $fShowPos$fOrdPos$fEqPosbaseGHC.Showshow showsPrecfin-0.2.1-3oDnWsPrUnxOWzFV6M5KlData.NatNat Data.Bits GHC.NaturalNaturalGHC.NumNumghc-primGHC.PrimcoerceData.Type.Equality:~:Refl TestEquality testEquality== GHC.TypesZ