úÎ!>ê;~<      !"#$%&'()*+,-./0123456789:;Singletons for GHC TypeLits(C) 2017-2018 mniipMITmniip@mniip.comstableportable Trustworthy &',-.0FQSTV ‘ singleton-typelits'A positive number is either a digit in [1, b)#, or another positive number times b plus a digit in [0, b). For example, 123 = 3 + 10 * (2 + 10 * 1): vBaseDigit (natSingleton :: p 3) (BaseDigit (natSingleton :: p 2) (BaseLead (natSingleton :: p 1))) :: PosBase p 10 123singleton-typelitsLA positive number is either 1, or twice another positive number plus 0 or 1. For example, "10 = 0 + 2 * (1 + 2 * (0 + 2 * 1)): )Bin0 (Bin1 (Bin0 BinOne)) :: PosBinary 10singleton-typelitsHA positive number is either 1 or a successor of another positive number. For example, 5 = 1 + (1 + (1 + (1 + 1))): AUnarySucc (UnarySucc (UnarySucc (UnarySucc UnaryOne))) :: Unary 5 singleton-typelits6A class of singletons capable of representing postive < natural numbers. singleton-typelits!A natural number is either 0, or b. times another natural number plus a digit in [1, b]. For example, 8123 = (2 + 1) + 10 * ((1 + 1) + 10 * ((0 + 1) + 10 * 0)): ”BaseCompxBp1p (natSingleton :: p 2) (BaseCompxBp1p (natSingleton :: p 1) (BaseCompxBp1p (natSingleton :: p 0) BaseCompZero)) :: NatBaseComp p 10 123singleton-typelitsJA natural number is either 0, or twice another natural number plus 1 or 2. For example, "12 = 2 + 2 * (1 + 2 * (2 + 2 * 0)): ITwosCompx2p2 (TwosCompx2p1 (TwosCompx2p2 TwosCompZero)) :: NatTwosComp 12singleton-typelitsFA natural number is either 0 or a successor of another natural number. For example, 3 = 1 + (1 + (1 + 0)): 9PeanoSucc (PeanoSucc (PeanoSucc PeanoZero)) :: NatPeano 3singleton-typelits1A natural number is either 0 or 1 plus something.singleton-typelits!Auxiliary class for implementing = on higher-kinded singletons.singleton-typelits2A class of singletons capable of representing any < natural number.    Induction for GHC TypeLits(C) 2017-2018 mniipMITmniip@mniip.comstableportableSafe &',-.0FQSTV;B5singleton-typelits8(\forall n. n > 0 \to P(n)) \to P(0) \to \forall m. P(m)6singleton-typelits;(\forall n. P(n) \to P(n + 1)) \to P(0) \to \forall m. P(m) For example: $inducePeano f z :: p 3 = f (f (f z))7singleton-typelitsi(\forall n. P(n) \to P(2n + 1)) \to \\ (\forall n. P(n) \to P(2n + 2)) \to \\ P(0) \to \\ \forall m. P(m) For example: /induceTwosComp f1 f2 z :: p 12 = f2 (f1 (f2 z))8singleton-typelitsy\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d + 1)) \to \\ \forall m. P(m) For example: hinduceBaseComp (_ :: s q) (_ :: r 10) d f z :: p 123 = (d :: q 2) `f` ((d :: q 1) `f` ((d :: q 0) `f` z)The s qA parameter is necessary because presently GHC is unable to unify q! under the equational constraint  1 + k <= b.9singleton-typelits?(\forall n. P(n) \to P(n + 1)) \to P(1) \to \forall m > 0. P(m) For example: (induceUnary f o :: p 5 = f (f (f (f o))):singleton-typelitsi(\forall n. P(n) \to P(2n)) \to \\ (\forall n. P(n) \to P(2n + 1)) \to \\ P(1) \to \\ \forall m > 0. P(m) For example: 0inducePosBinary f0 f1 o :: p 10 = f0 (f1 (f0 o));singleton-typelits°\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d)) \to \\ (\forall d. d > 0 \to d < b \to Q(d) \to P(d)) \to \\ \forall m > 0. P (m) For example: binducePosBase (_ :: s q) (_ :: r 10) d f l :: p 123 = (d :: q 3) `f` ((d :: q 2) `f` l (d :: q 1))The s qA parameter is necessary because presently GHC is unable to unify q! under the equational constraint  1 + k <= b.56789:;56789:;>      !"#$%&'()*+,-./0123456789:;<=>?@A?BCD1singleton-typelits-0.1.0.0-ALJAxvhJvoyAwDkdrpL8V7GHC.TypeLits.SingletonsGHC.TypeLits.InductionPosBaseBaseLead BaseDigit PosBinaryBinOneBin0Bin1UnaryUnaryOne UnarySuccPositiveSingleton posSingleton NatBaseComp BaseCompZero BaseCompxBp1p NatTwosComp TwosCompZero TwosCompx2p1 TwosCompx2p2NatPeano PeanoZero PeanoSucc NatIsZeroIsZero IsNonZeroShowN showsPrecN NatSingleton natSingleton$fNatSingletonProxy $fShowNProxy$fNatSingletonNatIsZero$fShowNNatIsZero$fNatSingletonNatPeano$fShowNNatPeano$fNatSingletonNatTwosComp$fShowNNatTwosComp$fNatSingletonNatBaseComp$fShowNNatBaseComp$fShowNatBaseComp$fPositiveSingletonProxy$fPositiveSingletonUnary $fShowNUnary$fPositiveSingletonPosBinary$fShowNPosBinary$fPositiveSingletonPosBase$fShowNPosBase $fShowPosBase$fShowPosBinary $fShowUnary$fShowNatTwosComp$fShowNatPeano$fShowNatIsZero induceIsZero inducePeanoinduceTwosCompinduceBaseComp induceUnaryinducePosBinary inducePosBasebase GHC.TypeNatsKnownNatGHC.ShowShow