Modulebin-0.1.4.1Haskell2010

Data.Type.BinP

Positive binary natural numbers. DataKinds stuff.

Contents

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

Synopsis

data SBinP
value sbinpToBinP
value sbinpToNatural
class SBinPI
value withSBinP
value reify
value reflect
value reflectToNum
value eqBinP
family EqBinP
value induction
family Succ
value withSucc
family Plus
family ToGHC
family FromGHC
family ToNat
type BinP1
type BinP2
type BinP3
type BinP4
type BinP5
type BinP6
type BinP7
type BinP8
type BinP9

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

Singleton

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

valuesbinpToBinP :: SBinP n -> BinP

Source#

Cconvert SBinP to BinP.

valuesbinpToNatural :: SBinP n -> Natural

Source#

Convert SBinP to Natural.

Example1 expression

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

Implicit

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

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

Source#

Construct SBinPI dictionary from SBinP.

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

Source#

Reify BinP.

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

Source#

Reflect type-level BinP to the term level.

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

Source#

Reflect type-level BinP to the term level Num.

Type equality

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

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

Source#

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

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

Source#

Induction on BinP.

Arithmetic

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

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

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