Data.Type.Bin

Binary natural numbers. DataKinds stuff.

Singleton

data SBin (b :: Bin) where

Singleton of Bin.

Constructors

SBZ :: SBin 'BZ

SBP :: SBinPI b => SBin ('BP b)

Instances

TestEquality SBin

Defined in Data.Type.Bin

Methods

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

EqP SBin

Since: 0.1.3

Defined in Data.Type.Bin

Methods

eqp :: forall (a :: k) (b :: k). SBin a -> SBin b -> Bool

GNFData SBin

Since: 0.1.2

Defined in Data.Type.Bin

Methods

grnf :: forall (a :: k). SBin a -> ()

GEq SBin

Since: 0.1.2

Defined in Data.Type.Bin

Methods

geq :: forall (a :: k) (b :: k). SBin a -> SBin b -> Maybe (a :~: b)

GShow SBin

Since: 0.1.2

Defined in Data.Type.Bin

Methods

gshowsPrec :: forall (a :: k). Int -> SBin a -> ShowS

Show (SBin b)

Defined in Data.Type.Bin

Methods

showsPrec :: Int -> SBin b -> ShowS

show :: SBin b -> String

showList :: [SBin b] -> ShowS

SBinI b => Boring (SBin b)

Since: 0.1.2

Defined in Data.Type.Bin

Methods

boring :: SBin b

NFData (SBin n)

Since: 0.1.2

Defined in Data.Type.Bin

Methods

rnf :: SBin n -> ()

Eq (SBin a)

Since: 0.1.3

Defined in Data.Type.Bin

Methods

(==) :: SBin a -> SBin a -> Bool

(/=) :: SBin a -> SBin a -> Bool

Ord (SBin a)

Since: 0.1.3

Defined in Data.Type.Bin

Methods

compare :: SBin a -> SBin a -> Ordering

(<) :: SBin a -> SBin a -> Bool

(<=) :: SBin a -> SBin a -> Bool

(>) :: SBin a -> SBin a -> Bool

(>=) :: SBin a -> SBin a -> Bool

max :: SBin a -> SBin a -> SBin a

min :: SBin a -> SBin a -> SBin a

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)

EqP SBinP

Since: 0.1.3

Defined in Data.Type.BinP

Methods

eqp :: forall (a :: k) (b :: k). SBinP a -> SBinP b -> Bool

GNFData SBinP

Since: 0.1.2

Defined in Data.Type.BinP

Methods

grnf :: forall (a :: k). SBinP a -> ()

GEq SBinP

Since: 0.1.2

Defined in Data.Type.BinP

Methods

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

GShow SBinP

Since: 0.1.2

Defined in Data.Type.BinP

Methods

gshowsPrec :: forall (a :: k). Int -> SBinP a -> ShowS

Show (SBinP b)

Defined in Data.Type.BinP

Methods

showsPrec :: Int -> SBinP b -> ShowS

show :: SBinP b -> String

showList :: [SBinP b] -> ShowS

SBinPI b => Boring (SBinP b)

Since: 0.1.2

Defined in Data.Type.BinP

Methods

boring :: SBinP b

NFData (SBinP n)

Since: 0.1.2

Defined in Data.Type.BinP

Methods

rnf :: SBinP n -> ()

Eq (SBinP a)

Since: 0.1.3

Defined in Data.Type.BinP

Methods

(==) :: SBinP a -> SBinP a -> Bool

(/=) :: SBinP a -> SBinP a -> Bool

Ord (SBinP a)

Since: 0.1.3

Defined in Data.Type.BinP

Methods

compare :: SBinP a -> SBinP a -> Ordering

(<) :: SBinP a -> SBinP a -> Bool

(<=) :: SBinP a -> SBinP a -> Bool

(>) :: SBinP a -> SBinP a -> Bool

(>=) :: SBinP a -> SBinP a -> Bool

max :: SBinP a -> SBinP a -> SBinP a

min :: SBinP a -> SBinP a -> SBinP a

sbinToBin :: forall n. SBin n -> Bin

Convert SBin to Bin.

sbinpToBinP :: forall n. SBinP n -> BinP

Cconvert SBinP to BinP.

sbinToNatural :: forall n. SBin n -> Natural

Convert SBin to Natural.

>>> sbinToNatural (sbin :: SBin Bin9)
9

sbinpToNatural :: forall n. SBinP n -> Natural

Convert SBinP to Natural.

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

Implicit

class SBinI (b :: Bin) where

Let constraint solver construct SBin.

Methods

sbin :: SBin b

Instances

SBinI 'BZ

Defined in Data.Type.Bin

Methods

sbin :: SBin 'BZ

