-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Finite totally ordered sets
--   
--   Finite totally ordered sets
@package data-fin
@version 0.1.0


-- | Type-level decimal natural numbers. This is based on [1], and is
--   intended to work with [2] (though we use the <tt>reflection</tt>
--   package for the actual reification part).
--   
--   Recent versions of GHC have type-level natural number literals.
--   Ideally, this module would be completely obviated by that work.
--   Unfortunately, the type-level literals aren't quite ready for prime
--   time yet, because they do not have a solver. Thus, we're implementing
--   here stuff that should be handled natively by GHC in the future. A lot
--   of this also duplicates the functionality in
--   <tt>HList:Data.HList.FakePrelude</tt>[3], which is (or should be)
--   obviated by the new data kinds extension.
--   
--   <ul>
--   <li><i>1</i> Oleg Kiselyov and Chung-chieh Shan. (2007)
--   <i>Lightweight</i> <i>static resources: Sexy types for embedded and
--   systems</i> <i>programming</i>. Proc. Trends in Functional
--   Programming. New York, 2--4 April 2007.
--   <a>http://okmij.org/ftp/Haskell/types.html#binary-arithm</a></li>
--   <li><i>2</i> Oleg Kiselyov and Chung-chieh Shan. (2004)
--   <i>Implicit</i> <i>configurations: or, type classes reflect the values
--   of</i> <i>types</i>. Proc. ACM SIGPLAN 2004 workshop on Haskell.
--   Snowbird, Utah, USA, 22 September 2004. pp.33--44.
--   <a>http://okmij.org/ftp/Haskell/types.html#Prepose</a></li>
--   <li><i>3</i> <a>http://hackage.haskell.org/package/HList</a></li>
--   </ul>
module Data.Number.Fin.TyDecimal

-- | The digit 0.
data D0

-- | The digit 1.
data D1

-- | The digit 2.
data D2

-- | The digit 3.
data D3

-- | The digit 4.
data D4

-- | The digit 5.
data D5

-- | The digit 6.
data D6

-- | The digit 7.
data D7

-- | The digit 8.
data D8

-- | The digit 9.
data D9

-- | The connective. This should only be used left associatively (it
--   associates to the left naturally). Decimal digits are
--   lexicographically big-endian, so they're written as usual; however,
--   they're structurally little-endian due to the left associativity.
data (:.) x y
data LT_
data EQ_
data GT_

-- | Is <tt>n</tt> a well-formed type of kind <tt>Nat</tt>? The only
--   well-formed types of kind <tt>Nat</tt> are type-level natural numbers
--   in structurally little-endian decimal.
--   
--   The hidden type class <tt>(Nat_ n)</tt> entails <tt>(Reifies n
--   Integer)</tt>.
class Nat_ n => Nat n

-- | Is <tt>n</tt> a well-formed type of kind <tt>NatNE0</tt>? The only
--   well-formed types of kind <tt>NatNE0</tt> are the non-zero well-formed
--   types of kind <tt>Nat</tt>;, i.e., the type-level whole numbers in
--   structurally little-endian decimal.
--   
--   The hidden type class <tt>(NatNE0_ n)</tt> entails <tt>(Nat_ n)</tt>
--   and <tt>(Reifies n Integer)</tt>.
class NatNE0_ n => NatNE0 n
nat0 :: Proxy D0
nat1 :: Proxy D1
nat2 :: Proxy D2
nat3 :: Proxy D3
nat4 :: Proxy D4
nat5 :: Proxy D5
nat6 :: Proxy D6
nat7 :: Proxy D7
nat8 :: Proxy D8
nat9 :: Proxy D9
type MaxBoundInt8 = (D1 :. D2) :. D7
type MaxBoundInt16 = (((D3 :. D2) :. D7) :. D6) :. D7
type MaxBoundInt32 = ((((((((D2 :. D1) :. D4) :. D7) :. D4) :. D8) :. D3) :. D6) :. D4) :. D7
type MaxBoundInt64 = (((((((((((((((((D9 :. D2) :. D2) :. D3) :. D3) :. D7) :. D2) :. D0) :. D3) :. D6) :. D8) :. D5) :. D4) :. D7) :. D7) :. D5) :. D8) :. D0) :. D7
type MaxBoundWord8 = (D2 :. D5) :. D5
type MaxBoundWord16 = (((D6 :. D5) :. D5) :. D3) :. D5
type MaxBoundWord32 = ((((((((D4 :. D2) :. D9) :. D4) :. D9) :. D6) :. D7) :. D2) :. D9) :. D5
type MaxBoundWord64 = ((((((((((((((((((D1 :. D8) :. D4) :. D4) :. D6) :. D7) :. D4) :. D4) :. D0) :. D7) :. D3) :. D7) :. D0) :. D9) :. D5) :. D5) :. D1) :. D6) :. D1) :. D5

-- | The successor/predecessor relation; by structural induction on the
--   first argument. Modes:
--   
--   <pre>
--   Succ x (succ x)  -- i.e., given x, return the successor of x
--   Succ (pred y) y  -- i.e., given y, return the predecessor of y
--   </pre>
class (Nat_ x, NatNE0_ y) => Succ x y | x -> y, y -> x
succ :: Succ x y => Proxy x -> Proxy y
pred :: Succ x y => Proxy y -> Proxy x

-- | The addition relation with full dependencies. Modes:
--   
--   <pre>
--   Add x y (x+y)
--   Add x (z-x) z  -- when it's defined.
--   Add (z-y) y z  -- when it's defined.
--   </pre>
class (Add_ x y z, Add_ y x z) => Add x y z | x y -> z, z x -> y, z y -> x
add :: Add x y z => Proxy x -> Proxy y -> Proxy z

-- | N.B., this will be ill-typed if <tt>x</tt> is greater than <tt>z</tt>.
minus :: Add x y z => Proxy z -> Proxy x -> Proxy y

-- | N.B., this will be ill-typed if <tt>x</tt> is greater than <tt>z</tt>.
subtract :: Add x y z => Proxy x -> Proxy z -> Proxy y

-- | Assert that the comparison relation <tt>r</tt> (<tt>LT_</tt>,
--   <tt>EQ_</tt>, or <tt>GT_</tt>) holds between <tt>x</tt> and
--   <tt>y</tt>; by structural induction on the first, and then the second
--   argument.
class (Nat_ x, Nat_ y) => Compare x y r | x y -> r
compare :: Compare x y r => Proxy x -> Proxy y -> Proxy r

-- | Assert that <tt>x &lt;= y</tt>. This is a popular constraint, so we
--   implement it specially. We could have said that <tt>Add n x y =&gt;
--   NatLE x y</tt>, but the following inductive definition is a bit more
--   optimal.
class (Nat_ x, Nat_ y) => NatLE x y

-- | Assert that <tt>x &lt; y</tt>. This is just a shorthand for <tt>x
--   &lt;= pred y</tt>.
class (Nat_ x, NatNE0_ y) => NatLT x y

-- | N.B., this will be ill-typed if <tt>x</tt> is greater than <tt>y</tt>.
assert_NatLE :: NatLE x y => Proxy x -> Proxy y -> ()

-- | Choose the smaller of <tt>x</tt> and <tt>y</tt>.
min :: (Compare x y r, Min_ x y r z) => Proxy x -> Proxy y -> Proxy z

