Modulebin-0.1.4.1Haskell2010

Data.Type.Bin

Binary natural numbers. DataKinds stuff.

Contents

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

Synopsis

data SBin
data SBinP
value sbinToBin
value sbinpToBinP
value sbinToNatural
value sbinpToNatural
class SBinI
class SBinPI
value withSBin
value withSBinP
value reify
value reflect
value reflectToNum
value eqBin
family EqBin
value induction
type Succ
family Succ'
type Succ''
value withSucc
family Pred
family Plus
family Mult2
family Mult2Plus1
family ToGHC
family FromGHC
family ToNat
family FromNat
type Bin0
type Bin1
type Bin2
type Bin3
type Bin4
type Bin5
type Bin6
type Bin7
type Bin8
type Bin9

Packagebin-0.1.4.1
Exports38
LanguageHaskell2010
LicenceGPL-2.0-or-later
SourceBin.hs

Singleton

datadata SBin (b :: Bin) where

Source#

Singleton of Bin.

Constructors

SBZ :: SBin 'BZ
SBP :: SBinPI b => SBin b

Instances10TestEquality, EqP, GEq, GNFData, GShow, Eq, …

TestEquality SBinDefined in bin-0.1.4.1 · Data.Type.Bin
EqP SBinDefined in bin-0.1.4.1 · Data.Type.Bin
GEq SBinDefined in bin-0.1.4.1 · Data.Type.Bin
GNFData SBinDefined in bin-0.1.4.1 · Data.Type.Bin
GShow SBinDefined in bin-0.1.4.1 · Data.Type.Bin
Eq (SBin a)Defined in bin-0.1.4.1 · Data.Type.Bin
Ord (SBin a)Defined in bin-0.1.4.1 · Data.Type.Bin
Show (SBin b)Defined in bin-0.1.4.1 · Data.Type.Bin
NFData (SBin n)Defined in bin-0.1.4.1 · Data.Type.Bin
SBinI b => Boring (SBin b)Defined in bin-0.1.4.1 · Data.Type.Bin

datadata SBinP (b :: BinP) where

Source#

Singleton of BinP.

Constructors

SBE :: SBinP 'BE
SB0 :: SBinPI b => SBinP b
SB1 :: SBinPI b => SBinP b

Instances10TestEquality, EqP, GEq, GNFData, GShow, Eq, …

TestEquality SBinPDefined in bin-0.1.4.1 · Data.Type.BinP
EqP SBinPDefined in bin-0.1.4.1 · Data.Type.BinP
GEq SBinPDefined in bin-0.1.4.1 · Data.Type.BinP
GNFData SBinPDefined in bin-0.1.4.1 · Data.Type.BinP
GShow SBinPDefined in bin-0.1.4.1 · Data.Type.BinP
Eq (SBinP a)Defined in bin-0.1.4.1 · Data.Type.BinP
Ord (SBinP a)Defined in bin-0.1.4.1 · Data.Type.BinP
Show (SBinP b)Defined in bin-0.1.4.1 · Data.Type.BinP
NFData (SBinP n)Defined in bin-0.1.4.1 · Data.Type.BinP
SBinPI b => Boring (SBinP b)Defined in bin-0.1.4.1 · Data.Type.BinP

valuesbinToBin :: SBin n -> Bin

Source#

Convert SBin to Bin.

valuesbinpToBinP :: SBinP n -> BinP

Source#

Cconvert SBinP to BinP.

valuesbinToNatural :: SBin n -> Natural

Source#

Convert SBin to Natural.

Example1 expression

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

valuesbinpToNatural :: SBinP n -> Natural

Source#

Convert SBinP to Natural.

Example1 expression

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

Implicit

classclass SBinI (b :: Bin) where

Source#

Let constraint solver construct SBin.

Methods

sbin :: SBin b

Instances2SBinI