SBinPI b => SBinI ('BP b)

Defined in Data.Type.Bin

Methods

sbin :: SBin ('BP b)

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)

withSBin :: SBin b -> (SBinI b => r) -> r

Construct SBinI dictionary from SBin.

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

Construct SBinPI dictionary from SBinP.

reify :: forall r. Bin -> (forall b. SBinI b => Proxy b -> r) -> r

Reify Bin

>>> reify bin3 reflect
3

reflect :: forall b proxy. SBinI b => proxy b -> Bin

Reflect type-level Bin to the term level.

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

Reflect type-level Bin to the term level Num.

Type equality

eqBin :: forall a b. (SBinI a, SBinI b) => Maybe (a :~: b)

type family EqBin (n :: Bin) (m :: Bin) where ...

Since: 0.1.2

Equations

EqBin 'BZ 'BZ = 'True

EqBin ('BP n) ('BP m) = EqBinP n m

EqBin n m = 'False

Induction

induction

Arguments

:: forall b f. SBinI b

=> f 'BZ

\(P(0)\)

-> f ('BP 'BE)

\(P(1)\)

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

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

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

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

-> f b

Induction on Bin.

Arithmetic

Successor

type Succ b = 'BP (Succ' b)

Successor type family.

>>> :kind! Succ Bin5
Succ Bin5 :: Bin
= 'BP ('B0 ('B1 'BE))

Succ   :: Bin -> Bin
Succ'  :: Bin -> BinP
Succ'' :: BinP -> Bin

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

Equations

Succ' 'BZ = 'BE

Succ' ('BP b) = Succ b

type Succ'' b = 'BP (Succ b)

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

Predecessor

type family Pred (b :: BinP) :: Bin where ...

Predecessor type family..

>>> :kind! Pred BP.BinP1
Pred BP.BinP1 :: Bin
= 'BZ

>>> :kind! Pred BP.BinP5 == Bin4
Pred BP.BinP5 == Bin4 :: Bool
= 'True

>>> :kind! Pred BP.BinP8 == Bin7
Pred BP.BinP8 == Bin7 :: Bool
= 'True

>>> :kind! Pred BP.BinP6 == Bin5
Pred BP.BinP6 == Bin5 :: Bool
= 'True

Equations

Pred 'BE = 'BZ

Pred ('B1 n) = 'BP ('B0 n)

Pred ('B0 n) = 'BP (Pred' n)

Addition

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

Addition.

>>> :kind! Plus Bin3 Bin3 == Bin6
Plus Bin3 Bin3 == Bin6 :: Bool
= 'True

>>> :kind! Mult2 Bin3 == Bin6
Mult2 Bin3 == Bin6 :: Bool
= 'True

Equations

Plus 'BZ b = b

Plus a 'BZ = a

Plus ('BP a) ('BP b) = 'BP (Plus a b)

Extras

type family Mult2 (b :: Bin) :: Bin where ...

Multiply by two.

>>> :kind! Mult2 Bin0 == Bin0
Mult2 Bin0 == Bin0 :: Bool
= 'True

>>> :kind! Mult2 Bin3 == Bin6
Mult2 Bin3 == Bin6 :: Bool
= 'True

Equations

Mult2 'BZ = 'BZ

Mult2 ('BP n) = 'BP ('B0 n)

type family Mult2Plus1 (b :: Bin) :: BinP where ...

Multiply by two and add one.

>>> :kind! Mult2Plus1 Bin0
Mult2Plus1 Bin0 :: BinP
= 'BE

>>> :kind! Mult2Plus1 Bin4 == BinP9
Mult2Plus1 Bin4 == BinP9 :: Bool
= 'True

Equations

Mult2Plus1 'BZ = 'BE

Mult2Plus1 ('BP n) = 'B1 n

Conversions

To GHC Nat

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

Convert to GHC Nat.

>>> :kind! ToGHC Bin5
ToGHC Bin5 :: GHC.Nat...
= 5

Equations

ToGHC 'BZ = 0

ToGHC ('BP n) = ToGHC n

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

Convert from GHC Nat.

>>> :kind! FromGHC 7
FromGHC 7 :: Bin
= 'BP ('B1 ('B1 'BE))

Equations

FromGHC n = FromGHC' (GhcDivMod2 n)

To fin Nat

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

Convert to fin Nat.

>>> :kind! ToNat Bin5
ToNat Bin5 :: Nat
= 'S ('S ('S ('S ('S 'Z))))

Equations

ToNat 'BZ = 'Z

ToNat ('BP n) = ToNat n

type family FromNat (n :: Nat) :: Bin where ...

Convert from fin Nat.

>>> :kind! FromNat N.Nat5
FromNat N.Nat5 :: Bin
= 'BP ('B1 ('B0 'BE))

Equations

FromNat n = FromNat' (DivMod2 n)

Aliases

type Bin0 = 'BZ

type Bin1 = 'BP BinP1

type Bin2 = 'BP BinP2

type Bin3 = 'BP BinP3

type Bin4 = 'BP BinP4

type Bin5 = 'BP BinP5

type Bin6 = 'BP BinP6

type Bin7 = 'BP BinP7

type Bin8 = 'BP BinP8

type Bin9 = 'BP BinP9