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

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

data PosP (b :: BinP) Source #

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

Instances

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

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