Modulebin-0.1.4.1Haskell2010

Data.BinP.PosP

2 types
13 values

Packagebin-0.1.4.1
Exports15
LanguageHaskell2010
LicenceGPL-2.0-or-later
SourcePosP.hs

newtypenewtype PosP (b :: BinP)

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

Constructors

PosP
- unPosP :: PosP' 'Z b

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

datadata PosP' (n :: Nat) (b :: BinP) where

PosP' is a structure inside PosP.

Constructors

AtEnd :: Wrd n -> PosP' n 'BE
Here :: Wrd n -> PosP' n b
There1 :: PosP' ('S n) b -> PosP' n b
There0 :: PosP' ('S n) b -> PosP' n b

Instances9GShow, Bounded, Eq, Ord, Show, NFData, …

SNatI n => GShow (PosP' n)Defined in bin-0.1.4.1 · Data.BinP.PosP
(SNatI n, SBinPI b) => Bounded (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
Eq (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
Ord (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
SNatI n => Show (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
NFData (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
(SNatI n, SBinPI b) => Arbitrary (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
SNatI n => CoArbitrary (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
(SNatI n, SBinPI b) => Function (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP

Top & Pop

2 declarations

valuetop :: SBinPI b => PosP b

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

Example1 expression

>>> top :: PosP BinP40

Example1 expression

>>> pop (pop top) :: PosP BinP42

Example1 expression

>>> pop (pop top) :: PosP BinP92

valuepop :: (SBinPI a, Pred b ~ 'BP a, Succ a ~ b) => PosP a -> PosP b

See top.

Showing

4 declarations

valueexplicitShow :: PosP b -> String

valueexplicitShow' :: PosP' n b -> String

valueexplicitShowsPrec :: Int -> PosP b -> ShowS

valueexplicitShowsPrec' :: Int -> PosP' n b -> ShowS

Conversions

2 declarations

valuetoNatural :: PosP b -> Natural

Convert PosP to Natural.

valuetoNatural' :: SNatI n => PosP' n b -> Natural

Convert PosP' to Natural.

Interesting

1 declaration

valueboring :: PosP 'BE

Counting to one is boring

Example1 expression

>>> boring0

Weakening (succ)

2 declarations

valueweakenRight1 :: SBinPI b => PosP b -> PosP (Succ b)

valueweakenRight1' :: SBinP b -> PosP' n b -> PosP' n (Succ b)

Universe

2 declarations

valueuniverse :: SBinPI b => [PosP b]

Example1 expression

>>> universe :: [PosP BinP9][0,1,2,3,4,5,6,7,8]

valueuniverse' :: (SNatI n, SBinPI b) => [PosP' n b]

This gives a hint, what the n parameter means in PosP'.

Example1 expression

>>> universe' :: [PosP' N.Nat2 BinP2][0,1,2,3,4,5,6,7]