Modulebin-0.1.4Haskell2010

Data.Type.BinP

Positive binary natural numbers. DataKinds stuff.

10 types
1 class
9 values

Packagebin-0.1.4
Exports26
LanguageHaskell2010
LicenceGPL-2.0-or-later
SourceBinP.hs

Singleton

3 declarations

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

valuesbinpToBinP :: SBinP n -> BinP

Cconvert SBinP to BinP.

valuesbinpToNatural :: SBinP n -> Natural

Convert SBinP to Natural.

Example1 expression

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

Implicit

5 declarations

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

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

Construct SBinPI dictionary from SBinP.

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

Reify BinP.

valuereflect :: SBinPI b => proxy b -> BinP

Reflect type-level BinP to the term level.

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

Reflect type-level BinP to the term level Num.

Type equality

2 declarations

valueeqBinP :: (SBinPI a, SBinPI b) => Maybe (a :~: b)

familytype family EqBinP (n :: BinP) (m :: BinP) :: Bool where

Equations

EqBinP 'BE 'BE = 'True
EqBinP ('B0 n) ('B0 m) = EqBinP n m
EqBinP ('B1 n) ('B1 m) = EqBinP n m
EqBinP n m = 'False

Induction

1 declaration

valueinduction

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

Induction on BinP.

Arithmetic

0 declarations

Successor

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

Equations

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

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

Addition

familytype 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

0 declarations

To GHC Nat

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

Equations

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

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

Equations

FromGHC n = FromGHC' (FromGHCMaybe n)

To fin Nat

familytype 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

9 declarations

typetype BinP1 = 'BE

typetype BinP2 = 'B0 BinP1

typetype BinP3 = 'B1 BinP1

typetype BinP4 = 'B0 BinP2

typetype BinP5 = 'B1 BinP2

typetype BinP6 = 'B0 BinP3

typetype BinP7 = 'B1 BinP3

typetype BinP8 = 'B0 BinP4

typetype BinP9 = 'B1 BinP4