Safe Haskell	None
Language	Haskell2010

Data.Bin.Pos

Contents

Top & Pop
Showing
Conversions
Interesting
Weakening (succ)
Universe

Synopsis

data Pos (b :: Bin ) where
- Pos :: PosP b -> Pos (' BP b)
data PosP (b :: BinP )
top :: SBinPI b => Pos (' BP b)
pop :: ( SBinPI a, Pred b ~ ' BP a, Succ a ~ b) => Pos (' BP a) -> Pos (' BP b)
explicitShow :: Pos b -> String
explicitShowsPrec :: Int -> Pos b -> ShowS
toNatural :: Pos b -> Natural
absurd :: Pos ' BZ -> b
boring :: Pos (' BP ' BE )
weakenRight1 :: SBinPI b => Pos (' BP b) -> Pos ( Succ'' b)
universe :: forall b. SBinI b => [ Pos b]

Documentation

data Pos (b :: Bin ) where Source #

Pos is to Bin is what Fin is to Nat .

The name is picked, as sthe lack of beter alternatives.

Constructors

Pos :: PosP b -> Pos (' BP b)

Instances

Instances details

( SBinPI n, b ~ ' BP n) => Bounded ( Pos b) Source #	`>>>` `minBound < (maxBound :: Pos Bin5)`True
Instance details Defined in Data.Bin.Pos Methods minBound :: Pos b Source # maxBound :: Pos b Source #
Eq ( Pos b) Source #
Instance details Defined in Data.Bin.Pos Methods (==) :: Pos b -> Pos b -> Bool Source # (/=) :: Pos b -> Pos b -> Bool Source #
Ord ( Pos b) Source #
Instance details Defined in Data.Bin.Pos Methods compare :: Pos b -> Pos b -> Ordering Source # (<) :: Pos b -> Pos b -> Bool Source # (<=) :: Pos b -> Pos b -> Bool Source # (>) :: Pos b -> Pos b -> Bool Source # (>=) :: Pos b -> Pos b -> Bool Source # max :: Pos b -> Pos b -> Pos b Source # min :: Pos b -> Pos b -> Pos b Source #
Show ( Pos b) Source #
Instance details Defined in Data.Bin.Pos Methods showsPrec :: Int -> Pos b -> ShowS Source # show :: Pos b -> String Source # showList :: [ Pos b] -> ShowS Source #
( SBinPI n, b ~ ' BP n) => Function ( Pos b) Source #
Instance details Defined in Data.Bin.Pos Methods function :: ( Pos b -> b0) -> Pos b :-> b0 Source #
( SBinPI n, b ~ ' BP n) => Arbitrary ( Pos b) Source #
Instance details Defined in Data.Bin.Pos Methods arbitrary :: Gen ( Pos b) Source # shrink :: Pos b -> [ Pos b] Source #
CoArbitrary ( Pos b) Source #
Instance details Defined in Data.Bin.Pos Methods coarbitrary :: Pos b -> Gen b0 -> Gen b0 Source #

data PosP (b :: BinP ) Source #

PosP is to BinP is what Fin is to Nat , when n is Z .

Instances

Instances details

SBinPI b => Bounded ( PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods minBound :: PosP b Source # maxBound :: PosP b Source #
Eq ( PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods (==) :: PosP b -> PosP b -> Bool Source # (/=) :: PosP b -> PosP b -> Bool Source #
Ord ( PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods compare :: PosP b -> PosP b -> Ordering Source # (<) :: PosP b -> PosP b -> Bool Source # (<=) :: PosP b -> PosP b -> Bool Source # (>) :: PosP b -> PosP b -> Bool Source # (>=) :: PosP b -> PosP b -> Bool Source # max :: PosP b -> PosP b -> PosP b Source # min :: PosP b -> PosP b -> PosP b Source #
Show ( PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods showsPrec :: Int -> PosP b -> ShowS Source # show :: PosP b -> String Source # showList :: [ PosP b] -> ShowS Source #
SBinPI b => Function ( PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods function :: ( PosP b -> b0) -> PosP b :-> b0 Source #
SBinPI b => Arbitrary ( PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods arbitrary :: Gen ( PosP b) Source # shrink :: PosP b -> [ PosP b] Source #
CoArbitrary ( PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods coarbitrary :: PosP b -> Gen b0 -> Gen b0 Source #

Top & Pop

top :: SBinPI b => Pos (' BP b) Source #

top and pop serve as FZ and FS , with types specified so type-inference works backwards from the result.

>>> top :: Pos Bin4
0

>>> pop (pop top) :: Pos Bin4
2

>>> pop (pop top) :: Pos Bin9
2

pop :: ( SBinPI a, Pred b ~ ' BP a, Succ a ~ b) => Pos (' BP a) -> Pos (' BP b) Source #

See top .

Showing

explicitShow :: Pos b -> String Source #

explicitShowsPrec :: Int -> Pos b -> ShowS Source #

Conversions

toNatural :: Pos b -> Natural Source #

Convert Pos to Natural

>>> map toNatural (universe :: [Pos Bin7])
[0,1,2,3,4,5,6]

Interesting

absurd :: Pos ' BZ -> b Source #

Pos BZ is not inhabited.

boring :: Pos (' BP ' BE ) Source #

Counting to one is boring

>>> boring
0

Weakening (succ)

weakenRight1 :: SBinPI b => Pos (' BP b) -> Pos ( Succ'' b) Source #

Like FS for Fin .

Some tests:

>>> map weakenRight1 $ (universe :: [Pos Bin2])
[1,2]

>>> map weakenRight1 $ (universe :: [Pos Bin3])
[1,2,3]

>>> map weakenRight1 $ (universe :: [Pos Bin4])
[1,2,3,4]

>>> map weakenRight1 $ (universe :: [Pos Bin5])
[1,2,3,4,5]

>>> map weakenRight1 $ (universe :: [Pos Bin6])
[1,2,3,4,5,6]

Universe

universe :: forall b. SBinI b => [ Pos b] Source #

Universe, i.e. all [Pos b]

>>> universe :: [Pos Bin9]
[0,1,2,3,4,5,6,7,8]

>>> traverse_ (putStrLn . explicitShow) (universe :: [Pos Bin5])
Pos (PosP (Here WE))
Pos (PosP (There1 (There0 (AtEnd 0b00))))
Pos (PosP (There1 (There0 (AtEnd 0b01))))
Pos (PosP (There1 (There0 (AtEnd 0b10))))
Pos (PosP (There1 (There0 (AtEnd 0b11))))