HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

Modulebin-0.1.4Haskell2010

Data.Bin.Pos

  • 2 types
  • 9 values
  • Packagebin-0.1.4
  • Exports11
  • LanguageHaskell2010
  • LicenceGPL-2.0-or-later
  • SourcePos.hs
datadata 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

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

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

Instances12EqP, GShow, OrdP, Bounded, Eq, Ord, …

Top & Pop

2 declarations
valuetop :: SBinPI b => Pos ('BP b)
#

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

2 declarations

Conversions

1 declaration

Interesting

2 declarations
valueboring :: Pos ('BP 'BE)
#

Counting to one is boring

Example1 expression
boring0

Weakening (succ)

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

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

1 declaration
valueuniverse :: SBinI b => [Pos b]
#

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