Data.Type.Bin · bin-0.1.4 · horizon-platform

Singleton

6 declarations

datadata SBin (b :: Bin) where

#

Singleton of Bin.

Constructors

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

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

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

datadata SBinP (b :: BinP) where

#

Singleton of BinP.

Constructors

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

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

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

valuesbinToBin :: SBin n -> Bin

#

Convert SBin to Bin.

valuesbinpToBinP :: SBinP n -> BinP

#

Cconvert SBinP to BinP.

valuesbinToNatural :: SBin n -> Natural

#

Convert SBin to Natural.

Example1 expression

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

valuesbinpToNatural :: SBinP n -> Natural

#

Convert SBinP to Natural.

Example1 expression

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

Implicit

7 declarations

classclass SBinI (b :: Bin) where

#

Let constraint solver construct SBin.

Methods

sbin :: SBin b

Instances2SBinI

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

classclass SBinPI (b :: BinP) where

#

Let constraint solver construct SBinP.

Methods

sbinp :: SBinP b

Instances3SBinPI

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

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

#

Construct SBinI dictionary from SBin.

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

#

Construct SBinPI dictionary from SBinP.

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

#

Reify Bin

Example1 expression

>>> reify bin3 reflect3

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

#

Reflect type-level Bin to the term level.

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

#

Reflect type-level Bin to the term level Num.

Type equality

2 declarations

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

#

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

#

Equations

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

Induction

1 declaration

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

#

Induction on Bin.

Arithmetic

0 declarations

Successor

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

#

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

#

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

#

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

#

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

#

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

0 declarations

To GHC Nat

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

#

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

#

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

#

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

#

Convert from fin Nat.

Example1 expression

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

Equations

FromNat n = FromNat' (DivMod2 n)

Aliases

10 declarations

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

#