-- | Choose the larger of <tt>x</tt> and <tt>y</tt>.
max :: (Compare x y r, Max_ x y r z) => Proxy x -> Proxy y -> Proxy z
instance Typeable D0
instance Typeable D1
instance Typeable D2
instance Typeable D3
instance Typeable D4
instance Typeable D5
instance Typeable D6
instance Typeable D7
instance Typeable D8
instance Typeable D9
instance Typeable2 :.
instance Min_ x y GT_ y
instance Min_ x y EQ_ x
instance Min_ x y LT_ x
instance Max_ x y GT_ x
instance Max_ x y EQ_ y
instance Max_ x y LT_ y
instance (Succ y' y, NatLE x y') => NatLT x y
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D9) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D9) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D9) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D9) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D9) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D9) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D9) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D9) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D9) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D9) (y :. D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D8) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D8) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D8) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D8) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D8) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D8) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D8) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D8) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D8) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D8) (y :. D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D7) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D7) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D7) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D7) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D7) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D7) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D7) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D7) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D7) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D7) (y :. D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D6) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D6) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D6) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D6) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D6) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D6) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D6) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D6) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D6) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D6) (y :. D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D5) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D5) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D5) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D5) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D5) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D5) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D5) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D5) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D5) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D5) (y :. D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D4) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D4) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D4) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D4) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D4) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D4) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D4) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D4) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D4) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D4) (y :. D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D3) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D3) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D3) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D3) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D3) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D3) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D3) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D3) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D3) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D3) (y :. D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D2) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D2) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D2) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D2) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D2) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D2) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D2) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D2) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D2) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D2) (y :. D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D1) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D1) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D1) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D1) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D1) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D1) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D1) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D1) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D1) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x :. D1) (y :. D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D9)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D3)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D2)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D1)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x :. D0) (y :. D0)
instance NatNE0_ (y :. dy) => NatLE D9 (y :. dy)
instance NatLE D9 D9
instance NatNE0_ (y :. dy) => NatLE D8 (y :. dy)
instance NatLE D8 D9
instance NatLE D8 D8
instance NatNE0_ (y :. dy) => NatLE D7 (y :. dy)
instance NatLE D7 D9
instance NatLE D7 D8
instance NatLE D7 D7
instance NatNE0_ (y :. dy) => NatLE D6 (y :. dy)
instance NatLE D6 D9
instance NatLE D6 D8
instance NatLE D6 D7
instance NatLE D6 D6
instance NatNE0_ (y :. dy) => NatLE D5 (y :. dy)
instance NatLE D5 D9
instance NatLE D5 D8
instance NatLE D5 D7
instance NatLE D5 D6
instance NatLE D5 D5
instance NatNE0_ (y :. dy) => NatLE D4 (y :. dy)
instance NatLE D4 D9
instance NatLE D4 D8
instance NatLE D4 D7
instance NatLE D4 D6
instance NatLE D4 D5
instance NatLE D4 D4
instance NatNE0_ (y :. dy) => NatLE D3 (y :. dy)
instance NatLE D3 D9
instance NatLE D3 D8
instance NatLE D3 D7
instance NatLE D3 D6
instance NatLE D3 D5
instance NatLE D3 D4
instance NatLE D3 D3
instance NatNE0_ (y :. dy) => NatLE D2 (y :. dy)
instance NatLE D2 D9
instance NatLE D2 D8
instance NatLE D2 D7
instance NatLE D2 D6
instance NatLE D2 D5
instance NatLE D2 D4
instance NatLE D2 D3
instance NatLE D2 D2
instance NatNE0_ (y :. dy) => NatLE D1 (y :. dy)
instance NatLE D1 D9
instance NatLE D1 D8
instance NatLE D1 D7
instance NatLE D1 D6
instance NatLE D1 D5
instance NatLE D1 D4
instance NatLE D1 D3
instance NatLE D1 D2
instance NatLE D1 D1
instance NatNE0_ (y :. dy) => NatLE D0 (y :. dy)
instance NatLE D0 D9
instance NatLE D0 D8
instance NatLE D0 D7
instance NatLE D0 D6
instance NatLE D0 D5
instance NatLE D0 D4
instance NatLE D0 D3
instance NatLE D0 D2
instance NatLE D0 D1
instance NatLE D0 D0
instance (NatNE0_ (x :. dx), NatNE0_ (y :. dy), Compare dx dy dr, Compare x y r', NCS r' dr r) => Compare (x :. dx) (y :. dy) r
instance NatNE0_ (x :. dx) => Compare (x :. dx) D9 GT_
instance NatNE0_ (x :. dx) => Compare (x :. dx) D8 GT_
instance NatNE0_ (x :. dx) => Compare (x :. dx) D7 GT_
instance NatNE0_ (x :. dx) => Compare (x :. dx) D6 GT_
instance NatNE0_ (x :. dx) => Compare (x :. dx) D5 GT_
instance NatNE0_ (x :. dx) => Compare (x :. dx) D4 GT_
instance NatNE0_ (x :. dx) => Compare (x :. dx) D3 GT_
instance NatNE0_ (x :. dx) => Compare (x :. dx) D2 GT_
instance NatNE0_ (x :. dx) => Compare (x :. dx) D1 GT_
instance NatNE0_ (x :. dx) => Compare (x :. dx) D0 GT_
instance NatNE0_ (y :. dy) => Compare D9 (y :. dy) LT_
instance Compare D9 D9 EQ_
instance Compare D9 D8 GT_
instance Compare D9 D7 GT_
instance Compare D9 D6 GT_
instance Compare D9 D5 GT_
instance Compare D9 D4 GT_
instance Compare D9 D3 GT_
instance Compare D9 D2 GT_
instance Compare D9 D1 GT_
instance Compare D9 D0 GT_
instance NatNE0_ (y :. dy) => Compare D8 (y :. dy) LT_
instance Compare D8 D9 LT_
instance Compare D8 D8 EQ_
instance Compare D8 D7 GT_
instance Compare D8 D6 GT_
instance Compare D8 D5 GT_
instance Compare D8 D4 GT_
instance Compare D8 D3 GT_
instance Compare D8 D2 GT_
instance Compare D8 D1 GT_
instance Compare D8 D0 GT_
instance NatNE0_ (y :. dy) => Compare D7 (y :. dy) LT_
instance Compare D7 D9 LT_
instance Compare D7 D8 LT_
instance Compare D7 D7 EQ_
instance Compare D7 D6 GT_
instance Compare D7 D5 GT_
instance Compare D7 D4 GT_
instance Compare D7 D3 GT_
instance Compare D7 D2 GT_
instance Compare D7 D1 GT_
instance Compare D7 D0 GT_
instance NatNE0_ (y :. dy) => Compare D6 (y :. dy) LT_
instance Compare D6 D9 LT_
instance Compare D6 D8 LT_
instance Compare D6 D7 LT_
instance Compare D6 D6 EQ_
instance Compare D6 D5 GT_
instance Compare D6 D4 GT_
instance Compare D6 D3 GT_
instance Compare D6 D2 GT_
instance Compare D6 D1 GT_
instance Compare D6 D0 GT_
instance NatNE0_ (y :. dy) => Compare D5 (y :. dy) LT_
instance Compare D5 D9 LT_
instance Compare D5 D8 LT_
instance Compare D5 D7 LT_
instance Compare D5 D6 LT_
instance Compare D5 D5 EQ_
instance Compare D5 D4 GT_
instance Compare D5 D3 GT_
instance Compare D5 D2 GT_
instance Compare D5 D1 GT_
instance Compare D5 D0 GT_
instance NatNE0_ (y :. dy) => Compare D4 (y :. dy) LT_
instance Compare D4 D9 LT_
instance Compare D4 D8 LT_
instance Compare D4 D7 LT_
instance Compare D4 D6 LT_
instance Compare D4 D5 LT_
instance Compare D4 D4 EQ_
instance Compare D4 D3 GT_
instance Compare D4 D2 GT_
instance Compare D4 D1 GT_
instance Compare D4 D0 GT_
instance NatNE0_ (y :. dy) => Compare D3 (y :. dy) LT_
instance Compare D3 D9 LT_
instance Compare D3 D8 LT_
instance Compare D3 D7 LT_
instance Compare D3 D6 LT_
instance Compare D3 D5 LT_
instance Compare D3 D4 LT_
instance Compare D3 D3 EQ_
instance Compare D3 D2 GT_
instance Compare D3 D1 GT_
instance Compare D3 D0 GT_
instance NatNE0_ (y :. dy) => Compare D2 (y :. dy) LT_
instance Compare D2 D9 LT_
instance Compare D2 D8 LT_
instance Compare D2 D7 LT_
instance Compare D2 D6 LT_
instance Compare D2 D5 LT_
instance Compare D2 D4 LT_
instance Compare D2 D3 LT_
instance Compare D2 D2 EQ_
instance Compare D2 D1 GT_
instance Compare D2 D0 GT_
instance NatNE0_ (y :. dy) => Compare D1 (y :. dy) LT_
instance Compare D1 D9 LT_
instance Compare D1 D8 LT_
instance Compare D1 D7 LT_
instance Compare D1 D6 LT_
instance Compare D1 D5 LT_
instance Compare D1 D4 LT_
instance Compare D1 D3 LT_
instance Compare D1 D2 LT_
instance Compare D1 D1 EQ_
instance Compare D1 D0 GT_
instance NatNE0_ (y :. dy) => Compare D0 (y :. dy) LT_
instance Compare D0 D9 LT_
instance Compare D0 D8 LT_
instance Compare D0 D7 LT_
instance Compare D0 D6 LT_
instance Compare D0 D5 LT_
instance Compare D0 D4 LT_
instance Compare D0 D3 LT_
instance Compare D0 D2 LT_
instance Compare D0 D1 LT_
instance Compare D0 D0 EQ_
instance (Add_ x y z, Add_ y x z) => Add x y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D9 (zh :. dy) z) => Add_ (x :. D9) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D8 (zh :. dy) z) => Add_ (x :. D8) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D7 (zh :. dy) z) => Add_ (x :. D7) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D6 (zh :. dy) z) => Add_ (x :. D6) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D5 (zh :. dy) z) => Add_ (x :. D5) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D4 (zh :. dy) z) => Add_ (x :. D4) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D3 (zh :. dy) z) => Add_ (x :. D3) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D2 (zh :. dy) z) => Add_ (x :. D2) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D1 (zh :. dy) z) => Add_ (x :. D1) y z
instance (NatNE0_ x, NatNE0_ (z :. dz), Add_ x y' z, Snoc y' dz y) => Add_ (x :. D0) y (z :. dz)
instance (Succ y y1, Succ y1 y2, Succ y2 y3, Succ y3 y4, Succ y4 y5, Succ y5 y6, Succ y6 y7, Succ y7 y8, Succ y8 y9) => Add_ D9 y y9
instance (Succ y y1, Succ y1 y2, Succ y2 y3, Succ y3 y4, Succ y4 y5, Succ y5 y6, Succ y6 y7, Succ y7 y8) => Add_ D8 y y8
instance (Succ y y1, Succ y1 y2, Succ y2 y3, Succ y3 y4, Succ y4 y5, Succ y5 y6, Succ y6 y7) => Add_ D7 y y7
instance (Succ y y1, Succ y1 y2, Succ y2 y3, Succ y3 y4, Succ y4 y5, Succ y5 y6) => Add_ D6 y y6
instance (Succ y y1, Succ y1 y2, Succ y2 y3, Succ y3 y4, Succ y4 y5) => Add_ D5 y y5
instance (Succ y y1, Succ y1 y2, Succ y2 y3, Succ y3 y4) => Add_ D4 y y4
instance (Succ y y1, Succ y1 y2, Succ y2 y3) => Add_ D3 y y3
instance (Succ y y1, Succ y1 y2) => Add_ D2 y y2
instance Succ y y1 => Add_ D1 y y1
instance Nat_ y => Add_ D0 y y
instance (Digit_ d', Nat_ (x :. d), Nat_ ((x :. d) :. d')) => Snoc (x :. d) d' ((x :. d) :. d')
instance (Digit_ d, Nat_ (D9 :. d)) => Snoc D9 d (D9 :. d)
instance (Digit_ d, Nat_ (D8 :. d)) => Snoc D8 d (D8 :. d)
instance (Digit_ d, Nat_ (D7 :. d)) => Snoc D7 d (D7 :. d)
instance (Digit_ d, Nat_ (D6 :. d)) => Snoc D6 d (D6 :. d)
instance (Digit_ d, Nat_ (D5 :. d)) => Snoc D5 d (D5 :. d)
instance (Digit_ d, Nat_ (D4 :. d)) => Snoc D4 d (D4 :. d)
instance (Digit_ d, Nat_ (D3 :. d)) => Snoc D3 d (D3 :. d)
instance (Digit_ d, Nat_ (D2 :. d)) => Snoc D2 d (D2 :. d)
instance (Digit_ d, Nat_ (D1 :. d)) => Snoc D1 d (D1 :. d)
instance Snoc D0 D9 D9
instance Snoc D0 D8 D8
instance Snoc D0 D7 D7
instance Snoc D0 D6 D6
instance Snoc D0 D5 D5
instance Snoc D0 D4 D4
instance Snoc D0 D3 D3
instance Snoc D0 D2 D2
instance Snoc D0 D1 D1
instance Snoc D0 D0 D0
instance (NatNE0_ x, Succ x (y :. d)) => Succ (x :. D9) ((y :. d) :. D0)
instance NatNE0_ x => Succ (x :. D8) (x :. D9)
instance NatNE0_ x => Succ (x :. D7) (x :. D8)
instance NatNE0_ x => Succ (x :. D6) (x :. D7)
instance NatNE0_ x => Succ (x :. D5) (x :. D6)
instance NatNE0_ x => Succ (x :. D4) (x :. D5)
instance NatNE0_ x => Succ (x :. D3) (x :. D4)
instance NatNE0_ x => Succ (x :. D2) (x :. D3)
instance NatNE0_ x => Succ (x :. D1) (x :. D2)
instance NatNE0_ x => Succ (x :. D0) (x :. D1)
instance Succ D9 (D1 :. D0)
instance Succ D8 D9
instance Succ D7 D8
instance Succ D6 D7
instance Succ D5 D6
instance Succ D4 D5
instance Succ D3 D4
instance Succ D2 D3
instance Succ D1 D2
instance Succ D0 D1
instance NatNE0_ x => Reifies * (x :. D9) Integer
instance NatNE0_ x => Reifies * (x :. D8) Integer
instance NatNE0_ x => Reifies * (x :. D7) Integer
instance NatNE0_ x => Reifies * (x :. D6) Integer
instance NatNE0_ x => Reifies * (x :. D5) Integer
instance NatNE0_ x => Reifies * (x :. D4) Integer
instance NatNE0_ x => Reifies * (x :. D3) Integer
instance NatNE0_ x => Reifies * (x :. D2) Integer
instance NatNE0_ x => Reifies * (x :. D1) Integer
instance NatNE0_ x => Reifies * (x :. D0) Integer
instance Reifies * D9 Integer
instance Reifies * D8 Integer
instance Reifies * D7 Integer
instance Reifies * D6 Integer
instance Reifies * D5 Integer
instance Reifies * D4 Integer
instance Reifies * D3 Integer
instance Reifies * D2 Integer
instance Reifies * D1 Integer
instance Reifies * D0 Integer
instance NatNE0_ x => Nat_ (x :. D9)
instance NatNE0_ x => Nat_ (x :. D8)
instance NatNE0_ x => Nat_ (x :. D7)
instance NatNE0_ x => Nat_ (x :. D6)
instance NatNE0_ x => Nat_ (x :. D5)
instance NatNE0_ x => Nat_ (x :. D4)
instance NatNE0_ x => Nat_ (x :. D3)
instance NatNE0_ x => Nat_ (x :. D2)
instance NatNE0_ x => Nat_ (x :. D1)
instance NatNE0_ x => Nat_ (x :. D0)
instance Nat_ D9
instance Nat_ D8
instance Nat_ D7
instance Nat_ D6
instance Nat_ D5
instance Nat_ D4
instance Nat_ D3
instance Nat_ D2
instance Nat_ D1
instance Nat_ D0
instance NatNE0_ n => NatNE0_ (n :. D9)
instance NatNE0_ n => NatNE0_ (n :. D8)
instance NatNE0_ n => NatNE0_ (n :. D7)
instance NatNE0_ n => NatNE0_ (n :. D6)
instance NatNE0_ n => NatNE0_ (n :. D5)
instance NatNE0_ n => NatNE0_ (n :. D4)
instance NatNE0_ n => NatNE0_ (n :. D3)
instance NatNE0_ n => NatNE0_ (n :. D2)
instance NatNE0_ n => NatNE0_ (n :. D1)
instance NatNE0_ n => NatNE0_ (n :. D0)
instance NatNE0_ D9
instance NatNE0_ D8
instance NatNE0_ D7
instance NatNE0_ D6
instance NatNE0_ D5
instance NatNE0_ D4
instance NatNE0_ D3
instance NatNE0_ D2
instance NatNE0_ D1
instance Digit_ D9
instance Digit_ D8
instance Digit_ D7
instance Digit_ D6
instance Digit_ D5
instance Digit_ D4
instance Digit_ D3
instance Digit_ D2
instance Digit_ D1
instance Digit_ D0
instance NatNE0_ n => NatNE0 n
instance Nat_ n => Nat n


