HORIZON HASKELLDocslts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K
Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

Modulebin-0.1.4.1Haskell2010

Data.Bin.Pos

Contents
  1. Top & Pop
  2. Showing
  3. Conversions
  4. Interesting
  5. Weakening (succ)
  6. Universe
Synopsis
  • Packagebin-0.1.4.1
  • Exports11
  • LanguageHaskell2010
  • LicenceGPL-2.0-or-later
  • SourcePos.hs
datadata Pos (b :: Bin) where
Source#

Pos is to Bin is what Fin is to Nat.

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

Constructors

Instances13EqP, GShow, OrdP, Bounded, Eq, Ord, …
  • EqP PosDefined in bin-0.1.4.1 · Data.Bin.Pos
    Example1 expression
    eqp (top :: Pos Bin4) (top :: Pos Bin6)True
    Example1 expression
    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]
  • GShow PosDefined in bin-0.1.4.1 · Data.Bin.Pos
  • OrdP PosDefined in bin-0.1.4.1 · Data.Bin.Pos
    Example1 expression
    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]
  • (SBinPI n, b ~ 'BP n) => Bounded (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
    Example1 expression
    minBound < (maxBound :: Pos Bin5)True
  • Eq (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
  • Ord (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
  • Show (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
  • NFData (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
  • (SBinPI n, b ~ 'BP n) => Arbitrary (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
  • CoArbitrary (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
  • (SBinPI n, b ~ 'BP n) => Function (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
  • b ~ 'BZ => Absurd (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
  • b ~ 'BP 'BE => Boring (Pos b)Defined in bin-0.1.4.1 · Data.Bin.Pos
newtypenewtype PosP (b :: BinP)
Source#

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

Instances12EqP, GShow, OrdP, Bounded, Eq, Ord, …
  • EqP PosPDefined in bin-0.1.4.1 · Data.BinP.PosP
  • GShow PosPDefined in bin-0.1.4.1 · Data.BinP.PosP
  • OrdP PosPDefined in bin-0.1.4.1 · Data.BinP.PosP
  • SBinPI b => Bounded (PosP b)Defined in bin-0.1.4.1 · Data.BinP.PosP
  • Eq (PosP b)Defined in bin-0.1.4.1 · Data.BinP.PosP
  • Ord (PosP b)Defined in bin-0.1.4.1 · Data.BinP.PosP
  • Show (PosP b)Defined in bin-0.1.4.1 · Data.BinP.PosP
  • NFData (PosP b)Defined in bin-0.1.4.1 · Data.BinP.PosP
  • SBinPI b => Arbitrary (PosP b)Defined in bin-0.1.4.1 · Data.BinP.PosP
  • CoArbitrary (PosP b)Defined in bin-0.1.4.1 · Data.BinP.PosP
  • SBinPI b => Function (PosP b)Defined in bin-0.1.4.1 · Data.BinP.PosP
  • b ~ 'BE => Boring (PosP b)Defined in bin-0.1.4.1 · Data.BinP.PosP

Top & Pop

valuetop :: 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.

Example1 expression
top :: Pos Bin40
Example1 expression
pop (pop top) :: Pos Bin42
Example1 expression
pop (pop top) :: Pos Bin92

Showing

Conversions

Interesting

Weakening (succ)

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

Like FS for Fin.

Some tests:

Example1 expression
map weakenRight1 $ (universe :: [Pos Bin2])[1,2]
Example1 expression
map weakenRight1 $ (universe :: [Pos Bin3])[1,2,3]
Example1 expression
map weakenRight1 $ (universe :: [Pos Bin4])[1,2,3,4]
Example1 expression
map weakenRight1 $ (universe :: [Pos Bin5])[1,2,3,4,5]
Example1 expression
map weakenRight1 $ (universe :: [Pos Bin6])[1,2,3,4,5,6]

Universe

valueuniverse :: SBinI b => [Pos b]
Source#

Universe, i.e. all [Pos b]

Example1 expression
universe :: [Pos Bin9][0,1,2,3,4,5,6,7,8]
Example1 expression
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))))