Safe Haskell	None
Language	Haskell2010

Data.Type.Bin

Contents

Singleton
Implicit
Type equality
Induction
Arithmetic
- Successor
- Predecessor
- Addition
- Extras
Conversions
- To GHC Nat
- To fin Nat
Aliases

Description

Binary natural numbers. DataKinds stuff.

Synopsis

data SBin (b :: Bin ) where
- SBZ :: SBin ' BZ
- SBP :: SBinPI b => SBin (' BP b)
data SBinP (b :: BinP ) where
- SBE :: SBinP ' BE
- SB0 :: SBinPI b => SBinP (' B0 b)
- SB1 :: SBinPI b => SBinP (' B1 b)
sbinToBin :: forall n. SBin n -> Bin
sbinpToBinP :: forall n. SBinP n -> BinP
sbinToNatural :: forall n. SBin n -> Natural
sbinpToNatural :: forall n. SBinP n -> Natural
class SBinI (b :: Bin ) where
- sbin :: SBin b
class SBinPI (b :: BinP ) where
- sbinp :: SBinP b
withSBin :: SBin b -> ( SBinI b => r) -> r
withSBinP :: SBinP b -> ( SBinPI b => r) -> r
reify :: forall r. Bin -> ( forall b. SBinI b => Proxy b -> r) -> r
reflect :: forall b proxy. SBinI b => proxy b -> Bin
reflectToNum :: forall b proxy a. ( SBinI b, Num a) => proxy b -> a
eqBin :: forall a b. ( SBinI a, SBinI b) => Maybe (a :~: b)
induction :: forall b f. SBinI b => f ' BZ -> f (' BP ' BE ) -> ( forall bb. SBinPI bb => f (' BP bb) -> f (' BP (' B0 bb))) -> ( forall bb. SBinPI bb => f (' BP bb) -> f (' BP (' B1 bb))) -> f b
type Succ b = ' BP ( Succ' b)
type family Succ' (b :: Bin ) :: BinP where ...
type Succ'' b = ' BP ( Succ b)
withSucc :: forall b r. SBinI b => Proxy b -> ( SBinPI ( Succ' b) => r) -> r
type family Pred (b :: BinP ) :: Bin where ...
type family Plus (a :: Bin ) (b :: Bin ) :: Bin where ...
type family Mult2 (b :: Bin ) :: Bin where ...
type family Mult2Plus1 (b :: Bin ) :: BinP where ...
type family ToGHC (b :: Bin ) :: Nat where ...
type family FromGHC (n :: Nat ) :: Bin where ...
type family ToNat (b :: Bin ) :: Nat where ...
type family FromNat (n :: Nat ) :: Bin where ...
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

Singleton

data SBin (b :: Bin ) where Source #

Singleton of Bin .

Constructors

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

Instances

Instances details

TestEquality SBin Source #
Instance details Defined in Data.Type.Bin Methods testEquality :: forall (a :: k) (b :: k). SBin a -> SBin b -> Maybe (a :~: b) Source #

data SBinP (b :: BinP ) where Source #

Singleton of BinP .

Constructors

SBE :: SBinP ' BE
SB0 :: SBinPI b => SBinP (' B0 b)
SB1 :: SBinPI b => SBinP (' B1 b)

Instances

Instances details

TestEquality SBinP Source #
Instance details Defined in Data.Type.BinP Methods testEquality :: forall (a :: k) (b :: k). SBinP a -> SBinP b -> Maybe (a :~: b) Source #

sbinToBin :: forall n. SBin n -> Bin Source #

Convert SBin to Bin .

sbinpToBinP :: forall n. SBinP n -> BinP Source #

Cconvert SBinP to BinP .

sbinToNatural :: forall n. SBin n -> Natural Source #

Convert SBin to Natural .

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

sbinpToNatural :: forall n. SBinP n -> Natural Source #

Convert SBinP to Natural .

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

Implicit

class SBinI (b :: Bin ) where Source #

Let constraint solver construct SBin .

Methods

sbin :: SBin b Source #

Instances

Instances details

SBinI ' BZ Source #
Instance details Defined in Data.Type.Bin Methods sbin :: SBin ' BZ Source #
SBinPI b => SBinI (' BP b) Source #
Instance details Defined in Data.Type.Bin Methods sbin :: SBin (' BP b) Source #

class SBinPI (b :: BinP ) where Source #

Let constraint solver construct SBinP .

Methods

sbinp :: SBinP b Source #

Instances

Instances details

SBinPI ' BE Source #
Instance details Defined in Data.Type.BinP Methods sbinp :: SBinP ' BE Source #
SBinPI b => SBinPI (' B0 b) Source #
Instance details Defined in Data.Type.BinP Methods sbinp :: SBinP (' B0 b) Source #
SBinPI b => SBinPI (' B1 b) Source #
Instance details Defined in Data.Type.BinP Methods sbinp :: SBinP (' B1 b) Source #

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

Construct SBinI dictionary from SBin .

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

Construct SBinPI dictionary from SBinP .

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

Reify Bin

>>> reify bin3 reflect
3

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

Reflect type-level Bin to the term level.

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

Reflect type-level Bin to the term level Num .

Type equality

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

Induction

induction Source #

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) Source #

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 ... Source #

Equations

Succ' ' BZ = ' BE
Succ' (' BP b) = Succ b

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

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

Predecessor

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

Predecessor type family..

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

>>> :kind! Pred BP.BinP5
Pred BP.BinP5 :: Bin
= 'BP ('B0 ('B0 BP.BinP1))

>>> :kind! Pred BP.BinP8
Pred BP.BinP8 :: Bin
= 'BP ('B1 ('B1 'BE))

>>> :kind! Pred BP.BinP6
Pred BP.BinP6 :: Bin
= 'BP ('B1 ('B0 'BE))

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 ... Source #

Addition.

>>> :kind! Plus Bin7 Bin7
Plus Bin7 Bin7 :: Bin
= 'BP ('B0 ('B1 ('B1 'BE)))

>>> :kind! Mult2 Bin7
Mult2 Bin7 :: Bin
= 'BP ('B0 ('B1 BinP3))

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 ... Source #

Multiply by two.

>>> :kind! Mult2 Bin0
Mult2 Bin0 :: Bin
= 'BZ

>>> :kind! Mult2 Bin7
Mult2 Bin7 :: Bin
= 'BP ('B0 ('B1 BinP3))

Equations

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

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

Multiply by two and add one.

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

>>> :kind! Mult2Plus1 Bin5
Mult2Plus1 Bin5 :: BinP
= 'B1 ('B1 BinP2)

Equations

Mult2Plus1 ' BZ = ' BE
Mult2Plus1 (' BP n) = ' B1 n

Conversions

To GHC Nat

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

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 ... Source #

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 ... Source #

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 ... Source #

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 Source #

type Bin1 = ' BP BinP1 Source #

type Bin2 = ' BP BinP2 Source #

type Bin3 = ' BP BinP3 Source #

type Bin4 = ' BP BinP4 Source #

type Bin5 = ' BP BinP5 Source #

type Bin6 = ' BP BinP6 Source #

type Bin7 = ' BP BinP7 Source #

type Bin8 = ' BP BinP8 Source #

type Bin9 = ' BP BinP9 Source #