-- | A newtype of <a>Int8</a> for finite subsets of the natural numbers.
module Data.Number.Fin.Int8

-- | A finite set of integers <tt>Fin n = { i :: Int8 | 0 &lt;= i &lt; n
--   }</tt> with the usual ordering. This is typed as if using the standard
--   GADT presentation of <tt>Fin n</tt>, however it is actually
--   implemented by a plain <a>Int8</a>.
data Fin n

-- | Like <a>show</a>, except it shows the type itself instead of the
--   value.
showFinType :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> String

-- | Like <a>shows</a>, except it shows the type itself instead of the
--   value.
showsFinType :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> ShowS

-- | Return the <a>minBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always zero, but is provided for symmetry with <a>maxBoundOf</a>.
minBoundOf :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> Int8

-- | Return the <a>maxBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always <tt>n-1</tt>, but it's helpful because you may not know what
--   <tt>n</tt> is at the time.
maxBoundOf :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> Int8

-- | Safely embed a number into <tt>Fin n</tt>. Use of this function will
--   generally require an explicit type signature in order to know which
--   <tt>n</tt> to use.
toFin :: (NatLE n MaxBoundInt8, Nat n) => Int8 -> Maybe (Fin n)

-- | Safely embed a number into <tt>Fin n</tt>. This variant of
--   <a>toFin</a> uses a proxy to avoid the need for type signatures.
toFinProxy :: (NatLE n MaxBoundInt8, Nat n) => Proxy n -> Int8 -> Maybe (Fin n)

