Data.Type.BinP

Positive binary natural numbers. DataKinds stuff.

Singleton

data SBinP (b :: BinP) where

Singleton of BinP.

Constructors

SBE :: SBinP 'BE

SB0 :: SBinPI b => SBinP ('B0 b)

SB1 :: SBinPI b => SBinP ('B1 b)

Instances

TestEquality SBinP

Defined in Data.Type.BinP

Methods

testEquality :: forall (a :: k) (b :: k). SBinP a -> SBinP b -> Maybe (a :~: b)

sbinpToBinP :: forall n. SBinP n -> BinP

Cconvert SBinP to BinP.

sbinpToNatural :: forall n. SBinP n -> Natural

Convert SBinP to Natural.

>>> sbinpToNatural (sbinp :: SBinP BinP8)
8

Implicit

class SBinPI (b :: BinP) where

Let constraint solver construct SBinP.

Methods

sbinp :: SBinP b

Instances

SBinPI 'BE

Defined in Data.Type.BinP

Methods

sbinp :: SBinP 'BE

SBinPI b => SBinPI ('B0 b)

Defined in Data.Type.BinP

Methods

sbinp :: SBinP ('B0 b)

SBinPI b => SBinPI ('B1 b)

Defined in Data.Type.BinP

Methods

sbinp :: SBinP ('B1 b)

withSBinP :: SBinP b -> (SBinPI b => r) -> r

Construct SBinPI dictionary from SBinP.

reify :: forall r. BinP -> (forall b. SBinPI b => Proxy b -> r) -> r

Reify BinP.

reflect :: forall b proxy. SBinPI b => proxy b -> BinP

Reflect type-level BinP to the term level.

reflectToNum :: forall b proxy a. (SBinPI b, Num a) => proxy b -> a

Reflect type-level BinP to the term level Num.

Type equality

eqBinP :: forall a b. (SBinPI a, SBinPI b) => Maybe (a :~: b)

Induction

induction

Arguments

:: forall b f. SBinPI b

=> f 'BE

\(P(1)\)

-> (forall bb. SBinPI bb => f bb -> f ('B0 bb))

\(\forall b. P(b) \to P(2b)\)

-> (forall bb. SBinPI bb => f bb -> f ('B1 bb))

\(\forall b. P(b) \to P(2b + 1)\)

-> f b

Induction on BinP.

Arithmetic

Successor

type family Succ (b :: BinP) :: BinP where ...

Equations

Succ 'BE = 'B0 'BE

Succ ('B0 n) = 'B1 n

Succ ('B1 n) = 'B0 (Succ n)

withSucc :: forall b r. SBinPI b => Proxy b -> (SBinPI (Succ b) => r) -> r

Addition

type family Plus (a :: BinP) (b :: BinP) :: BinP where ...

Equations

Plus 'BE b = Succ b

Plus a 'BE = Succ a

Plus ('B0 a) ('B0 b) = 'B0 (Plus a b)

Plus ('B1 a) ('B0 b) = 'B1 (Plus a b)

Plus ('B0 a) ('B1 b) = 'B1 (Plus a b)

Plus ('B1 a) ('B1 b) = 'B0 (Succ (Plus a b))

Conversions

To GHC Nat

type family ToGHC (b :: BinP) :: Nat where ...

Equations

ToGHC 'BE = 1

ToGHC ('B0 b) = 2 * ToGHC b

ToGHC ('B1 b) = 1 + (2 * ToGHC b)

type family FromGHC (n :: Nat) :: BinP where ...

Equations

FromGHC n = FromGHC' (FromGHCMaybe n)

To fin Nat

type family ToNat (b :: BinP) :: Nat where ...

Equations

ToNat 'BE = 'S 'Z

ToNat ('B0 b) = Mult2 (ToNat b)

ToNat ('B1 b) = 'S (Mult2 (ToNat b))

Aliases

type BinP1 = 'BE

type BinP2 = 'B0 BinP1

type BinP3 = 'B1 BinP1

type BinP4 = 'B0 BinP2

type BinP5 = 'B1 BinP2

type BinP6 = 'B0 BinP3

type BinP7 = 'B1 BinP3

type BinP8 = 'B0 BinP4

type BinP9 = 'B1 BinP4