Safe Haskell	Safe
Language	Haskell2010

Data.Type.BinP

Contents

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

Description

Positive binary natural numbers. DataKinds stuff.

Synopsis

data SBinP (b :: BinP) where
- SBE :: SBinP 'BE
- SB0 :: SBinPI b => SBinP ('B0 b)
- SB1 :: SBinPI b => SBinP ('B1 b)
sbinpToBinP :: forall n. SBinP n -> BinP
sbinpToNatural :: forall n. SBinP n -> Natural
class SBinPI (b :: BinP) where
- sbinp :: SBinP b
withSBinP :: SBinP b -> (SBinPI b => r) -> r
reify :: forall r. BinP -> (forall b. SBinPI b => Proxy b -> r) -> r
reflect :: forall b proxy. SBinPI b => proxy b -> BinP
reflectToNum :: forall b proxy a. (SBinPI b, Num a) => proxy b -> a
eqBinP :: forall a b. (SBinPI a, SBinPI b) => Maybe (a :~: b)
type family EqBinP (n :: BinP) (m :: BinP) where ...
induction :: forall b f. SBinPI b => f 'BE -> (forall bb. SBinPI bb => f bb -> f ('B0 bb)) -> (forall bb. SBinPI bb => f bb -> f ('B1 bb)) -> f b
type family Succ (b :: BinP) :: BinP where ...
withSucc :: forall b r. SBinPI b => Proxy b -> (SBinPI (Succ b) => r) -> r
type family Plus (a :: BinP) (b :: BinP) :: BinP where ...
type family ToGHC (b :: BinP) :: Nat where ...
type family FromGHC (n :: Nat) :: BinP where ...
type family ToNat (b :: BinP) :: Nat where ...
type BinP1 = 'BE
type BinP2 = 'B0 BinP1
type BinP3 = 'B1 BinP1
type BinP4 = 'B0 BinP2
type BinP5 = 'B1 BinP2
type BinP6 = 'B0 BinP3
type BinP7 = 'B1 BinP3
type BinP8 = 'B0 BinP4
type BinP9 = 'B1 BinP4

Singleton

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) #
EqP SBinP Source #	Since: 0.1.3
Instance details Defined in Data.Type.BinP Methods eqp :: forall (a :: k) (b :: k). SBinP a -> SBinP b -> Bool #
GNFData SBinP Source #	Since: 0.1.2
Instance details Defined in Data.Type.BinP Methods grnf :: forall (a :: k). SBinP a -> () #
GEq SBinP Source #	Since: 0.1.2
Instance details Defined in Data.Type.BinP Methods geq :: forall (a :: k) (b :: k). SBinP a -> SBinP b -> Maybe (a :~: b) #
GShow SBinP Source #	Since: 0.1.2
Instance details Defined in Data.Type.BinP Methods gshowsPrec :: forall (a :: k). Int -> SBinP a -> ShowS #
Show (SBinP b) Source #
Instance details Defined in Data.Type.BinP Methods showsPrec :: Int -> SBinP b -> ShowS # show :: SBinP b -> String # showList :: [SBinP b] -> ShowS #
SBinPI b => Boring (SBinP b) Source #	Since: 0.1.2
Instance details Defined in Data.Type.BinP Methods boring :: SBinP b #
NFData (SBinP n) Source #	Since: 0.1.2
Instance details Defined in Data.Type.BinP Methods rnf :: SBinP n -> () #
Eq (SBinP a) Source #	Since: 0.1.3
Instance details Defined in Data.Type.BinP Methods (==) :: SBinP a -> SBinP a -> Bool # (/=) :: SBinP a -> SBinP a -> Bool #
Ord (SBinP a) Source #	Since: 0.1.3
Instance details Defined in Data.Type.BinP Methods compare :: SBinP a -> SBinP a -> Ordering # (<) :: SBinP a -> SBinP a -> Bool # (<=) :: SBinP a -> SBinP a -> Bool # (>) :: SBinP a -> SBinP a -> Bool # (>=) :: SBinP a -> SBinP a -> Bool # max :: SBinP a -> SBinP a -> SBinP a # min :: SBinP a -> SBinP a -> SBinP a #

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

Cconvert SBinP to BinP.

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

Convert SBinP to Natural.

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

Implicit

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 #

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

Construct SBinPI dictionary from SBinP.

reify :: forall r. BinP -> (forall b. SBinPI b => Proxy b -> r) -> r Source #

Reify BinP.

reflect :: forall b proxy. SBinPI b => proxy b -> BinP Source #

Reflect type-level BinP to the term level.

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

Reflect type-level BinP to the term level Num.

Type equality

eqBinP :: forall a b. (SBinPI a, SBinPI b) => Maybe (a :~: b) Source #

type family EqBinP (n :: BinP) (m :: BinP) where ... Source #

Since: 0.1.2

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

induction Source #

Arguments

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

Induction on BinP.

Arithmetic

Successor

type family Succ (b :: BinP) :: BinP where ... Source #

Equations

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

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

Addition

type family Plus (a :: BinP) (b :: BinP) :: BinP where ... Source #

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