-- | Safely embed integers into <tt>Fin n</tt>, where <tt>n</tt> is the
--   first argument. We use rank-2 polymorphism to render the type-level
--   <tt>n</tt> existentially quantified, thereby hiding the dependent type
--   from the compiler. However, <tt>n</tt> will in fact be a skolem, so we
--   can't provide the continuation with proof that <tt>Nat n</tt> ---
--   unfortunately, rendering this function of little use.
--   
--   <pre>
--   toFinCPS n k i
--       | 0 &lt;= i &amp;&amp; i &lt; n  = Just (k i)  -- morally speaking...
--       | otherwise        = Nothing
--   </pre>
toFinCPS :: Int8 -> (forall n. Reifies n Integer => Fin n -> r) -> Int8 -> Maybe r

-- | Extract the value of a <tt>Fin n</tt>.
--   
--   <i>N.B.,</i> if somehow the <tt>Fin n</tt> value was constructed
--   invalidly, then this function will throw an exception. However, this
--   should <i>never</i> happen. If it does, contact the maintainer since
--   this indicates a bug/insecurity in this library.
fromFin :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> Int8

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>minBound</a>. That is,
--   
--   <pre>
--   fromFin (weaken x) == fromFin x
--   </pre>
--   
--   The opposite of this function is <a>maxView</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
weaken :: (NatLE n MaxBoundInt8, Succ m n) => Fin m -> Fin n

-- | A variant of <a>weaken</a> which allows weakening the type by multiple
--   steps. Use of this function will generally require an explicit type
--   signature in order to know which <tt>n</tt> to use.
--   
--   The opposite of this function is <a>maxViewLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
weakenLE :: (NatLE n MaxBoundInt8, NatLE m n) => Fin m -> Fin n

-- | A type-signature variant of <a>weakenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE m o</tt>. This is
--   the left half of <a>plus</a>.
weakenPlus :: (NatLE o MaxBoundInt8, Add m n o) => Fin m -> Fin o

-- | The maximum-element view. This strengthens the type by removing the
--   maximum element:
--   
--   <pre>
--   maxView maxBound = Nothing
--   maxView x        = Just x  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>weaken</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
maxView :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, Succ m n) => Fin n -> Maybe (Fin m)

-- | A variant of <a>maxView</a> which allows strengthening the type by
--   multiple steps. Use of this function will generally require an
--   explicit type signature in order to know which <tt>m</tt> to use.
--   
--   The opposite of this function is <a>weakenLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
maxViewLE :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE m n) => Fin n -> Maybe (Fin m)

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>maxBound</a>. That is, we shift everything up
--   by one:
--   
--   <pre>
--   fromFin (widen x) == 1 + fromFin x
--   </pre>
--   
--   The opposite of this function is <a>predView</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
widen :: (NatLE n MaxBoundInt8, Succ m n) => Fin m -> Fin n

-- | Embed a finite domain into any larger one, keeping the same position
--   relative to <a>maxBound</a>. That is,
--   
--   <pre>
--   maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
--       where y = widenLE x
--   </pre>
--   
--   Use of this function will generally require an explicit type signature
--   in order to know which <tt>n</tt> to use.
widenLE :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE m n) => Fin m -> Fin n

-- | A type-signature variant of <a>widenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE n o</tt>. This is
--   the right half of <a>plus</a>.
widenPlus :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8, Add m n o) => Fin n -> Fin o

-- | The predecessor view. This strengthens the type by shifting everything
--   down by one:
--   
--   <pre>
--   predView 0 = Nothing
--   predView x = Just (x-1)  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>widen</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
predView :: (NatLE n MaxBoundInt8, Succ m n) => Fin n -> Maybe (Fin m)

-- | The ordinal-sum functor, on objects. This internalizes the disjoint
--   union, mapping <tt>Fin m + Fin n</tt> into <tt>Fin(m+n)</tt> by
--   placing the image of the summands next to one another in the codomain,
--   thereby preserving the structure of both summands.
plus :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8, Add m n o) => Either (Fin m) (Fin n) -> Fin o

-- | The inverse of <a>plus</a>.
unplus :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8, Add m n o) => Fin o -> Either (Fin m) (Fin n)

