Data.Bin.Pos

Documentation

data Pos (b :: Bin) where

Pos is to Bin is what Fin is to Nat.

The name is picked, as the lack of better alternatives.

Constructors

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

Instances

EqP Pos

>>> eqp (top :: Pos Bin4) (top :: Pos Bin6)
True

>>> let xs = universe @Bin4; ys = universe @Bin6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
[True,False,False,False,False,False]
[False,True,False,False,False,False]
[False,False,True,False,False,False]
[False,False,False,True,False,False]

Since: 0.1.3

Defined in Data.Bin.Pos

Methods

eqp :: forall (a :: k) (b :: k). Pos a -> Pos b -> Bool

GShow Pos

Since: 0.1.3

Defined in Data.Bin.Pos

Methods

gshowsPrec :: forall (a :: k). Int -> Pos a -> ShowS

OrdP Pos

>>> let xs = universe @Bin4; ys = universe @Bin6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
[EQ,LT,LT,LT,LT,LT]
[GT,EQ,LT,LT,LT,LT]
[GT,GT,EQ,LT,LT,LT]
[GT,GT,GT,EQ,LT,LT]

Since: 0.1.3

Defined in Data.Bin.Pos

Methods

comparep :: forall (a :: k) (b :: k). Pos a -> Pos b -> Ordering

(SBinPI n, b ~ 'BP n) => Arbitrary (Pos b)

Defined in Data.Bin.Pos

Methods

arbitrary :: Gen (Pos b)

shrink :: Pos b -> [Pos b]

CoArbitrary (Pos b)

Defined in Data.Bin.Pos

Methods

coarbitrary :: Pos b -> Gen b0 -> Gen b0

(SBinPI n, b ~ 'BP n) => Function (Pos b)

Defined in Data.Bin.Pos

Methods

function :: (Pos b -> b0) -> Pos b :-> b0

(SBinPI n, b ~ 'BP n) => Bounded (Pos b)

>>> minBound < (maxBound :: Pos Bin5)
True

Defined in Data.Bin.Pos

Methods

minBound :: Pos b

maxBound :: Pos b

Show (Pos b)

Defined in Data.Bin.Pos

Methods

showsPrec :: Int -> Pos b -> ShowS

show :: Pos b -> String

showList :: [Pos b] -> ShowS

b ~ 'BZ => Absurd (Pos b)

Since: 0.1.2

Defined in Data.Bin.Pos

Methods

absurd :: Pos b -> b0

b ~ 'BP 'BE => Boring (Pos b)

Since: 0.1.2

Defined in Data.Bin.Pos

Methods

boring :: Pos b

NFData (Pos b)

Since: 0.1.2

Defined in Data.Bin.Pos

Methods

rnf :: Pos b -> ()

Eq (Pos b)

Defined in Data.Bin.Pos

Methods

(==) :: Pos b -> Pos b -> Bool

(/=) :: Pos b -> Pos b -> Bool

Ord (Pos b)

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

data PosP (b :: BinP)

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

Instances

EqP PosP

Since: 0.1.3

Defined in Data.BinP.PosP

Methods

eqp :: forall (a :: k) (b :: k). PosP a -> PosP b -> Bool

GShow PosP

Since: 0.1.3

Defined in Data.BinP.PosP

Methods

gshowsPrec :: forall (a :: k). Int -> PosP a -> ShowS

OrdP PosP

Since: 0.1.3

Defined in Data.BinP.PosP

Methods

comparep :: forall (a :: k) (b :: k). PosP a -> PosP b -> Ordering

SBinPI b => Arbitrary (PosP b)

Defined in Data.BinP.PosP

Methods

arbitrary :: Gen (PosP b)

shrink :: PosP b -> [PosP b]

CoArbitrary (PosP b)

Defined in Data.BinP.PosP

Methods

coarbitrary :: PosP b -> Gen b0 -> Gen b0

SBinPI b => Function (PosP b)

Defined in Data.BinP.PosP

Methods

function :: (PosP b -> b0) -> PosP b :-> b0

SBinPI b => Bounded (PosP b)

Defined in Data.BinP.PosP

Methods

minBound :: PosP b

maxBound :: PosP b

Show (PosP b)

Defined in Data.BinP.PosP

Methods

showsPrec :: Int -> PosP b -> ShowS

show :: PosP b -> String

showList :: [PosP b] -> ShowS

b ~ 'BE => Boring (PosP b)

Since: 0.1.2

Defined in Data.BinP.PosP

Methods

boring :: PosP b

NFData (PosP b)

Since: 0.1.2

Defined in Data.BinP.PosP

Methods

rnf :: PosP b -> ()

Eq (PosP b)

Defined in Data.BinP.PosP

Methods

(==) :: PosP b -> PosP b -> Bool

(/=) :: PosP b -> PosP b -> Bool

Ord (PosP b)

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

Top & Pop

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

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)

See top.

Showing

explicitShow :: Pos b -> String

explicitShowsPrec :: Int -> Pos b -> ShowS

Conversions

toNatural :: Pos b -> Natural

Convert Pos to Natural

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

Interesting

absurd :: Pos 'BZ -> b

Pos BZ is not inhabited.

boring :: Pos ('BP 'BE)

Counting to one is boring

>>> boring
0

Weakening (succ)

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

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]

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