SBinI 'BZDefined in bin-0.1.4.1 · Data.Type.Bin
SBinPI b => SBinI ('BP b)Defined in bin-0.1.4.1 · Data.Type.Bin

classclass SBinPI (b :: BinP) where

Source#

Let constraint solver construct SBinP.

Methods

sbinp :: SBinP b

Instances3SBinPI

SBinPI 'BEDefined in bin-0.1.4.1 · Data.Type.BinP
SBinPI b => SBinPI ('B0 b)Defined in bin-0.1.4.1 · Data.Type.BinP
SBinPI b => SBinPI ('B1 b)Defined in bin-0.1.4.1 · Data.Type.BinP

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

Source#

Construct SBinI dictionary from SBin.

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

Source#

Construct SBinPI dictionary from SBinP.

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

Source#

Reify Bin

Example1 expression

>>> reify bin3 reflect3

valuereflect :: SBinI b => proxy b -> Bin

Source#

Reflect type-level Bin to the term level.

valuereflectToNum :: (SBinI b, Num a) => proxy b -> a

Source#

Reflect type-level Bin to the term level Num.

Type equality

valueeqBin :: (SBinI a, SBinI b) => Maybe (a :~: b)

familytype family EqBin (n :: Bin) (m :: Bin) :: Bool where

Source#

Equations

EqBin 'BZ 'BZ = 'True
EqBin ('BP n) ('BP m) = EqBinP n m
EqBin n m = 'False

Induction

valueinduction

:: SBinI b
=> f 'BZ
P(0)
-> f ('BP 'BE)
P(1)
-> (forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B0 bb)))
\forall b. P(b) \to P(2b)
-> (forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B1 bb)))
\forall b. P(b) \to P(2b + 1)
-> f b

Source#

Induction on Bin.

Arithmetic

Successor

typetype Succ (b :: Bin) = 'BP (Succ' b)

Source#

Successor type family.

Example1 expression

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

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

familytype family Succ' (b :: Bin) :: BinP where

Equations

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

typetype Succ'' (b :: BinP) = 'BP (Succ b)

valuewithSucc :: SBinI b => Proxy b -> (SBinPI (Succ' b) => r) -> r

Predecessor

familytype family Pred (b :: BinP) :: Bin where

Source#

Predecessor type family..

Example1 expression

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

Example1 expression

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

Example1 expression

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

Example1 expression

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

Equations

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

Addition

familytype family Plus (a :: Bin) (b :: Bin) :: Bin where

Source#

Addition.

Example1 expression

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

Example1 expression

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

Equations

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

Extras

familytype family Mult2 (b :: Bin) :: Bin where

Source#

Multiply by two.

Example1 expression

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

Example1 expression

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

Equations

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

familytype family Mult2Plus1 (b :: Bin) :: BinP where

Source#

Multiply by two and add one.

Example1 expression

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

Example1 expression

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

Equations

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

Conversions

To GHC Nat

familytype family ToGHC (b :: Bin) :: Nat where

Source#

Convert to GHC Nat.

Example1 expression

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

Equations

ToGHC 'BZ = 0
ToGHC ('BP n) = ToGHC n

familytype family FromGHC (n :: Nat) :: Bin where

Source#

Convert from GHC Nat.

Example1 expression

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

Equations

FromGHC n = FromGHC' (GhcDivMod2 n)

To fin Nat

familytype family ToNat (b :: Bin) :: Nat where

Source#

Convert to fin Nat.

Example1 expression

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

Equations

ToNat 'BZ = 'Z
ToNat ('BP n) = ToNat n

familytype family FromNat (n :: Nat) :: Bin where

Source#

Convert from fin Nat.

Example1 expression

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

Equations

FromNat n = FromNat' (DivMod2 n)

Aliases

typetype Bin0 = 'BZ

typetype Bin1 = 'BP BinP1

typetype Bin2 = 'BP BinP2

typetype Bin3 = 'BP BinP3

typetype Bin4 = 'BP BinP4

typetype Bin5 = 'BP BinP5

typetype Bin6 = 'BP BinP6

typetype Bin7 = 'BP BinP7

typetype Bin8 = 'BP BinP8

typetype Bin9 = 'BP BinP9