-- | The ordinal-sum functor, on morphisms. If we view the maps as
--   bipartite graphs, then the new map is the result of placing the left
--   and right maps next to one another. This is similar to <tt>(+++)</tt>
--   from <a>Control.Arrow</a>.
fplus :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8, NatLE m' MaxBoundInt8, NatLE n' MaxBoundInt8, NatLE o' MaxBoundInt8, Add m n o, Add m' n' o') => (Fin m -> Fin m') -> (Fin n -> Fin n') -> (Fin o -> Fin o')

-- | The "face maps" for <tt>Fin</tt> viewed as the standard simplices
--   (aka: the thinning view). Traditionally spelled with delta or epsilon.
--   For each <tt>i</tt>, it is the unique injective monotonic map that
--   skips <tt>i</tt>. That is,
--   
--   <pre>
--   thin i = (\j -&gt; if j &lt; i then j else succ j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thin i j /= i
--   </pre>
thin :: (NatLE n MaxBoundInt8, Succ m n) => Fin n -> Fin m -> Fin n

-- | The "degeneracy maps" for <tt>Fin</tt> viewed as the standard
--   simplices. Traditionally spelled with sigma or eta. For each
--   <tt>i</tt>, it is the unique surjective monotonic map that covers
--   <tt>i</tt> twice. That is,
--   
--   <pre>
--   thick i = (\j -&gt; if j &lt;= i then j else pred j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thick i (i+1) == i
--   </pre>
thick :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, Succ m n) => Fin m -> Fin n -> Fin m
instance Typeable1 Fin
instance (NatLE n MaxBoundInt8, Nat n) => Serial (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Serial (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => CoArbitrary (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Arbitrary (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Ix (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Enum (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => DownwardEnum (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => UpwardEnum (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Enum (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Bounded (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Ord (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Eq (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Read (Fin n)
instance (NatLE n MaxBoundInt8, Nat n) => Show (Fin n)


-- | A newtype of <a>Int16</a> for finite subsets of the natural numbers.
module Data.Number.Fin.Int16

-- | A finite set of integers <tt>Fin n = { i :: Int16 | 0 &lt;= i &lt; n
--   }</tt> with the usual ordering. This is typed as if using the standard
--   GADT presentation of <tt>Fin n</tt>, however it is actually
--   implemented by a plain <a>Int16</a>.
data Fin n

-- | Like <a>show</a>, except it shows the type itself instead of the
--   value.
showFinType :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> String

-- | Like <a>shows</a>, except it shows the type itself instead of the
--   value.
showsFinType :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> ShowS

-- | Return the <a>minBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always zero, but is provided for symmetry with <a>maxBoundOf</a>.
minBoundOf :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> Int16

-- | Return the <a>maxBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always <tt>n-1</tt>, but it's helpful because you may not know what
--   <tt>n</tt> is at the time.
maxBoundOf :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> Int16

-- | Safely embed a number into <tt>Fin n</tt>. Use of this function will
--   generally require an explicit type signature in order to know which
--   <tt>n</tt> to use.
toFin :: (NatLE n MaxBoundInt16, Nat n) => Int16 -> Maybe (Fin n)

-- | Safely embed a number into <tt>Fin n</tt>. This variant of
--   <a>toFin</a> uses a proxy to avoid the need for type signatures.
toFinProxy :: (NatLE n MaxBoundInt16, Nat n) => Proxy n -> Int16 -> Maybe (Fin n)

-- | Safely embed integers into <tt>Fin n</tt>, where <tt>n</tt> is the
--   first argument. We use rank-2 polymorphism to render the type-level
--   <tt>n</tt> existentially quantified, thereby hiding the dependent type
--   from the compiler. However, <tt>n</tt> will in fact be a skolem, so we
--   can't provide the continuation with proof that <tt>Nat n</tt> ---
--   unfortunately, rendering this function of little use.
--   
--   <pre>
--   toFinCPS n k i
--       | 0 &lt;= i &amp;&amp; i &lt; n  = Just (k i)  -- morally speaking...
--       | otherwise        = Nothing
--   </pre>
toFinCPS :: Int16 -> (forall n. Reifies n Integer => Fin n -> r) -> Int16 -> Maybe r

-- | Extract the value of a <tt>Fin n</tt>.
--   
--   <i>N.B.,</i> if somehow the <tt>Fin n</tt> value was constructed
--   invalidly, then this function will throw an exception. However, this
--   should <i>never</i> happen. If it does, contact the maintainer since
--   this indicates a bug/insecurity in this library.
fromFin :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> Int16

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>minBound</a>. That is,
--   
--   <pre>
--   fromFin (weaken x) == fromFin x
--   </pre>
--   
--   The opposite of this function is <a>maxView</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
weaken :: (NatLE n MaxBoundInt16, Succ m n) => Fin m -> Fin n

-- | A variant of <a>weaken</a> which allows weakening the type by multiple
--   steps. Use of this function will generally require an explicit type
--   signature in order to know which <tt>n</tt> to use.
--   
--   The opposite of this function is <a>maxViewLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
weakenLE :: (NatLE n MaxBoundInt16, NatLE m n) => Fin m -> Fin n

-- | A type-signature variant of <a>weakenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE m o</tt>. This is
--   the left half of <a>plus</a>.
weakenPlus :: (NatLE o MaxBoundInt16, Add m n o) => Fin m -> Fin o

-- | The maximum-element view. This strengthens the type by removing the
--   maximum element:
--   
--   <pre>
--   maxView maxBound = Nothing
--   maxView x        = Just x  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>weaken</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
maxView :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, Succ m n) => Fin n -> Maybe (Fin m)

-- | A variant of <a>maxView</a> which allows strengthening the type by
--   multiple steps. Use of this function will generally require an
--   explicit type signature in order to know which <tt>m</tt> to use.
--   
--   The opposite of this function is <a>weakenLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
maxViewLE :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE m n) => Fin n -> Maybe (Fin m)

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>maxBound</a>. That is, we shift everything up
--   by one:
--   
--   <pre>
--   fromFin (widen x) == 1 + fromFin x
--   </pre>
--   
--   The opposite of this function is <a>predView</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
widen :: (NatLE n MaxBoundInt16, Succ m n) => Fin m -> Fin n

-- | Embed a finite domain into any larger one, keeping the same position
--   relative to <a>maxBound</a>. That is,
--   
--   <pre>
--   maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
--       where y = widenLE x
--   </pre>
--   
--   Use of this function will generally require an explicit type signature
--   in order to know which <tt>n</tt> to use.
widenLE :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE m n) => Fin m -> Fin n

-- | A type-signature variant of <a>widenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE n o</tt>. This is
--   the right half of <a>plus</a>.
widenPlus :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16, Add m n o) => Fin n -> Fin o

-- | The predecessor view. This strengthens the type by shifting everything
--   down by one:
--   
--   <pre>
--   predView 0 = Nothing
--   predView x = Just (x-1)  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>widen</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
predView :: (NatLE n MaxBoundInt16, Succ m n) => Fin n -> Maybe (Fin m)

-- | The ordinal-sum functor, on objects. This internalizes the disjoint
--   union, mapping <tt>Fin m + Fin n</tt> into <tt>Fin(m+n)</tt> by
--   placing the image of the summands next to one another in the codomain,
--   thereby preserving the structure of both summands.
plus :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16, Add m n o) => Either (Fin m) (Fin n) -> Fin o

-- | The inverse of <a>plus</a>.
unplus :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16, Add m n o) => Fin o -> Either (Fin m) (Fin n)

-- | The ordinal-sum functor, on morphisms. If we view the maps as
--   bipartite graphs, then the new map is the result of placing the left
--   and right maps next to one another. This is similar to <tt>(+++)</tt>
--   from <a>Control.Arrow</a>.
fplus :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16, NatLE m' MaxBoundInt16, NatLE n' MaxBoundInt16, NatLE o' MaxBoundInt16, Add m n o, Add m' n' o') => (Fin m -> Fin m') -> (Fin n -> Fin n') -> (Fin o -> Fin o')

-- | The "face maps" for <tt>Fin</tt> viewed as the standard simplices
--   (aka: the thinning view). Traditionally spelled with delta or epsilon.
--   For each <tt>i</tt>, it is the unique injective monotonic map that
--   skips <tt>i</tt>. That is,
--   
--   <pre>
--   thin i = (\j -&gt; if j &lt; i then j else succ j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thin i j /= i
--   </pre>
thin :: (NatLE n MaxBoundInt16, Succ m n) => Fin n -> Fin m -> Fin n

-- | The "degeneracy maps" for <tt>Fin</tt> viewed as the standard
--   simplices. Traditionally spelled with sigma or eta. For each
--   <tt>i</tt>, it is the unique surjective monotonic map that covers
--   <tt>i</tt> twice. That is,
--   
--   <pre>
--   thick i = (\j -&gt; if j &lt;= i then j else pred j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thick i (i+1) == i
--   </pre>
thick :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, Succ m n) => Fin m -> Fin n -> Fin m
instance Typeable1 Fin
instance (NatLE n MaxBoundInt16, Nat n) => Serial (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Serial (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => CoArbitrary (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Arbitrary (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Ix (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Enum (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => DownwardEnum (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => UpwardEnum (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Enum (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Bounded (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Ord (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Eq (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Read (Fin n)
instance (NatLE n MaxBoundInt16, Nat n) => Show (Fin n)


-- | A newtype of <a>Int32</a> for finite subsets of the natural numbers.
module Data.Number.Fin.Int32

-- | A finite set of integers <tt>Fin n = { i :: Int32 | 0 &lt;= i &lt; n
--   }</tt> with the usual ordering. This is typed as if using the standard
--   GADT presentation of <tt>Fin n</tt>, however it is actually
--   implemented by a plain <a>Int32</a>.
data Fin n

-- | Like <a>show</a>, except it shows the type itself instead of the
--   value.
showFinType :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> String

-- | Like <a>shows</a>, except it shows the type itself instead of the
--   value.
showsFinType :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> ShowS

-- | Return the <a>minBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always zero, but is provided for symmetry with <a>maxBoundOf</a>.
minBoundOf :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> Int32

-- | Return the <a>maxBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always <tt>n-1</tt>, but it's helpful because you may not know what
--   <tt>n</tt> is at the time.
maxBoundOf :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> Int32

-- | Safely embed a number into <tt>Fin n</tt>. Use of this function will
--   generally require an explicit type signature in order to know which
--   <tt>n</tt> to use.
toFin :: (NatLE n MaxBoundInt32, Nat n) => Int32 -> Maybe (Fin n)

-- | Safely embed a number into <tt>Fin n</tt>. This variant of
--   <a>toFin</a> uses a proxy to avoid the need for type signatures.
toFinProxy :: (NatLE n MaxBoundInt32, Nat n) => Proxy n -> Int32 -> Maybe (Fin n)

-- | Safely embed integers into <tt>Fin n</tt>, where <tt>n</tt> is the
--   first argument. We use rank-2 polymorphism to render the type-level
--   <tt>n</tt> existentially quantified, thereby hiding the dependent type
--   from the compiler. However, <tt>n</tt> will in fact be a skolem, so we
--   can't provide the continuation with proof that <tt>Nat n</tt> ---
--   unfortunately, rendering this function of little use.
--   
--   <pre>
--   toFinCPS n k i
--       | 0 &lt;= i &amp;&amp; i &lt; n  = Just (k i)  -- morally speaking...
--       | otherwise        = Nothing
--   </pre>
toFinCPS :: Int32 -> (forall n. Reifies n Integer => Fin n -> r) -> Int32 -> Maybe r

-- | Extract the value of a <tt>Fin n</tt>.
--   
--   <i>N.B.,</i> if somehow the <tt>Fin n</tt> value was constructed
--   invalidly, then this function will throw an exception. However, this
--   should <i>never</i> happen. If it does, contact the maintainer since
--   this indicates a bug/insecurity in this library.
fromFin :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> Int32

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>minBound</a>. That is,
--   
--   <pre>
--   fromFin (weaken x) == fromFin x
--   </pre>
--   
--   The opposite of this function is <a>maxView</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
weaken :: (NatLE n MaxBoundInt32, Succ m n) => Fin m -> Fin n

-- | A variant of <a>weaken</a> which allows weakening the type by multiple
--   steps. Use of this function will generally require an explicit type
--   signature in order to know which <tt>n</tt> to use.
--   
--   The opposite of this function is <a>maxViewLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
weakenLE :: (NatLE n MaxBoundInt32, NatLE m n) => Fin m -> Fin n

-- | A type-signature variant of <a>weakenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE m o</tt>. This is
--   the left half of <a>plus</a>.
weakenPlus :: (NatLE o MaxBoundInt32, Add m n o) => Fin m -> Fin o

-- | The maximum-element view. This strengthens the type by removing the
--   maximum element:
--   
--   <pre>
--   maxView maxBound = Nothing
--   maxView x        = Just x  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>weaken</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
maxView :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, Succ m n) => Fin n -> Maybe (Fin m)

-- | A variant of <a>maxView</a> which allows strengthening the type by
--   multiple steps. Use of this function will generally require an
--   explicit type signature in order to know which <tt>m</tt> to use.
--   
--   The opposite of this function is <a>weakenLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
maxViewLE :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE m n) => Fin n -> Maybe (Fin m)

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>maxBound</a>. That is, we shift everything up
--   by one:
--   
--   <pre>
--   fromFin (widen x) == 1 + fromFin x
--   </pre>
--   
--   The opposite of this function is <a>predView</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
widen :: (NatLE n MaxBoundInt32, Succ m n) => Fin m -> Fin n

-- | Embed a finite domain into any larger one, keeping the same position
--   relative to <a>maxBound</a>. That is,
--   
--   <pre>
--   maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
--       where y = widenLE x
--   </pre>
--   
--   Use of this function will generally require an explicit type signature
--   in order to know which <tt>n</tt> to use.
widenLE :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE m n) => Fin m -> Fin n

-- | A type-signature variant of <a>widenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE n o</tt>. This is
--   the right half of <a>plus</a>.
widenPlus :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32, Add m n o) => Fin n -> Fin o

-- | The predecessor view. This strengthens the type by shifting everything
--   down by one:
--   
--   <pre>
--   predView 0 = Nothing
--   predView x = Just (x-1)  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>widen</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
predView :: (NatLE n MaxBoundInt32, Succ m n) => Fin n -> Maybe (Fin m)

-- | The ordinal-sum functor, on objects. This internalizes the disjoint
--   union, mapping <tt>Fin m + Fin n</tt> into <tt>Fin(m+n)</tt> by
--   placing the image of the summands next to one another in the codomain,
--   thereby preserving the structure of both summands.
plus :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32, Add m n o) => Either (Fin m) (Fin n) -> Fin o

-- | The inverse of <a>plus</a>.
unplus :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32, Add m n o) => Fin o -> Either (Fin m) (Fin n)

-- | The ordinal-sum functor, on morphisms. If we view the maps as
--   bipartite graphs, then the new map is the result of placing the left
--   and right maps next to one another. This is similar to <tt>(+++)</tt>
--   from <a>Control.Arrow</a>.
fplus :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32, NatLE m' MaxBoundInt32, NatLE n' MaxBoundInt32, NatLE o' MaxBoundInt32, Add m n o, Add m' n' o') => (Fin m -> Fin m') -> (Fin n -> Fin n') -> (Fin o -> Fin o')

-- | The "face maps" for <tt>Fin</tt> viewed as the standard simplices
--   (aka: the thinning view). Traditionally spelled with delta or epsilon.
--   For each <tt>i</tt>, it is the unique injective monotonic map that
--   skips <tt>i</tt>. That is,
--   
--   <pre>
--   thin i = (\j -&gt; if j &lt; i then j else succ j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thin i j /= i
--   </pre>
thin :: (NatLE n MaxBoundInt32, Succ m n) => Fin n -> Fin m -> Fin n

-- | The "degeneracy maps" for <tt>Fin</tt> viewed as the standard
--   simplices. Traditionally spelled with sigma or eta. For each
--   <tt>i</tt>, it is the unique surjective monotonic map that covers
--   <tt>i</tt> twice. That is,
--   
--   <pre>
--   thick i = (\j -&gt; if j &lt;= i then j else pred j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thick i (i+1) == i
--   </pre>
thick :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, Succ m n) => Fin m -> Fin n -> Fin m
instance Typeable1 Fin
instance (NatLE n MaxBoundInt32, Nat n) => Serial (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Serial (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => CoArbitrary (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Arbitrary (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Ix (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Enum (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => DownwardEnum (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => UpwardEnum (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Enum (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Bounded (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Ord (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Eq (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Read (Fin n)
instance (NatLE n MaxBoundInt32, Nat n) => Show (Fin n)


-- | A newtype of <a>Int64</a> for finite subsets of the natural numbers.
module Data.Number.Fin.Int64

-- | A finite set of integers <tt>Fin n = { i :: Int64 | 0 &lt;= i &lt; n
--   }</tt> with the usual ordering. This is typed as if using the standard
--   GADT presentation of <tt>Fin n</tt>, however it is actually
--   implemented by a plain <a>Int64</a>.
data Fin n

-- | Like <a>show</a>, except it shows the type itself instead of the
--   value.
showFinType :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> String

-- | Like <a>shows</a>, except it shows the type itself instead of the
--   value.
showsFinType :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> ShowS

-- | Return the <a>minBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always zero, but is provided for symmetry with <a>maxBoundOf</a>.
minBoundOf :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> Int64

-- | Return the <a>maxBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always <tt>n-1</tt>, but it's helpful because you may not know what
--   <tt>n</tt> is at the time.
maxBoundOf :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> Int64

-- | Safely embed a number into <tt>Fin n</tt>. Use of this function will
--   generally require an explicit type signature in order to know which
--   <tt>n</tt> to use.
toFin :: (NatLE n MaxBoundInt64, Nat n) => Int64 -> Maybe (Fin n)

-- | Safely embed a number into <tt>Fin n</tt>. This variant of
--   <a>toFin</a> uses a proxy to avoid the need for type signatures.
toFinProxy :: (NatLE n MaxBoundInt64, Nat n) => Proxy n -> Int64 -> Maybe (Fin n)

-- | Safely embed integers into <tt>Fin n</tt>, where <tt>n</tt> is the
--   first argument. We use rank-2 polymorphism to render the type-level
--   <tt>n</tt> existentially quantified, thereby hiding the dependent type
--   from the compiler. However, <tt>n</tt> will in fact be a skolem, so we
--   can't provide the continuation with proof that <tt>Nat n</tt> ---
--   unfortunately, rendering this function of little use.
--   
--   <pre>
--   toFinCPS n k i
--       | 0 &lt;= i &amp;&amp; i &lt; n  = Just (k i)  -- morally speaking...
--       | otherwise        = Nothing
--   </pre>
toFinCPS :: Int64 -> (forall n. Reifies n Integer => Fin n -> r) -> Int64 -> Maybe r

-- | Extract the value of a <tt>Fin n</tt>.
--   
--   <i>N.B.,</i> if somehow the <tt>Fin n</tt> value was constructed
--   invalidly, then this function will throw an exception. However, this
--   should <i>never</i> happen. If it does, contact the maintainer since
--   this indicates a bug/insecurity in this library.
fromFin :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> Int64

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>minBound</a>. That is,
--   
--   <pre>
--   fromFin (weaken x) == fromFin x
--   </pre>
--   
--   The opposite of this function is <a>maxView</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
weaken :: (NatLE n MaxBoundInt64, Succ m n) => Fin m -> Fin n

-- | A variant of <a>weaken</a> which allows weakening the type by multiple
--   steps. Use of this function will generally require an explicit type
--   signature in order to know which <tt>n</tt> to use.
--   
--   The opposite of this function is <a>maxViewLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
weakenLE :: (NatLE n MaxBoundInt64, NatLE m n) => Fin m -> Fin n

-- | A type-signature variant of <a>weakenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE m o</tt>. This is
--   the left half of <a>plus</a>.
weakenPlus :: (NatLE o MaxBoundInt64, Add m n o) => Fin m -> Fin o

-- | The maximum-element view. This strengthens the type by removing the
--   maximum element:
--   
--   <pre>
--   maxView maxBound = Nothing
--   maxView x        = Just x  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>weaken</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
maxView :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, Succ m n) => Fin n -> Maybe (Fin m)

-- | A variant of <a>maxView</a> which allows strengthening the type by
--   multiple steps. Use of this function will generally require an
--   explicit type signature in order to know which <tt>m</tt> to use.
--   
--   The opposite of this function is <a>weakenLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
maxViewLE :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE m n) => Fin n -> Maybe (Fin m)

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>maxBound</a>. That is, we shift everything up
--   by one:
--   
--   <pre>
--   fromFin (widen x) == 1 + fromFin x
--   </pre>
--   
--   The opposite of this function is <a>predView</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
widen :: (NatLE n MaxBoundInt64, Succ m n) => Fin m -> Fin n

-- | Embed a finite domain into any larger one, keeping the same position
--   relative to <a>maxBound</a>. That is,
--   
--   <pre>
--   maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
--       where y = widenLE x
--   </pre>
--   
--   Use of this function will generally require an explicit type signature
--   in order to know which <tt>n</tt> to use.
widenLE :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE m n) => Fin m -> Fin n

-- | A type-signature variant of <a>widenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE n o</tt>. This is
--   the right half of <a>plus</a>.
widenPlus :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64, Add m n o) => Fin n -> Fin o

-- | The predecessor view. This strengthens the type by shifting everything
--   down by one:
--   
--   <pre>
--   predView 0 = Nothing
--   predView x = Just (x-1)  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>widen</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
predView :: (NatLE n MaxBoundInt64, Succ m n) => Fin n -> Maybe (Fin m)

-- | The ordinal-sum functor, on objects. This internalizes the disjoint
--   union, mapping <tt>Fin m + Fin n</tt> into <tt>Fin(m+n)</tt> by
--   placing the image of the summands next to one another in the codomain,
--   thereby preserving the structure of both summands.
plus :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64, Add m n o) => Either (Fin m) (Fin n) -> Fin o

-- | The inverse of <a>plus</a>.
unplus :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64, Add m n o) => Fin o -> Either (Fin m) (Fin n)

-- | The ordinal-sum functor, on morphisms. If we view the maps as
--   bipartite graphs, then the new map is the result of placing the left
--   and right maps next to one another. This is similar to <tt>(+++)</tt>
--   from <a>Control.Arrow</a>.
fplus :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64, NatLE m' MaxBoundInt64, NatLE n' MaxBoundInt64, NatLE o' MaxBoundInt64, Add m n o, Add m' n' o') => (Fin m -> Fin m') -> (Fin n -> Fin n') -> (Fin o -> Fin o')

-- | The "face maps" for <tt>Fin</tt> viewed as the standard simplices
--   (aka: the thinning view). Traditionally spelled with delta or epsilon.
--   For each <tt>i</tt>, it is the unique injective monotonic map that
--   skips <tt>i</tt>. That is,
--   
--   <pre>
--   thin i = (\j -&gt; if j &lt; i then j else succ j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thin i j /= i
--   </pre>
thin :: (NatLE n MaxBoundInt64, Succ m n) => Fin n -> Fin m -> Fin n

-- | The "degeneracy maps" for <tt>Fin</tt> viewed as the standard
--   simplices. Traditionally spelled with sigma or eta. For each
--   <tt>i</tt>, it is the unique surjective monotonic map that covers
--   <tt>i</tt> twice. That is,
--   
--   <pre>
--   thick i = (\j -&gt; if j &lt;= i then j else pred j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thick i (i+1) == i
--   </pre>
thick :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, Succ m n) => Fin m -> Fin n -> Fin m
instance Typeable1 Fin
instance (NatLE n MaxBoundInt64, Nat n) => Serial (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Serial (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => CoArbitrary (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Arbitrary (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Ix (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Enum (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => DownwardEnum (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => UpwardEnum (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Enum (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Bounded (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Ord (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Eq (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Read (Fin n)
instance (NatLE n MaxBoundInt64, Nat n) => Show (Fin n)


-- | A newtype of <a>Integer</a> for finite subsets of the natural numbers.
module Data.Number.Fin.Integer

-- | A finite set of integers <tt>Fin n = { i :: Integer | 0 &lt;= i &lt; n
--   }</tt> with the usual ordering. This is typed as if using the standard
--   GADT presentation of <tt>Fin n</tt>, however it is actually
--   implemented by a plain <a>Integer</a>.
--   
--   If you care more about performance than mathematical accuracy, see
--   <a>Data.Number.Fin.Int32</a> for an alternative implementation as a
--   newtype of <tt>Int32</tt>. Note, however, that doing so makes it
--   harder to reason about code since it introduces many corner cases.
data Fin n

-- | Like <a>show</a>, except it shows the type itself instead of the
--   value.
showFinType :: Nat n => Fin n -> String

-- | Like <a>shows</a>, except it shows the type itself instead of the
--   value.
showsFinType :: Nat n => Fin n -> ShowS

-- | Return the <a>minBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always zero, but is provided for symmetry with <a>maxBoundOf</a>.
minBoundOf :: Nat n => Fin n -> Integer

-- | Return the <a>maxBound</a> of <tt>Fin n</tt> as a plain integer. This
--   is always <tt>n-1</tt>, but it's helpful because you may not know what
--   <tt>n</tt> is at the time.
maxBoundOf :: Nat n => Fin n -> Integer

-- | Safely embed a number into <tt>Fin n</tt>. Use of this function will
--   generally require an explicit type signature in order to know which
--   <tt>n</tt> to use.
toFin :: Nat n => Integer -> Maybe (Fin n)

-- | Safely embed a number into <tt>Fin n</tt>. This variant of
--   <a>toFin</a> uses a proxy to avoid the need for type signatures.
toFinProxy :: Nat n => proxy n -> Integer -> Maybe (Fin n)

-- | Safely embed integers into <tt>Fin n</tt>, where <tt>n</tt> is the
--   first argument. We use rank-2 polymorphism to render the type-level
--   <tt>n</tt> existentially quantified, thereby hiding the dependent type
--   from the compiler. However, <tt>n</tt> will in fact be a skolem, so we
--   can't provide the continuation with proof that <tt>Nat n</tt> ---
--   unfortunately, rendering this function of little use.
--   
--   <pre>
--   toFinCPS n k i
--       | 0 &lt;= i &amp;&amp; i &lt; n  = Just (k i)  -- morally speaking...
--       | otherwise        = Nothing
--   </pre>
toFinCPS :: Integer -> (forall n. Reifies n Integer => Fin n -> r) -> Integer -> Maybe r

-- | Extract the value of a <tt>Fin n</tt>.
--   
--   <i>N.B.,</i> if somehow the <tt>Fin n</tt> value was constructed
--   invalidly, then this function will throw an exception. However, this
--   should <i>never</i> happen. If it does, contact the maintainer since
--   this indicates a bug/insecurity in this library.
fromFin :: Nat n => Fin n -> Integer

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>minBound</a>. That is,
--   
--   <pre>
--   fromFin (weaken x) == fromFin x
--   </pre>
--   
--   The opposite of this function is <a>maxView</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
weaken :: Succ m n => Fin m -> Fin n

-- | A variant of <a>weaken</a> which allows weakening the type by multiple
--   steps. Use of this function will generally require an explicit type
--   signature in order to know which <tt>n</tt> to use.
--   
--   The opposite of this function is <a>maxViewLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
weakenLE :: NatLE m n => Fin m -> Fin n

-- | A type-signature variant of <a>weakenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE m o</tt>. This is
--   the left half of <a>plus</a>.
weakenPlus :: Add m n o => Fin m -> Fin o

-- | The maximum-element view. This strengthens the type by removing the
--   maximum element:
--   
--   <pre>
--   maxView maxBound = Nothing
--   maxView x        = Just x  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>weaken</a>.
--   
--   <pre>
--   maxView . weaken                == Just
--   maybe maxBound weaken . maxView == id
--   </pre>
maxView :: Succ m n => Fin n -> Maybe (Fin m)

-- | A variant of <a>maxView</a> which allows strengthening the type by
--   multiple steps. Use of this function will generally require an
--   explicit type signature in order to know which <tt>m</tt> to use.
--   
--   The opposite of this function is <a>weakenLE</a>. When the choice of
--   <tt>m</tt> and <tt>n</tt> is held constant, we have that:
--   
--   <pre>
--   maxViewLE . weakenLE      == Just
--   fmap weakenLE . maxViewLE == (\i -&gt; if i &lt; m then Just i else Nothing)
--   </pre>
maxViewLE :: NatLE m n => Fin n -> Maybe (Fin m)

-- | Embed a finite domain into the next larger one, keeping the same
--   position relative to <a>maxBound</a>. That is, we shift everything up
--   by one:
--   
--   <pre>
--   fromFin (widen x) == 1 + fromFin x
--   </pre>
--   
--   The opposite of this function is <a>predView</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
widen :: Succ m n => Fin m -> Fin n

-- | Embed a finite domain into any larger one, keeping the same position
--   relative to <a>maxBound</a>. That is,
--   
--   <pre>
--   maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
--       where y = widenLE x
--   </pre>
--   
--   Use of this function will generally require an explicit type signature
--   in order to know which <tt>n</tt> to use.
widenLE :: NatLE m n => Fin m -> Fin n

-- | A type-signature variant of <a>widenLE</a> because we cannot
--   automatically deduce that <tt>Add m n o ==&gt; NatLE n o</tt>. This is
--   the right half of <a>plus</a>.
widenPlus :: Add m n o => Fin n -> Fin o

-- | The predecessor view. This strengthens the type by shifting everything
--   down by one:
--   
--   <pre>
--   predView 0 = Nothing
--   predView x = Just (x-1)  -- morally speaking...
--   </pre>
--   
--   The opposite of this function is <a>widen</a>.
--   
--   <pre>
--   predView . widen         == Just
--   maybe 0 widen . predView == id
--   </pre>
predView :: Succ m n => Fin n -> Maybe (Fin m)

-- | The ordinal-sum functor, on objects. This internalizes the disjoint
--   union, mapping <tt>Fin m + Fin n</tt> into <tt>Fin(m+n)</tt> by
--   placing the image of the summands next to one another in the codomain,
--   thereby preserving the structure of both summands.
plus :: Add m n o => Either (Fin m) (Fin n) -> Fin o

-- | The inverse of <a>plus</a>.
unplus :: Add m n o => Fin o -> Either (Fin m) (Fin n)

-- | The ordinal-sum functor, on morphisms. If we view the maps as
--   bipartite graphs, then the new map is the result of placing the left
--   and right maps next to one another. This is similar to <tt>(+++)</tt>
--   from <a>Control.Arrow</a>.
fplus :: (Add m n o, Add m' n' o') => (Fin m -> Fin m') -> (Fin n -> Fin n') -> (Fin o -> Fin o')

-- | The "face maps" for <tt>Fin</tt> viewed as the standard simplices
--   (aka: the thinning view). Traditionally spelled with delta or epsilon.
--   For each <tt>i</tt>, it is the unique injective monotonic map that
--   skips <tt>i</tt>. That is,
--   
--   <pre>
--   thin i = (\j -&gt; if j &lt; i then j else succ j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thin i j /= i
--   </pre>
thin :: Succ m n => Fin n -> Fin m -> Fin n

-- | The "degeneracy maps" for <tt>Fin</tt> viewed as the standard
--   simplices. Traditionally spelled with sigma or eta. For each
--   <tt>i</tt>, it is the unique surjective monotonic map that covers
--   <tt>i</tt> twice. That is,
--   
--   <pre>
--   thick i = (\j -&gt; if j &lt;= i then j else pred j)  -- morally speaking...
--   </pre>
--   
--   Which has the important universal property that:
--   
--   <pre>
--   thick i (i+1) == i
--   </pre>
thick :: Succ m n => Fin m -> Fin n -> Fin m
instance Typeable1 Fin
instance Nat n => Serial (Fin n)
instance Nat n => Serial (Fin n)
instance Nat n => CoArbitrary (Fin n)
instance Nat n => Arbitrary (Fin n)
instance Nat n => Ix (Fin n)
instance Nat n => Enum (Fin n)
instance Nat n => DownwardEnum (Fin n)
instance Nat n => UpwardEnum (Fin n)
instance Nat n => Enum (Fin n)
instance Nat n => Bounded (Fin n)
instance Nat n => Ord (Fin n)
instance Nat n => Eq (Fin n)
instance Nat n => Read (Fin n)
instance Nat n => Show (Fin n)


-- | Newtypes of built-in numeric types for finite subsets of the natural
--   numbers. The default implementation is the newtype of <a>Integer</a>,
--   since the type-level numbers are unbounded so this is the most
--   natural. Alternative implementations are available as nearly drop-in
--   replacements. The reason for using modules that provide the same API,
--   rather than using type classes or type families, is that those latter
--   approaches introduce a lot of additional complexity for very little
--   benefit. Using multiple different representations of finite sets in
--   the same module seems like an uncommon use case. Albeit, this impedes
--   writing representation-agnostic functions...
--   
--   When the underlying type can only represent finitely many values, this
--   introduces many corner cases which makes reasoning about programs more
--   difficult. However, the main use case for these finite representations
--   is because we know we'll only be dealing with "small" sets, so we'll
--   never actually encounter the corner cases. Thus, this library does not
--   try to handle the corner cases, but rather rules them out with the
--   type system.
--   
--   Many of the operations on finite sets arise from the (skeleton of the)
--   augmented simplex category. For example, the ordinal-sum functor
--   provides the monoidal structure of that category. For more details on
--   the mathematics, see
--   <a>http://ncatlab.org/nlab/show/simplex+category</a>.
module Data.Number.Fin