summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorWrenThornton <>2013-07-21 02:09:26 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2013-07-21 02:09:26 (GMT)
commit52d05e68b283724887d7f05fb4e3c453680254db (patch)
tree20c123c6ae3b2eebc7bfe06d2d6678218785d16c
version 0.1.00.1.0
-rw-r--r--AUTHORS4
-rw-r--r--LICENSE33
-rw-r--r--README49
-rw-r--r--Setup.hs7
-rw-r--r--VERSION2
-rw-r--r--data-fin.cabal81
-rw-r--r--src/Data/Number/Fin.hs53
-rw-r--r--src/Data/Number/Fin/Int16.hs865
-rw-r--r--src/Data/Number/Fin/Int32.hs865
-rw-r--r--src/Data/Number/Fin/Int64.hs865
-rw-r--r--src/Data/Number/Fin/Int8.hs865
-rw-r--r--src/Data/Number/Fin/Integer.hs828
-rw-r--r--src/Data/Number/Fin/TyDecimal.hs941
-rw-r--r--src/Data/Number/Fin/TyOrdering.hs79
14 files changed, 5537 insertions, 0 deletions
diff --git a/AUTHORS b/AUTHORS
new file mode 100644
index 0000000..1b5db46
--- /dev/null
+++ b/AUTHORS
@@ -0,0 +1,4 @@
+=== Haskell data-fin package AUTHORS/THANKS file ===
+
+The data-fin package was written by wren ng thornton and is released
+under the terms in the LICENSE file.
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..f9b11f9
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,33 @@
+Copyright (c) 2012, 2013 wren ng thornton.
+ALL RIGHTS RESERVED.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ * Redistributions in binary form must reproduce the above
+ copyright notice, this list of conditions and the following
+ disclaimer in the documentation and/or other materials provided
+ with the distribution.
+
+ * Neither the name of the copyright holders nor the names of
+ other contributors may be used to endorse or promote products
+ derived from this software without specific prior written
+ permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
+
diff --git a/README b/README
new file mode 100644
index 0000000..6684eb7
--- /dev/null
+++ b/README
@@ -0,0 +1,49 @@
+data-fin
+========
+
+While this package uses complex type machinery, it should be easy
+to install. You should be able to use one of the following standard
+methods to install it.
+
+ -- With cabal-install and without the source:
+ $> cabal install data-fin
+
+ -- With cabal-install and with the source already:
+ $> cd data-fin
+ $> cabal install
+
+ -- Without cabal-install, but with the source already:
+ $> cd data-fin
+ $> runhaskell Setup.hs configure --user
+ $> runhaskell Setup.hs build
+ $> runhaskell Setup.hs test
+ $> runhaskell Setup.hs haddock --hyperlink-source
+ $> runhaskell Setup.hs copy
+ $> runhaskell Setup.hs register
+
+The test step is optional and currently does nothing. The Haddock
+step is also optional.
+
+
+Portability
+===========
+
+While I usually try to keep things as portable as possible, this
+package relies on many GHC language extensions. Thus, no claim of
+portability ot non-GHC copilers is made. All the required language
+extensions are:
+
+CPP
+DeriveDataTypeable
+EmptyDataDecls
+FlexibleContexts
+FlexibleInstances
+FunctionalDependencies
+MultiParamTypeClasses
+Rank2Types
+ScopedTypeVariables
+TypeOperators
+Trustworthy -- GHC >= 7.1 only
+UndecidableInstances
+
+----------------------------------------------------------- fin.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..975c03a
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,7 @@
+#!/usr/bin/env runhaskell
+
+module Main (main) where
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
diff --git a/VERSION b/VERSION
new file mode 100644
index 0000000..08f5388
--- /dev/null
+++ b/VERSION
@@ -0,0 +1,2 @@
+0.1.0 (2013.07.20):
+ - Initial release \ No newline at end of file
diff --git a/data-fin.cabal b/data-fin.cabal
new file mode 100644
index 0000000..6a265f9
--- /dev/null
+++ b/data-fin.cabal
@@ -0,0 +1,81 @@
+----------------------------------------------------------------
+-- wren ng thornton <wren@community.haskell.org> ~ 2013.07.20
+----------------------------------------------------------------
+
+-- By and large Cabal >=1.2 is fine; but >= 1.6 gives tested-with:
+-- and source-repository:.
+Cabal-Version: >= 1.6
+Build-Type: Simple
+
+Name: data-fin
+Version: 0.1.0
+Stability: experimental
+Homepage: http://code.haskell.org/~wren/
+Author: wren ng thornton
+Maintainer: wren@community.haskell.org
+Copyright: Copyright (c) 2012--2013 wren ng thornton
+License: BSD3
+License-File: LICENSE
+
+Category: Data
+Synopsis:
+ Finite totally ordered sets
+Description:
+ Finite totally ordered sets
+
+
+Tested-With:
+ GHC ==6.12.1
+Extra-source-files:
+ AUTHORS, README, VERSION
+Source-Repository head
+ Type: darcs
+ Location: http://community.haskell.org/~wren/data-fin
+
+----------------------------------------------------------------
+Flag base4
+ Default: True
+ Description: base-4.0 emits "Prelude deprecated" messages in
+ order to get people to be explicit about which
+ version of base they use.
+Flag splitBase
+ Default: True
+ Description: base-3.0 (GHC 6.8) broke out the packages: array,
+ bytestring, containers, directory, old-locale,
+ old-time, packedstring, pretty, process, random.
+----------------------------------------------------------------
+Library
+ Hs-Source-Dirs: src
+ Exposed-Modules: Data.Number.Fin
+ , Data.Number.Fin.Integer
+ , Data.Number.Fin.Int8
+ , Data.Number.Fin.Int16
+ , Data.Number.Fin.Int32
+ , Data.Number.Fin.Int64
+ -- Data.Number.Fin.Word8
+ -- Data.Number.Fin.Word16
+ -- Data.Number.Fin.Word32
+ -- Data.Number.Fin.Word64
+ -- Data.Number.Fin.TyInteger
+ -- Data.Number.Fin.TyBinary
+ , Data.Number.Fin.TyDecimal
+ -- TODO: OfType should be moved elsewhere if we don't use it...
+ -- Data.Reflection.OfType
+ Other-Modules: Data.Number.Fin.TyOrdering
+
+ Build-Depends: tagged >= 0.2.3 && < 0.7
+ , reflection >= 1.1.6 && < 1.4
+ , prelude-safeenum < 0.2
+ -- N.B., major smallcheck API break between 0.5 and 0.6
+ , smallcheck >= 0.4 && < 0.7
+ , lazysmallcheck >= 0.5 && < 0.7
+ , QuickCheck >= 2.4.1.1 && < 2.7
+
+ -- I think this is all that needs doing to get rid of the warnings?
+ if flag(base4)
+ Build-Depends: base >= 4 && < 5
+ else
+ Build-Depends: base < 4
+
+----------------------------------------------------------------
+----------------------------------------------------------- fin.
diff --git a/src/Data/Number/Fin.hs b/src/Data/Number/Fin.hs
new file mode 100644
index 0000000..0c34874
--- /dev/null
+++ b/src/Data/Number/Fin.hs
@@ -0,0 +1,53 @@
+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+----------------------------------------------------------------
+-- 2013.07.20
+-- |
+-- Module : Data.Number.Fin
+-- Copyright : 2012--2013 wren ng thornton
+-- License : BSD3
+-- Maintainer : wren@community.haskell.org
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- Newtypes of built-in numeric types for finite subsets of the
+-- natural numbers. The default implementation is the newtype of
+-- 'Integer', 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
+-- <http://ncatlab.org/nlab/show/simplex+category>.
+----------------------------------------------------------------
+module Data.Number.Fin (module Data.Number.Fin.Integer) where
+import Data.Number.Fin.Integer
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+
+-- TODO: offer a newtype of 'Fin' (e.g., @IntMod@) which offers a 'Num' instance for modular arithmetic.
+
+{-
+-- TODO: make Fin a newtype family indexed by the representation type it's a newtype of (e.g., "Data.Number.Fin.Integer" would be @Fin Integer n@)? That would allow people to be polymorphic over the different representations. This would also work great with @Int `Mod` n@ for the modular arithmetic!
+
+However, note that this means we can't use the @reflection@ package because the 'Reifies' class has a fundep. Unless we always want to reflect as 'Integer' and then do 'fromInteger' everywhere... surely the fundep is there for a reason, but why? We could get around this with the 'OfType' branch of reflection we've been working on...
+-}
+
+----------------------------------------------------------------
+----------------------------------------------------------- fin.
diff --git a/src/Data/Number/Fin/Int16.hs b/src/Data/Number/Fin/Int16.hs
new file mode 100644
index 0000000..fe2e710
--- /dev/null
+++ b/src/Data/Number/Fin/Int16.hs
@@ -0,0 +1,865 @@
+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+{-# LANGUAGE ScopedTypeVariables
+ , DeriveDataTypeable
+ , MultiParamTypeClasses
+ , FlexibleContexts
+ , CPP
+ , Rank2Types
+ , UndecidableInstances
+ #-}
+
+#if __GLASGOW_HASKELL__ >= 701
+-- N.B., Data.Proxy and Test.QuickCheck aren't "safe".
+{-# LANGUAGE Trustworthy #-}
+#endif
+----------------------------------------------------------------
+-- 2013.05.29
+-- |
+-- Module : Data.Number.Fin.Int16
+-- Copyright : 2012--2013 wren ng thornton
+-- License : BSD3
+-- Maintainer : wren@community.haskell.org
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- A newtype of 'Int16' for finite subsets of the natural numbers.
+----------------------------------------------------------------
+module Data.Number.Fin.Int16
+ (
+ -- * @Fin@, finite sets of natural numbers
+ Fin()
+
+ -- ** Showing types
+ , showFinType
+ , showsFinType
+
+ -- ** Convenience functions
+ , minBoundOf
+ , maxBoundOf
+
+ -- ** Introduction and elimination
+ , toFin
+ , toFinProxy
+ , toFinCPS
+ , fromFin
+
+ -- ** Views and coersions
+ -- *** Weakening and maximum views
+ , weaken
+ , weakenLE
+ , weakenPlus
+ , maxView
+ , maxViewLE
+
+ -- *** Widening and the predecessor view
+ , widen
+ , widenLE
+ , widenPlus
+ , predView
+
+ -- *** The ordinal-sum functor
+ , plus
+ , unplus
+ , fplus
+
+ -- *** Face- and degeneracy-maps
+ , thin
+ , thick
+ -- TODO: is there any way to get equality to work right?
+ ) where
+
+import qualified Prelude.SafeEnum as SE
+import Data.Int (Int16)
+import Data.Ix
+import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE, MaxBoundInt16)
+import Data.Typeable (Typeable)
+import Data.Proxy (Proxy(Proxy))
+import Data.Reflection (Reifies(reflect), reify)
+import Control.Monad (liftM)
+
+import qualified Test.QuickCheck as QC
+#if (MIN_VERSION_smallcheck(0,6,0))
+import qualified Test.SmallCheck.Series as SC
+#else
+import qualified Test.SmallCheck as SC
+#endif
+import qualified Test.LazySmallCheck as LSC
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- | A finite set of integers @Fin n = { i :: Int16 | 0 <= i < n }@
+-- with the usual ordering. This is typed as if using the standard
+-- GADT presentation of @Fin n@, however it is actually implemented
+-- by a plain 'Int16'.
+newtype Fin n = Fin Int16
+ deriving Typeable
+ -- WART: to give additional constraints (e.g., Nat n) on derived
+ -- instances (e.g., Show, Eq, Ord), we need to specify the
+ -- constraints on the data type declaration; however, giving of
+ -- data-type constraints is deprecated and will be removed from
+ -- the language...
+
+{-
+-- Some fusion rules for treating newtypes like 'id', or as close
+-- as we can. We only have these fire in the last stage so that
+-- they don't inhibit the usual list-fusion rules. Hopefully there's
+-- nothing important which is defined to not fire at [0].
+--
+-- TODO: add other laws regarding 'id'
+{-# RULES
+"map Fin" [0] map Fin = unsafeCoerce
+"fmap Fin" [0] fmap Fin = unsafeCoerce
+"liftM Fin" [0] liftM Fin = unsafeCoerce
+"liftA Fin" [0] liftA Fin = unsafeCoerce
+ #-}
+-}
+
+{- TODO:
+-- also: <http://paczesiowa.blogspot.com/2010/01/pure-extensible-exceptions-and-self.html>
+
+-- | An error for attempts to evaluate an undefined value which is
+-- passed around as a type token. The string should give the source
+-- where the token was generated, or some other helpful information
+-- for tracking the problem down.
+data EvaluatedTypeTokenException = EvaluatedTypeTokenException String
+ deriving (Typeable, Show)
+
+instance Exception EvaluatedTypeTokenException
+
+-- | Construct a type token with the given message.
+__ :: String -> a
+__ here = throw (EvaluatedTypeTokenException here)
+
+
+-- TODO: use Control.Exception.assert instead?
+data FinException = FinOOB (Fin n)
+ deriving (Typeable)
+
+instance Show FinException where
+ show (FinOOB x) =
+ "Value "++show x++" out of bounds for "++showFinType x
+
+instance Exception FinException
+-}
+
+
+-- | Often, we don't want to use the @Fin n@ as a proxy, since that
+-- would introduce spurious data dependencies. This function ignores
+-- its argument (other than for type propagation) so, hopefully,
+-- via massive inlining this function will avoid that spurious
+-- dependency. Hopefully...
+--
+-- Also, this lets us minimize the use of @-XScopedTypeVariables@
+-- which makes the Haddocks ugly. And so it lets us avoid the hacks
+-- to hide our use of @-XScopedTypeVariables@.
+--
+-- TODO: is this enough to ensure reflection is/can-be done at compile-time?
+-- TODO: is there any way to tell GHC that this function should /never/ appear in the output of compilation?
+fin2proxy :: (NatLE n MaxBoundInt16, Nat n) => fin n -> Proxy n
+fin2proxy _ = Proxy
+{-# INLINE fin2proxy #-}
+
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt16, Nat n) => Show (Fin n) where
+ showsPrec d (Fin i) =
+ showParen (d > 10) $ ("Fin "++) . shows i
+
+
+-- | Like 'show', except it shows the type itself instead of the
+-- value.
+showFinType :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> String
+showFinType x = showsFinType x []
+{-# INLINE showFinType #-}
+-- Should never fire, due to inlining
+{- RULES
+"showFinType/++" forall x s. showFinType x ++ s = showsFinType x s
+ -}
+
+
+-- | Like 'shows', except it shows the type itself instead of the
+-- value.
+showsFinType :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> ShowS
+showsFinType x = ("Fin "++) . shows (reflect (fin2proxy x))
+{-# INLINE [0] showsFinType #-}
+-- TODO: Is [0] the best level to start inlining showsFinType?
+{-# RULES
+"showsFinType/++" forall x s1 s2.
+ showsFinType x s1 ++ s2 = showsFinType x (s1 ++ s2)
+ #-}
+
+-- TODO: showsPrecFinType?
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Read, since that would inject invalid numbers!
+instance (NatLE n MaxBoundInt16, Nat n) => Read (Fin n) where
+ readsPrec d =
+ readParen (d > 10) $ \s0 -> do
+ ("Fin", s1) <- lex s0
+ (i, s2) <- readsPrec 11 s1
+ maybe [] (\n -> [(n,s2)]) (toFin i)
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt16, Nat n) => Eq (Fin n) where
+ Fin i == Fin j = i == j
+ Fin i /= Fin j = i /= j
+ {-# INLINE (==) #-}
+ {-# INLINE (/=) #-}
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt16, Nat n) => Ord (Fin n) where
+ Fin i < Fin j = i < j
+ Fin i <= Fin j = i <= j
+ Fin i > Fin j = i > j
+ Fin i >= Fin j = i >= j
+ compare (Fin i) (Fin j) = compare i j
+ min (Fin i) (Fin j) = Fin (min i j)
+ max (Fin i) (Fin j) = Fin (max i j)
+ {-# INLINE (<) #-}
+ {-# INLINE (<=) #-}
+ {-# INLINE (>) #-}
+ {-# INLINE (>=) #-}
+ {-# INLINE compare #-}
+ {-# INLINE min #-}
+ {-# INLINE max #-}
+
+----------------------------------------------------------------
+instance (NatLE n MaxBoundInt16, Nat n) => Bounded (Fin n) where
+ minBound = Fin 0
+ maxBound = Fin (fromInteger (reflect (Proxy :: Proxy n) - 1))
+ {-# INLINE minBound #-}
+ {-# INLINE maxBound #-}
+
+
+-- | Return the 'minBound' of @Fin n@ as a plain integer. This is
+-- always zero, but is provided for symmetry with 'maxBoundOf'.
+minBoundOf :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> Int16
+minBoundOf _ = 0
+{-# INLINE minBoundOf #-}
+
+
+-- | Return the 'maxBound' of @Fin n@ as a plain integer. This is
+-- always @n-1@, but it's helpful because you may not know what
+-- @n@ is at the time.
+maxBoundOf :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> Int16
+maxBoundOf x = fromInteger (reflect (fin2proxy x) - 1)
+{-# INLINE maxBoundOf #-}
+
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Enum, since that would inject invalid numbers!
+-- N.B., we're using partial functions, because H98 requires it!
+instance (NatLE n MaxBoundInt16, Nat n) => Enum (Fin n) where
+ succ x =
+ case SE.succ x of
+ Just y -> y
+ Nothing -> _succ_maxBound "Fin.Int16" -- cf, @GHC.Word.succError@
+ {-# INLINE succ #-}
+
+ pred x =
+ case SE.pred x of
+ Just y -> y
+ Nothing -> _pred_minBound "Fin.Int16" -- cf, @GHC.Word.predError@
+ {-# INLINE pred #-}
+
+ toEnum i =
+ case SE.toEnum i of
+ Just y -> y
+ Nothing -> _toEnum_OOR "Fin.Int16" -- cf, @GHC.Word.toEnumError@
+ {-# INLINE toEnum #-}
+
+ fromEnum = fromIntegral . fromFin
+ {-# INLINE fromEnum #-}
+
+ -- Hopefully list fusion will get rid of the map, and preserve
+ -- the fusion tricks in GHC.Enum...
+ enumFrom x@(Fin i) = map Fin (enumFromTo i (maxBoundOf x))
+ enumFromThen x@(Fin i) (Fin j)
+ | j >= i = map Fin (enumFromThenTo i j (maxBoundOf x))
+ | otherwise = map Fin (enumFromThenTo i j (minBoundOf x))
+ enumFromTo (Fin i) (Fin k) = map Fin (enumFromTo i k)
+ enumFromThenTo (Fin i) (Fin j) (Fin k) = map Fin (enumFromThenTo i j k)
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromTo #-}
+ {-# INLINE enumFromThenTo #-}
+
+{-
+_pred_succ :: Nat n => Fin n -> Fin n
+_pred_succ x = if x == maxBound then _succ_maxBound "Fin.Int16" else x
+{-# INLINE _pred_succ #-}
+
+_succ_pred :: Nat n => Fin n -> Fin n
+_succ_pred x = if x == minBound then _pred_minBound "Fin.Int16" else x
+{-# INLINE _succ_pred #-}
+
+-- BUG: how can we introduce the (Nat n) constraint? Floating out the RHSs to give them signatures doesn't help.
+{-# RULES
+"pred (succ x) :: Fin n" forall x. pred (succ x) = _pred_succ x
+"pred . succ :: Fin n -> Fin n" pred . succ = _pred_succ
+
+"succ (pred x) :: Fin n" forall x. succ (pred x) = _succ_pred x
+"succ . pred :: Fin n -> Fin n" succ . pred = _succ_pred
+ #-}
+-}
+
+instance (NatLE n MaxBoundInt16, Nat n) => SE.UpwardEnum (Fin n) where
+ succ x@(Fin i)
+ | x < maxBound = Just $! Fin (i + 1)
+ | otherwise = Nothing
+ succeeds = (>)
+ enumFrom = enumFrom
+ enumFromTo = enumFromTo
+ {-# INLINE succ #-}
+ {-# INLINE succeeds #-}
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromTo #-}
+
+instance (NatLE n MaxBoundInt16, Nat n) => SE.DownwardEnum (Fin n) where
+ pred (Fin i)
+ | 0 < i = Just $! Fin (i - 1)
+ | otherwise = Nothing
+ precedes = (<)
+ enumDownFrom (Fin i) = map Fin (enumFromThenTo i (i-1) 0)
+ enumDownFromTo (Fin i) (Fin k) = map Fin (enumFromThenTo i (i-1) (max 0 k))
+ {-# INLINE pred #-}
+ {-# INLINE precedes #-}
+ {-# INLINE enumDownFrom #-}
+ {-# INLINE enumDownFromTo #-}
+
+instance (NatLE n MaxBoundInt16, Nat n) => SE.Enum (Fin n) where
+ toEnum i
+ | 0 <= j && j <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ j = fromIntegral i
+ x = Fin j :: Fin n
+ fromEnum x = Just $! (fromIntegral . fromFin) x
+ enumFromThen = enumFromThen
+ enumFromThenTo = enumFromThenTo
+ {-# INLINE toEnum #-}
+ {-# INLINE fromEnum #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromThenTo #-}
+
+
+-- TODO: can we trust the validity of the input arguments?
+instance (NatLE n MaxBoundInt16, Nat n) => Ix (Fin n) where
+ index (Fin i, Fin j) (Fin k) = index (i,j) k
+ range (Fin i, Fin j) = map Fin (range (i,j))
+ inRange (Fin i, Fin j) (Fin k) = inRange (i,j) k
+ rangeSize (Fin i, Fin j) = rangeSize (i,j)
+
+
+----------------------------------------------------------------
+-- TODO: define Num, Real, Integral? (N.B., Can't derive them safely.)
+
+
+----------------------------------------------------------------
+-- TODO: why was the checking stuff done using exceptions instead of Maybe?
+-- TODO: can we successfully ensure that invalid values can *never* be constructed?
+
+
+-- | A version of 'const' which checks that the second argument is
+-- in fact valid for its type before returning the first argument.
+-- Throws an exception if the @Fin n@ is invalid. The name and
+-- argument ordering are indended for infix use.
+checking :: (NatLE n MaxBoundInt16, Nat n) => a -> Fin n -> a
+checking a x
+ | minBound <= x && x <= maxBound = a
+ | otherwise = _checking_OOR x
+{-# INLINE checking #-}
+
+
+-- TODO: use extensible-exceptions instead of 'error'
+_checking_OOR :: (NatLE n MaxBoundInt16, Nat n) => Fin n -> a
+_checking_OOR x = error
+ . ("The value "++)
+ . shows x
+ . (" is out of bounds for "++)
+ . showsFinType x
+ $ ". This is a library error; contact the maintainer."
+
+
+-- | Extract the value of a @Fin n@.
+--
+-- /N.B.,/ if somehow the @Fin n@ value was constructed invalidly,
+-- then this function will throw an exception. However, this should
+-- /never/ 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
+fromFin x@(Fin i) = i `checking` x
+{-# INLINE fromFin #-}
+
+
+-- | Safely embed a number into @Fin n@. Use of this function will
+-- generally require an explicit type signature in order to know
+-- which @n@ to use.
+toFin :: (NatLE n MaxBoundInt16, Nat n) => Int16 -> Maybe (Fin n)
+toFin = toFin_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous?
+ toFin_ :: forall n. (NatLE n MaxBoundInt16, Nat n)
+ => Int16 -> Maybe (Fin n)
+ toFin_ i
+ | 0 <= i && i <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ x = Fin i :: Fin n
+ {-# INLINE toFin_ #-}
+{-# INLINE toFin #-}
+
+-- TODO: RULES for toFin.fromFin and fromFin.toFin
+
+
+-- | Safely embed a number into @Fin n@. This variant of 'toFin'
+-- uses a proxy to avoid the need for type signatures.
+toFinProxy :: (NatLE n MaxBoundInt16, Nat n)
+ => Proxy n -> Int16 -> Maybe (Fin n)
+toFinProxy _ = toFin
+{-# INLINE toFinProxy #-}
+
+
+-- | Safely embed integers into @Fin n@, where @n@ is the first
+-- argument. We use rank-2 polymorphism to render the type-level
+-- @n@ existentially quantified, thereby hiding the dependent type
+-- from the compiler. However, @n@ will in fact be a skolem, so we
+-- can't provide the continuation with proof that @Nat n@ ---
+-- unfortunately, rendering this function of little use.
+--
+-- > toFinCPS n k i
+-- > | 0 <= i && i < n = Just (k i) -- morally speaking...
+-- > | otherwise = Nothing
+--
+toFinCPS :: Int16 -> (forall n. Reifies n Integer => Fin n -> r) -> Int16 -> Maybe r
+toFinCPS n k i
+ | 0 <= i && i < n = Just (reify (toInteger n) $ \(_ :: Proxy n) -> k (Fin i :: Fin n))
+ | otherwise = Nothing
+{-# INLINE toFinCPS #-}
+-- BUG: can't use @Nat n@ because: Could not deduce (Nat_ n) from the context (Reifies n Integer)
+-- TODO: how can we get Data.Number.Fin.TyDecimal.reifyNat to work?
+
+
+----------------------------------------------------------------
+instance (NatLE n MaxBoundInt16, Nat n) => QC.Arbitrary (Fin n) where
+ shrink = tail . SE.enumDownFrom
+ arbitrary
+ | x >= 0 = (Fin . fromInteger) `liftM` QC.choose (0,x)
+ | otherwise =
+ -- BUG: there's no way to say it's impossible...
+ error . ("Arbitrary.arbitrary{"++)
+ . showsFinType (__ :: Fin n)
+ $ "}: this type is empty"
+ -- TODO: use extensible-exceptions instead of 'error'
+ where
+ -- BUG: no instance Random Int16
+ x = toInteger (maxBoundOf (__ :: Fin n))
+
+
+
+instance (NatLE n MaxBoundInt16, Nat n) => QC.CoArbitrary (Fin n) where
+ coarbitrary (Fin n) = QC.variant n
+
+
+instance (NatLE n MaxBoundInt16, Nat n) => SC.Serial (Fin n) where
+ series d
+ | d < 0 = [] -- paranoia.
+ | otherwise =
+ case toFin (fromIntegral d) of
+ Nothing -> enumFromTo minBound maxBound
+ Just n -> enumFromTo minBound n
+
+ coseries rs d =
+ [ \(Fin i) ->
+ if i > 0
+ then let j = Fin (i-1) :: Fin n
+ in f j `checking` j -- more paranoia; in case n==0 or i>n
+ else z
+ | z <- SC.alts0 rs d
+ , f <- SC.alts1 rs d
+ ]
+
+instance (NatLE n MaxBoundInt16, Nat n) => LSC.Serial (Fin n) where
+ series = LSC.drawnFrom . SC.series
+
+
+----------------------------------------------------------------
+-- TODO: do we care about <http://ncatlab.org/nlab/show/decalage>?
+
+
+-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe?
+{- -- Agda's version:
+data MaxView {n : Nat} : Fin (suc n) -> Set where
+ theMax : MaxView (fromNat n)
+ notMax : (i : Fin n) -> MaxView (weaken i)
+
+maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i
+maxView {zero} zero = theMax
+maxView {zero} (suc ())
+maxView {suc n} zero = notMax zero
+maxView {suc n} (suc i) with maxView i
+maxView {suc n} (suc .(fromNat n)) | theMax = theMax
+maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i)
+-}
+-- | The maximum-element view. This strengthens the type by removing
+-- the maximum element:
+--
+-- > maxView maxBound = Nothing
+-- > maxView x = Just x -- morally speaking...
+--
+-- The opposite of this function is 'weaken'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+maxView
+ :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, Succ m n)
+ => Fin n -> Maybe (Fin m)
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n); so can't use maxViewLE as the implementation.
+-- BUG: Could not deduce (NatLE m MaxBoundInt16) from the context (NatLE n MaxBoundInt16, Succ m n); so we have to add it.
+maxView = maxView_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@...
+ maxView_ :: forall m n. (NatLE m MaxBoundInt16) => Fin n -> Maybe (Fin m)
+ maxView_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxView_ #-}
+{-# INLINE maxView #-}
+
+
+-- | A variant of 'maxView' which allows strengthening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @m@ to use.
+--
+-- The opposite of this function is 'weakenLE'. When the choice of
+-- @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+maxViewLE
+ :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE m n)
+ => Fin n -> Maybe (Fin m)
+-- BUG: Could not deduce (NatLE m MaxBoundInt16) from the context (NatLE n MaxBoundInt16, Succ m n); so we have to add it.
+maxViewLE = maxViewLE_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ maxViewLE_ :: forall m n. (NatLE m MaxBoundInt16) => Fin n -> Maybe (Fin m)
+ maxViewLE_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxViewLE_ #-}
+{-# INLINE maxViewLE #-}
+
+
+-- TODO: maxViewPlus?
+
+
+-- This type-restricted version is a~la Agda.
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'minBound'. That is,
+--
+-- > fromFin (weaken x) == fromFin x
+--
+-- The opposite of this function is 'maxView'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+weaken :: (NatLE n MaxBoundInt16, Succ m n) => Fin m -> Fin n
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n)
+weaken (Fin i) = Fin i
+{-# INLINE weaken #-}
+
+
+-- | A variant of 'weaken' which allows weakening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @n@ to use.
+--
+-- The opposite of this function is 'maxViewLE'. When the choice
+-- of @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+weakenLE :: (NatLE n MaxBoundInt16, NatLE m n) => Fin m -> Fin n
+weakenLE (Fin i) = Fin i
+{-# INLINE weakenLE #-}
+
+
+----------------------------------------------------------------
+-- | The predecessor view. This strengthens the type by shifting
+-- everything down by one:
+--
+-- > predView 0 = Nothing
+-- > predView x = Just (x-1) -- morally speaking...
+--
+-- The opposite of this function is 'widen'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+predView :: (NatLE n MaxBoundInt16, Succ m n) => Fin n -> Maybe (Fin m)
+predView (Fin i)
+ | i <= 0 = Nothing
+ | otherwise = Just $! Fin (i-1)
+{-# INLINE predView #-}
+
+
+-- TODO: predViewLE? predViewPlus?
+
+
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'maxBound'. That is, we shift everything
+-- up by one:
+--
+-- > fromFin (widen x) == 1 + fromFin x
+--
+-- The opposite of this function is 'predView'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+widen :: (NatLE n MaxBoundInt16, Succ m n) => Fin m -> Fin n
+widen (Fin i) = Fin (i+1)
+{-# INLINE widen #-}
+
+
+-- | Embed a finite domain into any larger one, keeping the same
+-- position relative to 'maxBound'. That is,
+--
+-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
+-- > where y = widenLE x
+--
+-- Use of this function will generally require an explicit type
+-- signature in order to know which @n@ to use.
+widenLE
+ :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE m n)
+ => Fin m -> Fin n
+-- BUG: Could not deduce (NatLE m MaxBoundInt16) from the context (NatLE n MaxBoundInt16, NatLE m n); so we have to add it.
+widenLE x@(Fin i) = y
+ where
+ y = Fin (maxBoundOf y - maxBoundOf x + i)
+{-# INLINE widenLE #-}
+
+
+----------------------------------------------------------------
+-- BUG: Could not deduce (NatLE m o) from the context (Add m n o)
+-- | A type-signature variant of 'weakenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE m o@. This is the
+-- left half of 'plus'.
+weakenPlus :: (NatLE o MaxBoundInt16, Add m n o) => Fin m -> Fin o
+weakenPlus (Fin i) = Fin i
+{-# INLINE weakenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE n o) from the context (Add m n o)
+-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it.
+-- | A type-signature variant of 'widenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE n o@. This is the
+-- right half of 'plus'.
+widenPlus
+ :: ( NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16
+ , Add m n o)
+ => Fin n -> Fin o
+widenPlus = widenPlus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ widenPlus_ :: forall m n o
+ . (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, Add m n o)
+ => Fin n -> Fin o
+ widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y)
+ {-# INLINE widenPlus_ #-}
+{-# INLINE widenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it.
+-- | The ordinal-sum functor, on objects. This internalizes the
+-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ 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
+plus = either weakenPlus widenPlus
+{-# INLINE plus #-}
+
+
+-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it.
+-- | The inverse of 'plus'.
+unplus
+ :: ( NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16
+ , Add m n o)
+ => Fin o -> Either (Fin m) (Fin n)
+unplus = unplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ unplus_ :: forall m n o. (NatLE m MaxBoundInt16)
+ => Fin o -> Either (Fin m) (Fin n)
+ unplus_ (Fin i)
+ | i <= x = Left $! Fin i
+ | otherwise = Right $! Fin (i-x)
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE unplus_ #-}
+{-# INLINE unplus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- BUG: Ditto for (Add m' n' o')
+-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it.
+-- | 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
+-- @(+++)@ from "Control.Arrow".
+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') -- ^ The left morphism
+ -> (Fin n -> Fin n') -- ^ The right morphism
+ -> (Fin o -> Fin o') -- ^
+fplus = fplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ fplus_ :: forall m n o m' n' o'
+ . ( 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'
+ fplus_ f g (Fin i)
+ | i <= x = weakenPlus (f $! Fin i)
+ | otherwise = widenPlus (g $! Fin (i-x))
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE fplus_ #-}
+{-# INLINE fplus #-}
+
+
+-- TODO: (Fin m, Fin n) <-> Fin (Times m n)
+
+----------------------------------------------------------------
+{- -- Agda's version:
+thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n)
+thin zero j = suc j
+thin (suc i) zero = zero
+thin (suc i) (suc j) = suc (thin i j)
+-}
+-- | The \"face maps\" for @Fin@ viewed as the standard simplices
+-- (aka: the thinning view). Traditionally spelled with delta or
+-- epsilon. For each @i@, it is the unique injective monotonic map
+-- that skips @i@. That is,
+--
+-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thin i j /= i
+--
+thin :: (NatLE n MaxBoundInt16, Succ m n) => Fin n -> Fin m -> Fin n
+thin i j
+ | weaken j < i = weaken j
+ | otherwise = succ (weaken j)
+{-# INLINE thin #-}
+
+
+-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it.
+-- | The \"degeneracy maps\" for @Fin@ viewed as the standard
+-- simplices. Traditionally spelled with sigma or eta. For each
+-- @i@, it is the unique surjective monotonic map that covers @i@
+-- twice. That is,
+--
+-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thick i (i+1) == i
+--
+thick
+ :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, Succ m n)
+ => Fin m -> Fin n -> Fin m
+thick i j =
+ case maxView (if j <= weaken i then j else pred j) of
+ Just j' -> j'
+ Nothing -> _thick_impossible
+{-# INLINE thick #-}
+
+
+
+{-
+-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne?
+-- The non zero view, which is used for defining compare...
+data NonEmptyView : {n : Nat} -> Fin n -> Set where
+ ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i
+
+nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i
+nonEmpty zero = ne
+nonEmpty (suc _) = ne
+
+
+data EqView : {n : Nat} -> Fin n -> Fin n -> Set where
+ equal : {n : Nat}{i : Fin n} -> EqView i i
+ notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j)
+
+compare : {n : Nat}(i j : Fin n) -> EqView i j
+compare zero zero = equal
+compare zero (suc j) = notequal j
+compare (suc i) zero with nonEmpty i
+... | ne = notequal zero
+compare (suc i) (suc j) with compare i j
+compare (suc i) (suc .i) | equal = equal
+compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j)
+-}
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- Error messages
+
+__ :: a
+__ = error "Data.Number.Fin.Int16: attempted to evaluate type token"
+{-# NOINLINE __ #-}
+-- TODO: use extensible-exceptions instead of 'error'
+-- TODO: use Proxy instead of these undefined values...
+
+_thick_impossible :: a
+_thick_impossible =
+ error "Data.Number.Fin.Int16.thick: the impossible happened"
+{-# NOINLINE _thick_impossible #-}
+-- TODO: use extensible-exceptions instead of 'error'
+
+_succ_maxBound :: String -> a
+_succ_maxBound ty =
+ error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound"
+{-# NOINLINE _succ_maxBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_pred_minBound :: String -> a
+_pred_minBound ty =
+ error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound"
+{-# NOINLINE _pred_minBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_toEnum_OOR :: String -> a
+_toEnum_OOR ty =
+ error $ "Enum.toEnum{"++ty++"}: argument out of range"
+{-# NOINLINE _toEnum_OOR #-}
+-- TODO: is there an extensible-exception for this?
+
+----------------------------------------------------------------
+----------------------------------------------------------- fin.
diff --git a/src/Data/Number/Fin/Int32.hs b/src/Data/Number/Fin/Int32.hs
new file mode 100644
index 0000000..a6628ef
--- /dev/null
+++ b/src/Data/Number/Fin/Int32.hs
@@ -0,0 +1,865 @@
+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+{-# LANGUAGE ScopedTypeVariables
+ , DeriveDataTypeable
+ , MultiParamTypeClasses
+ , FlexibleContexts
+ , CPP
+ , Rank2Types
+ , UndecidableInstances
+ #-}
+
+#if __GLASGOW_HASKELL__ >= 701
+-- N.B., Data.Proxy and Test.QuickCheck aren't "safe".
+{-# LANGUAGE Trustworthy #-}
+#endif
+----------------------------------------------------------------
+-- 2013.05.29
+-- |
+-- Module : Data.Number.Fin.Int32
+-- Copyright : 2012--2013 wren ng thornton
+-- License : BSD3
+-- Maintainer : wren@community.haskell.org
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- A newtype of 'Int32' for finite subsets of the natural numbers.
+----------------------------------------------------------------
+module Data.Number.Fin.Int32
+ (
+ -- * @Fin@, finite sets of natural numbers
+ Fin()
+
+ -- ** Showing types
+ , showFinType
+ , showsFinType
+
+ -- ** Convenience functions
+ , minBoundOf
+ , maxBoundOf
+
+ -- ** Introduction and elimination
+ , toFin
+ , toFinProxy
+ , toFinCPS
+ , fromFin
+
+ -- ** Views and coersions
+ -- *** Weakening and maximum views
+ , weaken
+ , weakenLE
+ , weakenPlus
+ , maxView
+ , maxViewLE
+
+ -- *** Widening and the predecessor view
+ , widen
+ , widenLE
+ , widenPlus
+ , predView
+
+ -- *** The ordinal-sum functor
+ , plus
+ , unplus
+ , fplus
+
+ -- *** Face- and degeneracy-maps
+ , thin
+ , thick
+ -- TODO: is there any way to get equality to work right?
+ ) where
+
+import qualified Prelude.SafeEnum as SE
+import Data.Int (Int32)
+import Data.Ix
+import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE, MaxBoundInt32)
+import Data.Typeable (Typeable)
+import Data.Proxy (Proxy(Proxy))
+import Data.Reflection (Reifies(reflect), reify)
+import Control.Monad (liftM)
+
+import qualified Test.QuickCheck as QC
+#if (MIN_VERSION_smallcheck(0,6,0))
+import qualified Test.SmallCheck.Series as SC
+#else
+import qualified Test.SmallCheck as SC
+#endif
+import qualified Test.LazySmallCheck as LSC
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- | A finite set of integers @Fin n = { i :: Int32 | 0 <= i < n }@
+-- with the usual ordering. This is typed as if using the standard
+-- GADT presentation of @Fin n@, however it is actually implemented
+-- by a plain 'Int32'.
+newtype Fin n = Fin Int32
+ deriving Typeable
+ -- WART: to give additional constraints (e.g., Nat n) on derived
+ -- instances (e.g., Show, Eq, Ord), we need to specify the
+ -- constraints on the data type declaration; however, giving of
+ -- data-type constraints is deprecated and will be removed from
+ -- the language...
+
+{-
+-- Some fusion rules for treating newtypes like 'id', or as close
+-- as we can. We only have these fire in the last stage so that
+-- they don't inhibit the usual list-fusion rules. Hopefully there's
+-- nothing important which is defined to not fire at [0].
+--
+-- TODO: add other laws regarding 'id'
+{-# RULES
+"map Fin" [0] map Fin = unsafeCoerce
+"fmap Fin" [0] fmap Fin = unsafeCoerce
+"liftM Fin" [0] liftM Fin = unsafeCoerce
+"liftA Fin" [0] liftA Fin = unsafeCoerce
+ #-}
+-}
+
+{- TODO:
+-- also: <http://paczesiowa.blogspot.com/2010/01/pure-extensible-exceptions-and-self.html>
+
+-- | An error for attempts to evaluate an undefined value which is
+-- passed around as a type token. The string should give the source
+-- where the token was generated, or some other helpful information
+-- for tracking the problem down.
+data EvaluatedTypeTokenException = EvaluatedTypeTokenException String
+ deriving (Typeable, Show)
+
+instance Exception EvaluatedTypeTokenException
+
+-- | Construct a type token with the given message.
+__ :: String -> a
+__ here = throw (EvaluatedTypeTokenException here)
+
+
+-- TODO: use Control.Exception.assert instead?
+data FinException = FinOOB (Fin n)
+ deriving (Typeable)
+
+instance Show FinException where
+ show (FinOOB x) =
+ "Value "++show x++" out of bounds for "++showFinType x
+
+instance Exception FinException
+-}
+
+
+-- | Often, we don't want to use the @Fin n@ as a proxy, since that
+-- would introduce spurious data dependencies. This function ignores
+-- its argument (other than for type propagation) so, hopefully,
+-- via massive inlining this function will avoid that spurious
+-- dependency. Hopefully...
+--
+-- Also, this lets us minimize the use of @-XScopedTypeVariables@
+-- which makes the Haddocks ugly. And so it lets us avoid the hacks
+-- to hide our use of @-XScopedTypeVariables@.
+--
+-- TODO: is this enough to ensure reflection is/can-be done at compile-time?
+-- TODO: is there any way to tell GHC that this function should /never/ appear in the output of compilation?
+fin2proxy :: (NatLE n MaxBoundInt32, Nat n) => fin n -> Proxy n
+fin2proxy _ = Proxy
+{-# INLINE fin2proxy #-}
+
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt32, Nat n) => Show (Fin n) where
+ showsPrec d (Fin i) =
+ showParen (d > 10) $ ("Fin "++) . shows i
+
+
+-- | Like 'show', except it shows the type itself instead of the
+-- value.
+showFinType :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> String
+showFinType x = showsFinType x []
+{-# INLINE showFinType #-}
+-- Should never fire, due to inlining
+{- RULES
+"showFinType/++" forall x s. showFinType x ++ s = showsFinType x s
+ -}
+
+
+-- | Like 'shows', except it shows the type itself instead of the
+-- value.
+showsFinType :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> ShowS
+showsFinType x = ("Fin "++) . shows (reflect (fin2proxy x))
+{-# INLINE [0] showsFinType #-}
+-- TODO: Is [0] the best level to start inlining showsFinType?
+{-# RULES
+"showsFinType/++" forall x s1 s2.
+ showsFinType x s1 ++ s2 = showsFinType x (s1 ++ s2)
+ #-}
+
+-- TODO: showsPrecFinType?
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Read, since that would inject invalid numbers!
+instance (NatLE n MaxBoundInt32, Nat n) => Read (Fin n) where
+ readsPrec d =
+ readParen (d > 10) $ \s0 -> do
+ ("Fin", s1) <- lex s0
+ (i, s2) <- readsPrec 11 s1
+ maybe [] (\n -> [(n,s2)]) (toFin i)
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt32, Nat n) => Eq (Fin n) where
+ Fin i == Fin j = i == j
+ Fin i /= Fin j = i /= j
+ {-# INLINE (==) #-}
+ {-# INLINE (/=) #-}
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt32, Nat n) => Ord (Fin n) where
+ Fin i < Fin j = i < j
+ Fin i <= Fin j = i <= j
+ Fin i > Fin j = i > j
+ Fin i >= Fin j = i >= j
+ compare (Fin i) (Fin j) = compare i j
+ min (Fin i) (Fin j) = Fin (min i j)
+ max (Fin i) (Fin j) = Fin (max i j)
+ {-# INLINE (<) #-}
+ {-# INLINE (<=) #-}
+ {-# INLINE (>) #-}
+ {-# INLINE (>=) #-}
+ {-# INLINE compare #-}
+ {-# INLINE min #-}
+ {-# INLINE max #-}
+
+----------------------------------------------------------------
+instance (NatLE n MaxBoundInt32, Nat n) => Bounded (Fin n) where
+ minBound = Fin 0
+ maxBound = Fin (fromInteger (reflect (Proxy :: Proxy n) - 1))
+ {-# INLINE minBound #-}
+ {-# INLINE maxBound #-}
+
+
+-- | Return the 'minBound' of @Fin n@ as a plain integer. This is
+-- always zero, but is provided for symmetry with 'maxBoundOf'.
+minBoundOf :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> Int32
+minBoundOf _ = 0
+{-# INLINE minBoundOf #-}
+
+
+-- | Return the 'maxBound' of @Fin n@ as a plain integer. This is
+-- always @n-1@, but it's helpful because you may not know what
+-- @n@ is at the time.
+maxBoundOf :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> Int32
+maxBoundOf x = fromInteger (reflect (fin2proxy x) - 1)
+{-# INLINE maxBoundOf #-}
+
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Enum, since that would inject invalid numbers!
+-- N.B., we're using partial functions, because H98 requires it!
+instance (NatLE n MaxBoundInt32, Nat n) => Enum (Fin n) where
+ succ x =
+ case SE.succ x of
+ Just y -> y
+ Nothing -> _succ_maxBound "Fin.Int32" -- cf, @GHC.Word.succError@
+ {-# INLINE succ #-}
+
+ pred x =
+ case SE.pred x of
+ Just y -> y
+ Nothing -> _pred_minBound "Fin.Int32" -- cf, @GHC.Word.predError@
+ {-# INLINE pred #-}
+
+ toEnum i =
+ case SE.toEnum i of
+ Just y -> y
+ Nothing -> _toEnum_OOR "Fin.Int32" -- cf, @GHC.Word.toEnumError@
+ {-# INLINE toEnum #-}
+
+ fromEnum = fromIntegral . fromFin
+ {-# INLINE fromEnum #-}
+
+ -- Hopefully list fusion will get rid of the map, and preserve
+ -- the fusion tricks in GHC.Enum...
+ enumFrom x@(Fin i) = map Fin (enumFromTo i (maxBoundOf x))
+ enumFromThen x@(Fin i) (Fin j)
+ | j >= i = map Fin (enumFromThenTo i j (maxBoundOf x))
+ | otherwise = map Fin (enumFromThenTo i j (minBoundOf x))
+ enumFromTo (Fin i) (Fin k) = map Fin (enumFromTo i k)
+ enumFromThenTo (Fin i) (Fin j) (Fin k) = map Fin (enumFromThenTo i j k)
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromTo #-}
+ {-# INLINE enumFromThenTo #-}
+
+{-
+_pred_succ :: Nat n => Fin n -> Fin n
+_pred_succ x = if x == maxBound then _succ_maxBound "Fin.Int32" else x
+{-# INLINE _pred_succ #-}
+
+_succ_pred :: Nat n => Fin n -> Fin n
+_succ_pred x = if x == minBound then _pred_minBound "Fin.Int32" else x
+{-# INLINE _succ_pred #-}
+
+-- BUG: how can we introduce the (Nat n) constraint? Floating out the RHSs to give them signatures doesn't help.
+{-# RULES
+"pred (succ x) :: Fin n" forall x. pred (succ x) = _pred_succ x
+"pred . succ :: Fin n -> Fin n" pred . succ = _pred_succ
+
+"succ (pred x) :: Fin n" forall x. succ (pred x) = _succ_pred x
+"succ . pred :: Fin n -> Fin n" succ . pred = _succ_pred
+ #-}
+-}
+
+instance (NatLE n MaxBoundInt32, Nat n) => SE.UpwardEnum (Fin n) where
+ succ x@(Fin i)
+ | x < maxBound = Just $! Fin (i + 1)
+ | otherwise = Nothing
+ succeeds = (>)
+ enumFrom = enumFrom
+ enumFromTo = enumFromTo
+ {-# INLINE succ #-}
+ {-# INLINE succeeds #-}
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromTo #-}
+
+instance (NatLE n MaxBoundInt32, Nat n) => SE.DownwardEnum (Fin n) where
+ pred (Fin i)
+ | 0 < i = Just $! Fin (i - 1)
+ | otherwise = Nothing
+ precedes = (<)
+ enumDownFrom (Fin i) = map Fin (enumFromThenTo i (i-1) 0)
+ enumDownFromTo (Fin i) (Fin k) = map Fin (enumFromThenTo i (i-1) (max 0 k))
+ {-# INLINE pred #-}
+ {-# INLINE precedes #-}
+ {-# INLINE enumDownFrom #-}
+ {-# INLINE enumDownFromTo #-}
+
+instance (NatLE n MaxBoundInt32, Nat n) => SE.Enum (Fin n) where
+ toEnum i
+ | 0 <= j && j <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ j = fromIntegral i
+ x = Fin j :: Fin n
+ fromEnum x = Just $! (fromIntegral . fromFin) x
+ enumFromThen = enumFromThen
+ enumFromThenTo = enumFromThenTo
+ {-# INLINE toEnum #-}
+ {-# INLINE fromEnum #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromThenTo #-}
+
+
+-- TODO: can we trust the validity of the input arguments?
+instance (NatLE n MaxBoundInt32, Nat n) => Ix (Fin n) where
+ index (Fin i, Fin j) (Fin k) = index (i,j) k
+ range (Fin i, Fin j) = map Fin (range (i,j))
+ inRange (Fin i, Fin j) (Fin k) = inRange (i,j) k
+ rangeSize (Fin i, Fin j) = rangeSize (i,j)
+
+
+----------------------------------------------------------------
+-- TODO: define Num, Real, Integral? (N.B., Can't derive them safely.)
+
+
+----------------------------------------------------------------
+-- TODO: why was the checking stuff done using exceptions instead of Maybe?
+-- TODO: can we successfully ensure that invalid values can *never* be constructed?
+
+
+-- | A version of 'const' which checks that the second argument is
+-- in fact valid for its type before returning the first argument.
+-- Throws an exception if the @Fin n@ is invalid. The name and
+-- argument ordering are indended for infix use.
+checking :: (NatLE n MaxBoundInt32, Nat n) => a -> Fin n -> a
+checking a x
+ | minBound <= x && x <= maxBound = a
+ | otherwise = _checking_OOR x
+{-# INLINE checking #-}
+
+
+-- TODO: use extensible-exceptions instead of 'error'
+_checking_OOR :: (NatLE n MaxBoundInt32, Nat n) => Fin n -> a
+_checking_OOR x = error
+ . ("The value "++)
+ . shows x
+ . (" is out of bounds for "++)
+ . showsFinType x
+ $ ". This is a library error; contact the maintainer."
+
+
+-- | Extract the value of a @Fin n@.
+--
+-- /N.B.,/ if somehow the @Fin n@ value was constructed invalidly,
+-- then this function will throw an exception. However, this should
+-- /never/ 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
+fromFin x@(Fin i) = i `checking` x
+{-# INLINE fromFin #-}
+
+
+-- | Safely embed a number into @Fin n@. Use of this function will
+-- generally require an explicit type signature in order to know
+-- which @n@ to use.
+toFin :: (NatLE n MaxBoundInt32, Nat n) => Int32 -> Maybe (Fin n)
+toFin = toFin_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous?
+ toFin_ :: forall n. (NatLE n MaxBoundInt32, Nat n)
+ => Int32 -> Maybe (Fin n)
+ toFin_ i
+ | 0 <= i && i <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ x = Fin i :: Fin n
+ {-# INLINE toFin_ #-}
+{-# INLINE toFin #-}
+
+-- TODO: RULES for toFin.fromFin and fromFin.toFin
+
+
+-- | Safely embed a number into @Fin n@. This variant of 'toFin'
+-- uses a proxy to avoid the need for type signatures.
+toFinProxy :: (NatLE n MaxBoundInt32, Nat n)
+ => Proxy n -> Int32 -> Maybe (Fin n)
+toFinProxy _ = toFin
+{-# INLINE toFinProxy #-}
+
+
+-- | Safely embed integers into @Fin n@, where @n@ is the first
+-- argument. We use rank-2 polymorphism to render the type-level
+-- @n@ existentially quantified, thereby hiding the dependent type
+-- from the compiler. However, @n@ will in fact be a skolem, so we
+-- can't provide the continuation with proof that @Nat n@ ---
+-- unfortunately, rendering this function of little use.
+--
+-- > toFinCPS n k i
+-- > | 0 <= i && i < n = Just (k i) -- morally speaking...
+-- > | otherwise = Nothing
+--
+toFinCPS :: Int32 -> (forall n. Reifies n Integer => Fin n -> r) -> Int32 -> Maybe r
+toFinCPS n k i
+ | 0 <= i && i < n = Just (reify (toInteger n) $ \(_ :: Proxy n) -> k (Fin i :: Fin n))
+ | otherwise = Nothing
+{-# INLINE toFinCPS #-}
+-- BUG: can't use @Nat n@ because: Could not deduce (Nat_ n) from the context (Reifies n Integer)
+-- TODO: how can we get Data.Number.Fin.TyDecimal.reifyNat to work?
+
+
+----------------------------------------------------------------
+instance (NatLE n MaxBoundInt32, Nat n) => QC.Arbitrary (Fin n) where
+ shrink = tail . SE.enumDownFrom
+ arbitrary
+ | x >= 0 = (Fin . fromInteger) `liftM` QC.choose (0,x)
+ | otherwise =
+ -- BUG: there's no way to say it's impossible...
+ error . ("Arbitrary.arbitrary{"++)
+ . showsFinType (__ :: Fin n)
+ $ "}: this type is empty"
+ -- TODO: use extensible-exceptions instead of 'error'
+ where
+ -- BUG: no instance Random Int32
+ x = toInteger (maxBoundOf (__ :: Fin n))
+
+
+
+instance (NatLE n MaxBoundInt32, Nat n) => QC.CoArbitrary (Fin n) where
+ coarbitrary (Fin n) = QC.variant n
+
+
+instance (NatLE n MaxBoundInt32, Nat n) => SC.Serial (Fin n) where
+ series d
+ | d < 0 = [] -- paranoia.
+ | otherwise =
+ case toFin (fromIntegral d) of
+ Nothing -> enumFromTo minBound maxBound
+ Just n -> enumFromTo minBound n
+
+ coseries rs d =
+ [ \(Fin i) ->
+ if i > 0
+ then let j = Fin (i-1) :: Fin n
+ in f j `checking` j -- more paranoia; in case n==0 or i>n
+ else z
+ | z <- SC.alts0 rs d
+ , f <- SC.alts1 rs d
+ ]
+
+instance (NatLE n MaxBoundInt32, Nat n) => LSC.Serial (Fin n) where
+ series = LSC.drawnFrom . SC.series
+
+
+----------------------------------------------------------------
+-- TODO: do we care about <http://ncatlab.org/nlab/show/decalage>?
+
+
+-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe?
+{- -- Agda's version:
+data MaxView {n : Nat} : Fin (suc n) -> Set where
+ theMax : MaxView (fromNat n)
+ notMax : (i : Fin n) -> MaxView (weaken i)
+
+maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i
+maxView {zero} zero = theMax
+maxView {zero} (suc ())
+maxView {suc n} zero = notMax zero
+maxView {suc n} (suc i) with maxView i
+maxView {suc n} (suc .(fromNat n)) | theMax = theMax
+maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i)
+-}
+-- | The maximum-element view. This strengthens the type by removing
+-- the maximum element:
+--
+-- > maxView maxBound = Nothing
+-- > maxView x = Just x -- morally speaking...
+--
+-- The opposite of this function is 'weaken'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+maxView
+ :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, Succ m n)
+ => Fin n -> Maybe (Fin m)
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n); so can't use maxViewLE as the implementation.
+-- BUG: Could not deduce (NatLE m MaxBoundInt32) from the context (NatLE n MaxBoundInt32, Succ m n); so we have to add it.
+maxView = maxView_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@...
+ maxView_ :: forall m n. (NatLE m MaxBoundInt32) => Fin n -> Maybe (Fin m)
+ maxView_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxView_ #-}
+{-# INLINE maxView #-}
+
+
+-- | A variant of 'maxView' which allows strengthening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @m@ to use.
+--
+-- The opposite of this function is 'weakenLE'. When the choice of
+-- @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+maxViewLE
+ :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE m n)
+ => Fin n -> Maybe (Fin m)
+-- BUG: Could not deduce (NatLE m MaxBoundInt32) from the context (NatLE n MaxBoundInt32, Succ m n); so we have to add it.
+maxViewLE = maxViewLE_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ maxViewLE_ :: forall m n. (NatLE m MaxBoundInt32) => Fin n -> Maybe (Fin m)
+ maxViewLE_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxViewLE_ #-}
+{-# INLINE maxViewLE #-}
+
+
+-- TODO: maxViewPlus?
+
+
+-- This type-restricted version is a~la Agda.
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'minBound'. That is,
+--
+-- > fromFin (weaken x) == fromFin x
+--
+-- The opposite of this function is 'maxView'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+weaken :: (NatLE n MaxBoundInt32, Succ m n) => Fin m -> Fin n
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n)
+weaken (Fin i) = Fin i
+{-# INLINE weaken #-}
+
+
+-- | A variant of 'weaken' which allows weakening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @n@ to use.
+--
+-- The opposite of this function is 'maxViewLE'. When the choice
+-- of @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+weakenLE :: (NatLE n MaxBoundInt32, NatLE m n) => Fin m -> Fin n
+weakenLE (Fin i) = Fin i
+{-# INLINE weakenLE #-}
+
+
+----------------------------------------------------------------
+-- | The predecessor view. This strengthens the type by shifting
+-- everything down by one:
+--
+-- > predView 0 = Nothing
+-- > predView x = Just (x-1) -- morally speaking...
+--
+-- The opposite of this function is 'widen'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+predView :: (NatLE n MaxBoundInt32, Succ m n) => Fin n -> Maybe (Fin m)
+predView (Fin i)
+ | i <= 0 = Nothing
+ | otherwise = Just $! Fin (i-1)
+{-# INLINE predView #-}
+
+
+-- TODO: predViewLE? predViewPlus?
+
+
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'maxBound'. That is, we shift everything
+-- up by one:
+--
+-- > fromFin (widen x) == 1 + fromFin x
+--
+-- The opposite of this function is 'predView'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+widen :: (NatLE n MaxBoundInt32, Succ m n) => Fin m -> Fin n
+widen (Fin i) = Fin (i+1)
+{-# INLINE widen #-}
+
+
+-- | Embed a finite domain into any larger one, keeping the same
+-- position relative to 'maxBound'. That is,
+--
+-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
+-- > where y = widenLE x
+--
+-- Use of this function will generally require an explicit type
+-- signature in order to know which @n@ to use.
+widenLE
+ :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE m n)
+ => Fin m -> Fin n
+-- BUG: Could not deduce (NatLE m MaxBoundInt32) from the context (NatLE n MaxBoundInt32, NatLE m n); so we have to add it.
+widenLE x@(Fin i) = y
+ where
+ y = Fin (maxBoundOf y - maxBoundOf x + i)
+{-# INLINE widenLE #-}
+
+
+----------------------------------------------------------------
+-- BUG: Could not deduce (NatLE m o) from the context (Add m n o)
+-- | A type-signature variant of 'weakenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE m o@. This is the
+-- left half of 'plus'.
+weakenPlus :: (NatLE o MaxBoundInt32, Add m n o) => Fin m -> Fin o
+weakenPlus (Fin i) = Fin i
+{-# INLINE weakenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE n o) from the context (Add m n o)
+-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it.
+-- | A type-signature variant of 'widenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE n o@. This is the
+-- right half of 'plus'.
+widenPlus
+ :: ( NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32
+ , Add m n o)
+ => Fin n -> Fin o
+widenPlus = widenPlus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ widenPlus_ :: forall m n o
+ . (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, Add m n o)
+ => Fin n -> Fin o
+ widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y)
+ {-# INLINE widenPlus_ #-}
+{-# INLINE widenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it.
+-- | The ordinal-sum functor, on objects. This internalizes the
+-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ 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
+plus = either weakenPlus widenPlus
+{-# INLINE plus #-}
+
+
+-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it.
+-- | The inverse of 'plus'.
+unplus
+ :: ( NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32
+ , Add m n o)
+ => Fin o -> Either (Fin m) (Fin n)
+unplus = unplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ unplus_ :: forall m n o. (NatLE m MaxBoundInt32)
+ => Fin o -> Either (Fin m) (Fin n)
+ unplus_ (Fin i)
+ | i <= x = Left $! Fin i
+ | otherwise = Right $! Fin (i-x)
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE unplus_ #-}
+{-# INLINE unplus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- BUG: Ditto for (Add m' n' o')
+-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it.
+-- | 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
+-- @(+++)@ from "Control.Arrow".
+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') -- ^ The left morphism
+ -> (Fin n -> Fin n') -- ^ The right morphism
+ -> (Fin o -> Fin o') -- ^
+fplus = fplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ fplus_ :: forall m n o m' n' o'
+ . ( 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'
+ fplus_ f g (Fin i)
+ | i <= x = weakenPlus (f $! Fin i)
+ | otherwise = widenPlus (g $! Fin (i-x))
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE fplus_ #-}
+{-# INLINE fplus #-}
+
+
+-- TODO: (Fin m, Fin n) <-> Fin (Times m n)
+
+----------------------------------------------------------------
+{- -- Agda's version:
+thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n)
+thin zero j = suc j
+thin (suc i) zero = zero
+thin (suc i) (suc j) = suc (thin i j)
+-}
+-- | The \"face maps\" for @Fin@ viewed as the standard simplices
+-- (aka: the thinning view). Traditionally spelled with delta or
+-- epsilon. For each @i@, it is the unique injective monotonic map
+-- that skips @i@. That is,
+--
+-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thin i j /= i
+--
+thin :: (NatLE n MaxBoundInt32, Succ m n) => Fin n -> Fin m -> Fin n
+thin i j
+ | weaken j < i = weaken j
+ | otherwise = succ (weaken j)
+{-# INLINE thin #-}
+
+
+-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it.
+-- | The \"degeneracy maps\" for @Fin@ viewed as the standard
+-- simplices. Traditionally spelled with sigma or eta. For each
+-- @i@, it is the unique surjective monotonic map that covers @i@
+-- twice. That is,
+--
+-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thick i (i+1) == i
+--
+thick
+ :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, Succ m n)
+ => Fin m -> Fin n -> Fin m
+thick i j =
+ case maxView (if j <= weaken i then j else pred j) of
+ Just j' -> j'
+ Nothing -> _thick_impossible
+{-# INLINE thick #-}
+
+
+
+{-
+-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne?
+-- The non zero view, which is used for defining compare...
+data NonEmptyView : {n : Nat} -> Fin n -> Set where
+ ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i
+
+nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i
+nonEmpty zero = ne
+nonEmpty (suc _) = ne
+
+
+data EqView : {n : Nat} -> Fin n -> Fin n -> Set where
+ equal : {n : Nat}{i : Fin n} -> EqView i i
+ notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j)
+
+compare : {n : Nat}(i j : Fin n) -> EqView i j
+compare zero zero = equal
+compare zero (suc j) = notequal j
+compare (suc i) zero with nonEmpty i
+... | ne = notequal zero
+compare (suc i) (suc j) with compare i j
+compare (suc i) (suc .i) | equal = equal
+compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j)
+-}
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- Error messages
+
+__ :: a
+__ = error "Data.Number.Fin.Int32: attempted to evaluate type token"
+{-# NOINLINE __ #-}
+-- TODO: use extensible-exceptions instead of 'error'
+-- TODO: use Proxy instead of these undefined values...
+
+_thick_impossible :: a
+_thick_impossible =
+ error "Data.Number.Fin.Int32.thick: the impossible happened"
+{-# NOINLINE _thick_impossible #-}
+-- TODO: use extensible-exceptions instead of 'error'
+
+_succ_maxBound :: String -> a
+_succ_maxBound ty =
+ error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound"
+{-# NOINLINE _succ_maxBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_pred_minBound :: String -> a
+_pred_minBound ty =
+ error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound"
+{-# NOINLINE _pred_minBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_toEnum_OOR :: String -> a
+_toEnum_OOR ty =
+ error $ "Enum.toEnum{"++ty++"}: argument out of range"
+{-# NOINLINE _toEnum_OOR #-}
+-- TODO: is there an extensible-exception for this?
+
+----------------------------------------------------------------
+----------------------------------------------------------- fin.
diff --git a/src/Data/Number/Fin/Int64.hs b/src/Data/Number/Fin/Int64.hs
new file mode 100644
index 0000000..2b748ce
--- /dev/null
+++ b/src/Data/Number/Fin/Int64.hs
@@ -0,0 +1,865 @@
+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+{-# LANGUAGE ScopedTypeVariables
+ , DeriveDataTypeable
+ , MultiParamTypeClasses
+ , FlexibleContexts
+ , CPP
+ , Rank2Types
+ , UndecidableInstances
+ #-}
+
+#if __GLASGOW_HASKELL__ >= 701
+-- N.B., Data.Proxy and Test.QuickCheck aren't "safe".
+{-# LANGUAGE Trustworthy #-}
+#endif
+----------------------------------------------------------------
+-- 2013.05.29
+-- |
+-- Module : Data.Number.Fin.Int64
+-- Copyright : 2012--2013 wren ng thornton
+-- License : BSD3
+-- Maintainer : wren@community.haskell.org
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- A newtype of 'Int64' for finite subsets of the natural numbers.
+----------------------------------------------------------------
+module Data.Number.Fin.Int64
+ (
+ -- * @Fin@, finite sets of natural numbers
+ Fin()
+
+ -- ** Showing types
+ , showFinType
+ , showsFinType
+
+ -- ** Convenience functions
+ , minBoundOf
+ , maxBoundOf
+
+ -- ** Introduction and elimination
+ , toFin
+ , toFinProxy
+ , toFinCPS
+ , fromFin
+
+ -- ** Views and coersions
+ -- *** Weakening and maximum views
+ , weaken
+ , weakenLE
+ , weakenPlus
+ , maxView
+ , maxViewLE
+
+ -- *** Widening and the predecessor view
+ , widen
+ , widenLE
+ , widenPlus
+ , predView
+
+ -- *** The ordinal-sum functor
+ , plus
+ , unplus
+ , fplus
+
+ -- *** Face- and degeneracy-maps
+ , thin
+ , thick
+ -- TODO: is there any way to get equality to work right?
+ ) where
+
+import qualified Prelude.SafeEnum as SE
+import Data.Int (Int64)
+import Data.Ix
+import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE, MaxBoundInt64)
+import Data.Typeable (Typeable)
+import Data.Proxy (Proxy(Proxy))
+import Data.Reflection (Reifies(reflect), reify)
+import Control.Monad (liftM)
+
+import qualified Test.QuickCheck as QC
+#if (MIN_VERSION_smallcheck(0,6,0))
+import qualified Test.SmallCheck.Series as SC
+#else
+import qualified Test.SmallCheck as SC
+#endif
+import qualified Test.LazySmallCheck as LSC
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- | A finite set of integers @Fin n = { i :: Int64 | 0 <= i < n }@
+-- with the usual ordering. This is typed as if using the standard
+-- GADT presentation of @Fin n@, however it is actually implemented
+-- by a plain 'Int64'.
+newtype Fin n = Fin Int64
+ deriving Typeable
+ -- WART: to give additional constraints (e.g., Nat n) on derived
+ -- instances (e.g., Show, Eq, Ord), we need to specify the
+ -- constraints on the data type declaration; however, giving of
+ -- data-type constraints is deprecated and will be removed from
+ -- the language...
+
+{-
+-- Some fusion rules for treating newtypes like 'id', or as close
+-- as we can. We only have these fire in the last stage so that
+-- they don't inhibit the usual list-fusion rules. Hopefully there's
+-- nothing important which is defined to not fire at [0].
+--
+-- TODO: add other laws regarding 'id'
+{-# RULES
+"map Fin" [0] map Fin = unsafeCoerce
+"fmap Fin" [0] fmap Fin = unsafeCoerce
+"liftM Fin" [0] liftM Fin = unsafeCoerce
+"liftA Fin" [0] liftA Fin = unsafeCoerce
+ #-}
+-}
+
+{- TODO:
+-- also: <http://paczesiowa.blogspot.com/2010/01/pure-extensible-exceptions-and-self.html>
+
+-- | An error for attempts to evaluate an undefined value which is
+-- passed around as a type token. The string should give the source
+-- where the token was generated, or some other helpful information
+-- for tracking the problem down.
+data EvaluatedTypeTokenException = EvaluatedTypeTokenException String
+ deriving (Typeable, Show)
+
+instance Exception EvaluatedTypeTokenException
+
+-- | Construct a type token with the given message.
+__ :: String -> a
+__ here = throw (EvaluatedTypeTokenException here)
+
+
+-- TODO: use Control.Exception.assert instead?
+data FinException = FinOOB (Fin n)
+ deriving (Typeable)
+
+instance Show FinException where
+ show (FinOOB x) =
+ "Value "++show x++" out of bounds for "++showFinType x
+
+instance Exception FinException
+-}
+
+
+-- | Often, we don't want to use the @Fin n@ as a proxy, since that
+-- would introduce spurious data dependencies. This function ignores
+-- its argument (other than for type propagation) so, hopefully,
+-- via massive inlining this function will avoid that spurious
+-- dependency. Hopefully...
+--
+-- Also, this lets us minimize the use of @-XScopedTypeVariables@
+-- which makes the Haddocks ugly. And so it lets us avoid the hacks
+-- to hide our use of @-XScopedTypeVariables@.
+--
+-- TODO: is this enough to ensure reflection is/can-be done at compile-time?
+-- TODO: is there any way to tell GHC that this function should /never/ appear in the output of compilation?
+fin2proxy :: (NatLE n MaxBoundInt64, Nat n) => fin n -> Proxy n
+fin2proxy _ = Proxy
+{-# INLINE fin2proxy #-}
+
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt64, Nat n) => Show (Fin n) where
+ showsPrec d (Fin i) =
+ showParen (d > 10) $ ("Fin "++) . shows i
+
+
+-- | Like 'show', except it shows the type itself instead of the
+-- value.
+showFinType :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> String
+showFinType x = showsFinType x []
+{-# INLINE showFinType #-}
+-- Should never fire, due to inlining
+{- RULES
+"showFinType/++" forall x s. showFinType x ++ s = showsFinType x s
+ -}
+
+
+-- | Like 'shows', except it shows the type itself instead of the
+-- value.
+showsFinType :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> ShowS
+showsFinType x = ("Fin "++) . shows (reflect (fin2proxy x))
+{-# INLINE [0] showsFinType #-}
+-- TODO: Is [0] the best level to start inlining showsFinType?
+{-# RULES
+"showsFinType/++" forall x s1 s2.
+ showsFinType x s1 ++ s2 = showsFinType x (s1 ++ s2)
+ #-}
+
+-- TODO: showsPrecFinType?
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Read, since that would inject invalid numbers!
+instance (NatLE n MaxBoundInt64, Nat n) => Read (Fin n) where
+ readsPrec d =
+ readParen (d > 10) $ \s0 -> do
+ ("Fin", s1) <- lex s0
+ (i, s2) <- readsPrec 11 s1
+ maybe [] (\n -> [(n,s2)]) (toFin i)
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt64, Nat n) => Eq (Fin n) where
+ Fin i == Fin j = i == j
+ Fin i /= Fin j = i /= j
+ {-# INLINE (==) #-}
+ {-# INLINE (/=) #-}
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt64, Nat n) => Ord (Fin n) where
+ Fin i < Fin j = i < j
+ Fin i <= Fin j = i <= j
+ Fin i > Fin j = i > j
+ Fin i >= Fin j = i >= j
+ compare (Fin i) (Fin j) = compare i j
+ min (Fin i) (Fin j) = Fin (min i j)
+ max (Fin i) (Fin j) = Fin (max i j)
+ {-# INLINE (<) #-}
+ {-# INLINE (<=) #-}
+ {-# INLINE (>) #-}
+ {-# INLINE (>=) #-}
+ {-# INLINE compare #-}
+ {-# INLINE min #-}
+ {-# INLINE max #-}
+
+----------------------------------------------------------------
+instance (NatLE n MaxBoundInt64, Nat n) => Bounded (Fin n) where
+ minBound = Fin 0
+ maxBound = Fin (fromInteger (reflect (Proxy :: Proxy n) - 1))
+ {-# INLINE minBound #-}
+ {-# INLINE maxBound #-}
+
+
+-- | Return the 'minBound' of @Fin n@ as a plain integer. This is
+-- always zero, but is provided for symmetry with 'maxBoundOf'.
+minBoundOf :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> Int64
+minBoundOf _ = 0
+{-# INLINE minBoundOf #-}
+
+
+-- | Return the 'maxBound' of @Fin n@ as a plain integer. This is
+-- always @n-1@, but it's helpful because you may not know what
+-- @n@ is at the time.
+maxBoundOf :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> Int64
+maxBoundOf x = fromInteger (reflect (fin2proxy x) - 1)
+{-# INLINE maxBoundOf #-}
+
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Enum, since that would inject invalid numbers!
+-- N.B., we're using partial functions, because H98 requires it!
+instance (NatLE n MaxBoundInt64, Nat n) => Enum (Fin n) where
+ succ x =
+ case SE.succ x of
+ Just y -> y
+ Nothing -> _succ_maxBound "Fin.Int64" -- cf, @GHC.Word.succError@
+ {-# INLINE succ #-}
+
+ pred x =
+ case SE.pred x of
+ Just y -> y
+ Nothing -> _pred_minBound "Fin.Int64" -- cf, @GHC.Word.predError@
+ {-# INLINE pred #-}
+
+ toEnum i =
+ case SE.toEnum i of
+ Just y -> y
+ Nothing -> _toEnum_OOR "Fin.Int64" -- cf, @GHC.Word.toEnumError@
+ {-# INLINE toEnum #-}
+
+ fromEnum = fromIntegral . fromFin
+ {-# INLINE fromEnum #-}
+
+ -- Hopefully list fusion will get rid of the map, and preserve
+ -- the fusion tricks in GHC.Enum...
+ enumFrom x@(Fin i) = map Fin (enumFromTo i (maxBoundOf x))
+ enumFromThen x@(Fin i) (Fin j)
+ | j >= i = map Fin (enumFromThenTo i j (maxBoundOf x))
+ | otherwise = map Fin (enumFromThenTo i j (minBoundOf x))
+ enumFromTo (Fin i) (Fin k) = map Fin (enumFromTo i k)
+ enumFromThenTo (Fin i) (Fin j) (Fin k) = map Fin (enumFromThenTo i j k)
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromTo #-}
+ {-# INLINE enumFromThenTo #-}
+
+{-
+_pred_succ :: Nat n => Fin n -> Fin n
+_pred_succ x = if x == maxBound then _succ_maxBound "Fin.Int64" else x
+{-# INLINE _pred_succ #-}
+
+_succ_pred :: Nat n => Fin n -> Fin n
+_succ_pred x = if x == minBound then _pred_minBound "Fin.Int64" else x
+{-# INLINE _succ_pred #-}
+
+-- BUG: how can we introduce the (Nat n) constraint? Floating out the RHSs to give them signatures doesn't help.
+{-# RULES
+"pred (succ x) :: Fin n" forall x. pred (succ x) = _pred_succ x
+"pred . succ :: Fin n -> Fin n" pred . succ = _pred_succ
+
+"succ (pred x) :: Fin n" forall x. succ (pred x) = _succ_pred x
+"succ . pred :: Fin n -> Fin n" succ . pred = _succ_pred
+ #-}
+-}
+
+instance (NatLE n MaxBoundInt64, Nat n) => SE.UpwardEnum (Fin n) where
+ succ x@(Fin i)
+ | x < maxBound = Just $! Fin (i + 1)
+ | otherwise = Nothing
+ succeeds = (>)
+ enumFrom = enumFrom
+ enumFromTo = enumFromTo
+ {-# INLINE succ #-}
+ {-# INLINE succeeds #-}
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromTo #-}
+
+instance (NatLE n MaxBoundInt64, Nat n) => SE.DownwardEnum (Fin n) where
+ pred (Fin i)
+ | 0 < i = Just $! Fin (i - 1)
+ | otherwise = Nothing
+ precedes = (<)
+ enumDownFrom (Fin i) = map Fin (enumFromThenTo i (i-1) 0)
+ enumDownFromTo (Fin i) (Fin k) = map Fin (enumFromThenTo i (i-1) (max 0 k))
+ {-# INLINE pred #-}
+ {-# INLINE precedes #-}
+ {-# INLINE enumDownFrom #-}
+ {-# INLINE enumDownFromTo #-}
+
+instance (NatLE n MaxBoundInt64, Nat n) => SE.Enum (Fin n) where
+ toEnum i
+ | 0 <= j && j <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ j = fromIntegral i
+ x = Fin j :: Fin n
+ fromEnum x = Just $! (fromIntegral . fromFin) x
+ enumFromThen = enumFromThen
+ enumFromThenTo = enumFromThenTo
+ {-# INLINE toEnum #-}
+ {-# INLINE fromEnum #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromThenTo #-}
+
+
+-- TODO: can we trust the validity of the input arguments?
+instance (NatLE n MaxBoundInt64, Nat n) => Ix (Fin n) where
+ index (Fin i, Fin j) (Fin k) = index (i,j) k
+ range (Fin i, Fin j) = map Fin (range (i,j))
+ inRange (Fin i, Fin j) (Fin k) = inRange (i,j) k
+ rangeSize (Fin i, Fin j) = rangeSize (i,j)
+
+
+----------------------------------------------------------------
+-- TODO: define Num, Real, Integral? (N.B., Can't derive them safely.)
+
+
+----------------------------------------------------------------
+-- TODO: why was the checking stuff done using exceptions instead of Maybe?
+-- TODO: can we successfully ensure that invalid values can *never* be constructed?
+
+
+-- | A version of 'const' which checks that the second argument is
+-- in fact valid for its type before returning the first argument.
+-- Throws an exception if the @Fin n@ is invalid. The name and
+-- argument ordering are indended for infix use.
+checking :: (NatLE n MaxBoundInt64, Nat n) => a -> Fin n -> a
+checking a x
+ | minBound <= x && x <= maxBound = a
+ | otherwise = _checking_OOR x
+{-# INLINE checking #-}
+
+
+-- TODO: use extensible-exceptions instead of 'error'
+_checking_OOR :: (NatLE n MaxBoundInt64, Nat n) => Fin n -> a
+_checking_OOR x = error
+ . ("The value "++)
+ . shows x
+ . (" is out of bounds for "++)
+ . showsFinType x
+ $ ". This is a library error; contact the maintainer."
+
+
+-- | Extract the value of a @Fin n@.
+--
+-- /N.B.,/ if somehow the @Fin n@ value was constructed invalidly,
+-- then this function will throw an exception. However, this should
+-- /never/ 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
+fromFin x@(Fin i) = i `checking` x
+{-# INLINE fromFin #-}
+
+
+-- | Safely embed a number into @Fin n@. Use of this function will
+-- generally require an explicit type signature in order to know
+-- which @n@ to use.
+toFin :: (NatLE n MaxBoundInt64, Nat n) => Int64 -> Maybe (Fin n)
+toFin = toFin_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous?
+ toFin_ :: forall n. (NatLE n MaxBoundInt64, Nat n)
+ => Int64 -> Maybe (Fin n)
+ toFin_ i
+ | 0 <= i && i <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ x = Fin i :: Fin n
+ {-# INLINE toFin_ #-}
+{-# INLINE toFin #-}
+
+-- TODO: RULES for toFin.fromFin and fromFin.toFin
+
+
+-- | Safely embed a number into @Fin n@. This variant of 'toFin'
+-- uses a proxy to avoid the need for type signatures.
+toFinProxy :: (NatLE n MaxBoundInt64, Nat n)
+ => Proxy n -> Int64 -> Maybe (Fin n)
+toFinProxy _ = toFin
+{-# INLINE toFinProxy #-}
+
+
+-- | Safely embed integers into @Fin n@, where @n@ is the first
+-- argument. We use rank-2 polymorphism to render the type-level
+-- @n@ existentially quantified, thereby hiding the dependent type
+-- from the compiler. However, @n@ will in fact be a skolem, so we
+-- can't provide the continuation with proof that @Nat n@ ---
+-- unfortunately, rendering this function of little use.
+--
+-- > toFinCPS n k i
+-- > | 0 <= i && i < n = Just (k i) -- morally speaking...
+-- > | otherwise = Nothing
+--
+toFinCPS :: Int64 -> (forall n. Reifies n Integer => Fin n -> r) -> Int64 -> Maybe r
+toFinCPS n k i
+ | 0 <= i && i < n = Just (reify (toInteger n) $ \(_ :: Proxy n) -> k (Fin i :: Fin n))
+ | otherwise = Nothing
+{-# INLINE toFinCPS #-}
+-- BUG: can't use @Nat n@ because: Could not deduce (Nat_ n) from the context (Reifies n Integer)
+-- TODO: how can we get Data.Number.Fin.TyDecimal.reifyNat to work?
+
+
+----------------------------------------------------------------
+instance (NatLE n MaxBoundInt64, Nat n) => QC.Arbitrary (Fin n) where
+ shrink = tail . SE.enumDownFrom
+ arbitrary
+ | x >= 0 = (Fin . fromInteger) `liftM` QC.choose (0,x)
+ | otherwise =
+ -- BUG: there's no way to say it's impossible...
+ error . ("Arbitrary.arbitrary{"++)
+ . showsFinType (__ :: Fin n)
+ $ "}: this type is empty"
+ -- TODO: use extensible-exceptions instead of 'error'
+ where
+ -- BUG: no instance Random Int64
+ x = toInteger (maxBoundOf (__ :: Fin n))
+
+
+
+instance (NatLE n MaxBoundInt64, Nat n) => QC.CoArbitrary (Fin n) where
+ coarbitrary (Fin n) = QC.variant n
+
+
+instance (NatLE n MaxBoundInt64, Nat n) => SC.Serial (Fin n) where
+ series d
+ | d < 0 = [] -- paranoia.
+ | otherwise =
+ case toFin (fromIntegral d) of
+ Nothing -> enumFromTo minBound maxBound
+ Just n -> enumFromTo minBound n
+
+ coseries rs d =
+ [ \(Fin i) ->
+ if i > 0
+ then let j = Fin (i-1) :: Fin n
+ in f j `checking` j -- more paranoia; in case n==0 or i>n
+ else z
+ | z <- SC.alts0 rs d
+ , f <- SC.alts1 rs d
+ ]
+
+instance (NatLE n MaxBoundInt64, Nat n) => LSC.Serial (Fin n) where
+ series = LSC.drawnFrom . SC.series
+
+
+----------------------------------------------------------------
+-- TODO: do we care about <http://ncatlab.org/nlab/show/decalage>?
+
+
+-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe?
+{- -- Agda's version:
+data MaxView {n : Nat} : Fin (suc n) -> Set where
+ theMax : MaxView (fromNat n)
+ notMax : (i : Fin n) -> MaxView (weaken i)
+
+maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i
+maxView {zero} zero = theMax
+maxView {zero} (suc ())
+maxView {suc n} zero = notMax zero
+maxView {suc n} (suc i) with maxView i
+maxView {suc n} (suc .(fromNat n)) | theMax = theMax
+maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i)
+-}
+-- | The maximum-element view. This strengthens the type by removing
+-- the maximum element:
+--
+-- > maxView maxBound = Nothing
+-- > maxView x = Just x -- morally speaking...
+--
+-- The opposite of this function is 'weaken'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+maxView
+ :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, Succ m n)
+ => Fin n -> Maybe (Fin m)
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n); so can't use maxViewLE as the implementation.
+-- BUG: Could not deduce (NatLE m MaxBoundInt64) from the context (NatLE n MaxBoundInt64, Succ m n); so we have to add it.
+maxView = maxView_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@...
+ maxView_ :: forall m n. (NatLE m MaxBoundInt64) => Fin n -> Maybe (Fin m)
+ maxView_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxView_ #-}
+{-# INLINE maxView #-}
+
+
+-- | A variant of 'maxView' which allows strengthening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @m@ to use.
+--
+-- The opposite of this function is 'weakenLE'. When the choice of
+-- @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+maxViewLE
+ :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE m n)
+ => Fin n -> Maybe (Fin m)
+-- BUG: Could not deduce (NatLE m MaxBoundInt64) from the context (NatLE n MaxBoundInt64, Succ m n); so we have to add it.
+maxViewLE = maxViewLE_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ maxViewLE_ :: forall m n. (NatLE m MaxBoundInt64) => Fin n -> Maybe (Fin m)
+ maxViewLE_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxViewLE_ #-}
+{-# INLINE maxViewLE #-}
+
+
+-- TODO: maxViewPlus?
+
+
+-- This type-restricted version is a~la Agda.
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'minBound'. That is,
+--
+-- > fromFin (weaken x) == fromFin x
+--
+-- The opposite of this function is 'maxView'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+weaken :: (NatLE n MaxBoundInt64, Succ m n) => Fin m -> Fin n
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n)
+weaken (Fin i) = Fin i
+{-# INLINE weaken #-}
+
+
+-- | A variant of 'weaken' which allows weakening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @n@ to use.
+--
+-- The opposite of this function is 'maxViewLE'. When the choice
+-- of @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+weakenLE :: (NatLE n MaxBoundInt64, NatLE m n) => Fin m -> Fin n
+weakenLE (Fin i) = Fin i
+{-# INLINE weakenLE #-}
+
+
+----------------------------------------------------------------
+-- | The predecessor view. This strengthens the type by shifting
+-- everything down by one:
+--
+-- > predView 0 = Nothing
+-- > predView x = Just (x-1) -- morally speaking...
+--
+-- The opposite of this function is 'widen'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+predView :: (NatLE n MaxBoundInt64, Succ m n) => Fin n -> Maybe (Fin m)
+predView (Fin i)
+ | i <= 0 = Nothing
+ | otherwise = Just $! Fin (i-1)
+{-# INLINE predView #-}
+
+
+-- TODO: predViewLE? predViewPlus?
+
+
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'maxBound'. That is, we shift everything
+-- up by one:
+--
+-- > fromFin (widen x) == 1 + fromFin x
+--
+-- The opposite of this function is 'predView'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+widen :: (NatLE n MaxBoundInt64, Succ m n) => Fin m -> Fin n
+widen (Fin i) = Fin (i+1)
+{-# INLINE widen #-}
+
+
+-- | Embed a finite domain into any larger one, keeping the same
+-- position relative to 'maxBound'. That is,
+--
+-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
+-- > where y = widenLE x
+--
+-- Use of this function will generally require an explicit type
+-- signature in order to know which @n@ to use.
+widenLE
+ :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE m n)
+ => Fin m -> Fin n
+-- BUG: Could not deduce (NatLE m MaxBoundInt64) from the context (NatLE n MaxBoundInt64, NatLE m n); so we have to add it.
+widenLE x@(Fin i) = y
+ where
+ y = Fin (maxBoundOf y - maxBoundOf x + i)
+{-# INLINE widenLE #-}
+
+
+----------------------------------------------------------------
+-- BUG: Could not deduce (NatLE m o) from the context (Add m n o)
+-- | A type-signature variant of 'weakenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE m o@. This is the
+-- left half of 'plus'.
+weakenPlus :: (NatLE o MaxBoundInt64, Add m n o) => Fin m -> Fin o
+weakenPlus (Fin i) = Fin i
+{-# INLINE weakenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE n o) from the context (Add m n o)
+-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it.
+-- | A type-signature variant of 'widenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE n o@. This is the
+-- right half of 'plus'.
+widenPlus
+ :: ( NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64
+ , Add m n o)
+ => Fin n -> Fin o
+widenPlus = widenPlus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ widenPlus_ :: forall m n o
+ . (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, Add m n o)
+ => Fin n -> Fin o
+ widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y)
+ {-# INLINE widenPlus_ #-}
+{-# INLINE widenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it.
+-- | The ordinal-sum functor, on objects. This internalizes the
+-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ 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
+plus = either weakenPlus widenPlus
+{-# INLINE plus #-}
+
+
+-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it.
+-- | The inverse of 'plus'.
+unplus
+ :: ( NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64
+ , Add m n o)
+ => Fin o -> Either (Fin m) (Fin n)
+unplus = unplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ unplus_ :: forall m n o. (NatLE m MaxBoundInt64)
+ => Fin o -> Either (Fin m) (Fin n)
+ unplus_ (Fin i)
+ | i <= x = Left $! Fin i
+ | otherwise = Right $! Fin (i-x)
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE unplus_ #-}
+{-# INLINE unplus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- BUG: Ditto for (Add m' n' o')
+-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it.
+-- | 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
+-- @(+++)@ from "Control.Arrow".
+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') -- ^ The left morphism
+ -> (Fin n -> Fin n') -- ^ The right morphism
+ -> (Fin o -> Fin o') -- ^
+fplus = fplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ fplus_ :: forall m n o m' n' o'
+ . ( 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'
+ fplus_ f g (Fin i)
+ | i <= x = weakenPlus (f $! Fin i)
+ | otherwise = widenPlus (g $! Fin (i-x))
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE fplus_ #-}
+{-# INLINE fplus #-}
+
+
+-- TODO: (Fin m, Fin n) <-> Fin (Times m n)
+
+----------------------------------------------------------------
+{- -- Agda's version:
+thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n)
+thin zero j = suc j
+thin (suc i) zero = zero
+thin (suc i) (suc j) = suc (thin i j)
+-}
+-- | The \"face maps\" for @Fin@ viewed as the standard simplices
+-- (aka: the thinning view). Traditionally spelled with delta or
+-- epsilon. For each @i@, it is the unique injective monotonic map
+-- that skips @i@. That is,
+--
+-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thin i j /= i
+--
+thin :: (NatLE n MaxBoundInt64, Succ m n) => Fin n -> Fin m -> Fin n
+thin i j
+ | weaken j < i = weaken j
+ | otherwise = succ (weaken j)
+{-# INLINE thin #-}
+
+
+-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it.
+-- | The \"degeneracy maps\" for @Fin@ viewed as the standard
+-- simplices. Traditionally spelled with sigma or eta. For each
+-- @i@, it is the unique surjective monotonic map that covers @i@
+-- twice. That is,
+--
+-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thick i (i+1) == i
+--
+thick
+ :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, Succ m n)
+ => Fin m -> Fin n -> Fin m
+thick i j =
+ case maxView (if j <= weaken i then j else pred j) of
+ Just j' -> j'
+ Nothing -> _thick_impossible
+{-# INLINE thick #-}
+
+
+
+{-
+-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne?
+-- The non zero view, which is used for defining compare...
+data NonEmptyView : {n : Nat} -> Fin n -> Set where
+ ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i
+
+nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i
+nonEmpty zero = ne
+nonEmpty (suc _) = ne
+
+
+data EqView : {n : Nat} -> Fin n -> Fin n -> Set where
+ equal : {n : Nat}{i : Fin n} -> EqView i i
+ notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j)
+
+compare : {n : Nat}(i j : Fin n) -> EqView i j
+compare zero zero = equal
+compare zero (suc j) = notequal j
+compare (suc i) zero with nonEmpty i
+... | ne = notequal zero
+compare (suc i) (suc j) with compare i j
+compare (suc i) (suc .i) | equal = equal
+compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j)
+-}
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- Error messages
+
+__ :: a
+__ = error "Data.Number.Fin.Int64: attempted to evaluate type token"
+{-# NOINLINE __ #-}
+-- TODO: use extensible-exceptions instead of 'error'
+-- TODO: use Proxy instead of these undefined values...
+
+_thick_impossible :: a
+_thick_impossible =
+ error "Data.Number.Fin.Int64.thick: the impossible happened"
+{-# NOINLINE _thick_impossible #-}
+-- TODO: use extensible-exceptions instead of 'error'
+
+_succ_maxBound :: String -> a
+_succ_maxBound ty =
+ error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound"
+{-# NOINLINE _succ_maxBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_pred_minBound :: String -> a
+_pred_minBound ty =
+ error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound"
+{-# NOINLINE _pred_minBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_toEnum_OOR :: String -> a
+_toEnum_OOR ty =
+ error $ "Enum.toEnum{"++ty++"}: argument out of range"
+{-# NOINLINE _toEnum_OOR #-}
+-- TODO: is there an extensible-exception for this?
+
+----------------------------------------------------------------
+----------------------------------------------------------- fin.
diff --git a/src/Data/Number/Fin/Int8.hs b/src/Data/Number/Fin/Int8.hs
new file mode 100644
index 0000000..aa5c856
--- /dev/null
+++ b/src/Data/Number/Fin/Int8.hs
@@ -0,0 +1,865 @@
+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+{-# LANGUAGE ScopedTypeVariables
+ , DeriveDataTypeable
+ , MultiParamTypeClasses
+ , FlexibleContexts
+ , CPP
+ , Rank2Types
+ , UndecidableInstances
+ #-}
+
+#if __GLASGOW_HASKELL__ >= 701
+-- N.B., Data.Proxy and Test.QuickCheck aren't "safe".
+{-# LANGUAGE Trustworthy #-}
+#endif
+----------------------------------------------------------------
+-- 2013.05.29
+-- |
+-- Module : Data.Number.Fin.Int8
+-- Copyright : 2012--2013 wren ng thornton
+-- License : BSD3
+-- Maintainer : wren@community.haskell.org
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- A newtype of 'Int8' for finite subsets of the natural numbers.
+----------------------------------------------------------------
+module Data.Number.Fin.Int8
+ (
+ -- * @Fin@, finite sets of natural numbers
+ Fin()
+
+ -- ** Showing types
+ , showFinType
+ , showsFinType
+
+ -- ** Convenience functions
+ , minBoundOf
+ , maxBoundOf
+
+ -- ** Introduction and elimination
+ , toFin
+ , toFinProxy
+ , toFinCPS
+ , fromFin
+
+ -- ** Views and coersions
+ -- *** Weakening and maximum views
+ , weaken
+ , weakenLE
+ , weakenPlus
+ , maxView
+ , maxViewLE
+
+ -- *** Widening and the predecessor view
+ , widen
+ , widenLE
+ , widenPlus
+ , predView
+
+ -- *** The ordinal-sum functor
+ , plus
+ , unplus
+ , fplus
+
+ -- *** Face- and degeneracy-maps
+ , thin
+ , thick
+ -- TODO: is there any way to get equality to work right?
+ ) where
+
+import qualified Prelude.SafeEnum as SE
+import Data.Int (Int8)
+import Data.Ix
+import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE, MaxBoundInt8)
+import Data.Typeable (Typeable)
+import Data.Proxy (Proxy(Proxy))
+import Data.Reflection (Reifies(reflect), reify)
+import Control.Monad (liftM)
+
+import qualified Test.QuickCheck as QC
+#if (MIN_VERSION_smallcheck(0,6,0))
+import qualified Test.SmallCheck.Series as SC
+#else
+import qualified Test.SmallCheck as SC
+#endif
+import qualified Test.LazySmallCheck as LSC
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- | A finite set of integers @Fin n = { i :: Int8 | 0 <= i < n }@
+-- with the usual ordering. This is typed as if using the standard
+-- GADT presentation of @Fin n@, however it is actually implemented
+-- by a plain 'Int8'.
+newtype Fin n = Fin Int8
+ deriving Typeable
+ -- WART: to give additional constraints (e.g., Nat n) on derived
+ -- instances (e.g., Show, Eq, Ord), we need to specify the
+ -- constraints on the data type declaration; however, giving of
+ -- data-type constraints is deprecated and will be removed from
+ -- the language...
+
+{-
+-- Some fusion rules for treating newtypes like 'id', or as close
+-- as we can. We only have these fire in the last stage so that
+-- they don't inhibit the usual list-fusion rules. Hopefully there's
+-- nothing important which is defined to not fire at [0].
+--
+-- TODO: add other laws regarding 'id'
+{-# RULES
+"map Fin" [0] map Fin = unsafeCoerce
+"fmap Fin" [0] fmap Fin = unsafeCoerce
+"liftM Fin" [0] liftM Fin = unsafeCoerce
+"liftA Fin" [0] liftA Fin = unsafeCoerce
+ #-}
+-}
+
+{- TODO:
+-- also: <http://paczesiowa.blogspot.com/2010/01/pure-extensible-exceptions-and-self.html>
+
+-- | An error for attempts to evaluate an undefined value which is
+-- passed around as a type token. The string should give the source
+-- where the token was generated, or some other helpful information
+-- for tracking the problem down.
+data EvaluatedTypeTokenException = EvaluatedTypeTokenException String
+ deriving (Typeable, Show)
+
+instance Exception EvaluatedTypeTokenException
+
+-- | Construct a type token with the given message.
+__ :: String -> a
+__ here = throw (EvaluatedTypeTokenException here)
+
+
+-- TODO: use Control.Exception.assert instead?
+data FinException = FinOOB (Fin n)
+ deriving (Typeable)
+
+instance Show FinException where
+ show (FinOOB x) =
+ "Value "++show x++" out of bounds for "++showFinType x
+
+instance Exception FinException
+-}
+
+
+-- | Often, we don't want to use the @Fin n@ as a proxy, since that
+-- would introduce spurious data dependencies. This function ignores
+-- its argument (other than for type propagation) so, hopefully,
+-- via massive inlining this function will avoid that spurious
+-- dependency. Hopefully...
+--
+-- Also, this lets us minimize the use of @-XScopedTypeVariables@
+-- which makes the Haddocks ugly. And so it lets us avoid the hacks
+-- to hide our use of @-XScopedTypeVariables@.
+--
+-- TODO: is this enough to ensure reflection is/can-be done at compile-time?
+-- TODO: is there any way to tell GHC that this function should /never/ appear in the output of compilation?
+fin2proxy :: (NatLE n MaxBoundInt8, Nat n) => fin n -> Proxy n
+fin2proxy _ = Proxy
+{-# INLINE fin2proxy #-}
+
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt8, Nat n) => Show (Fin n) where
+ showsPrec d (Fin i) =
+ showParen (d > 10) $ ("Fin "++) . shows i
+
+
+-- | Like 'show', except it shows the type itself instead of the
+-- value.
+showFinType :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> String
+showFinType x = showsFinType x []
+{-# INLINE showFinType #-}
+-- Should never fire, due to inlining
+{- RULES
+"showFinType/++" forall x s. showFinType x ++ s = showsFinType x s
+ -}
+
+
+-- | Like 'shows', except it shows the type itself instead of the
+-- value.
+showsFinType :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> ShowS
+showsFinType x = ("Fin "++) . shows (reflect (fin2proxy x))
+{-# INLINE [0] showsFinType #-}
+-- TODO: Is [0] the best level to start inlining showsFinType?
+{-# RULES
+"showsFinType/++" forall x s1 s2.
+ showsFinType x s1 ++ s2 = showsFinType x (s1 ++ s2)
+ #-}
+
+-- TODO: showsPrecFinType?
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Read, since that would inject invalid numbers!
+instance (NatLE n MaxBoundInt8, Nat n) => Read (Fin n) where
+ readsPrec d =
+ readParen (d > 10) $ \s0 -> do
+ ("Fin", s1) <- lex s0
+ (i, s2) <- readsPrec 11 s1
+ maybe [] (\n -> [(n,s2)]) (toFin i)
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt8, Nat n) => Eq (Fin n) where
+ Fin i == Fin j = i == j
+ Fin i /= Fin j = i /= j
+ {-# INLINE (==) #-}
+ {-# INLINE (/=) #-}
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance (NatLE n MaxBoundInt8, Nat n) => Ord (Fin n) where
+ Fin i < Fin j = i < j
+ Fin i <= Fin j = i <= j
+ Fin i > Fin j = i > j
+ Fin i >= Fin j = i >= j
+ compare (Fin i) (Fin j) = compare i j
+ min (Fin i) (Fin j) = Fin (min i j)
+ max (Fin i) (Fin j) = Fin (max i j)
+ {-# INLINE (<) #-}
+ {-# INLINE (<=) #-}
+ {-# INLINE (>) #-}
+ {-# INLINE (>=) #-}
+ {-# INLINE compare #-}
+ {-# INLINE min #-}
+ {-# INLINE max #-}
+
+----------------------------------------------------------------
+instance (NatLE n MaxBoundInt8, Nat n) => Bounded (Fin n) where
+ minBound = Fin 0
+ maxBound = Fin (fromInteger (reflect (Proxy :: Proxy n) - 1))
+ {-# INLINE minBound #-}
+ {-# INLINE maxBound #-}
+
+
+-- | Return the 'minBound' of @Fin n@ as a plain integer. This is
+-- always zero, but is provided for symmetry with 'maxBoundOf'.
+minBoundOf :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> Int8
+minBoundOf _ = 0
+{-# INLINE minBoundOf #-}
+
+
+-- | Return the 'maxBound' of @Fin n@ as a plain integer. This is
+-- always @n-1@, but it's helpful because you may not know what
+-- @n@ is at the time.
+maxBoundOf :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> Int8
+maxBoundOf x = fromInteger (reflect (fin2proxy x) - 1)
+{-# INLINE maxBoundOf #-}
+
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Enum, since that would inject invalid numbers!
+-- N.B., we're using partial functions, because H98 requires it!
+instance (NatLE n MaxBoundInt8, Nat n) => Enum (Fin n) where
+ succ x =
+ case SE.succ x of
+ Just y -> y
+ Nothing -> _succ_maxBound "Fin.Int8" -- cf, @GHC.Word.succError@
+ {-# INLINE succ #-}
+
+ pred x =
+ case SE.pred x of
+ Just y -> y
+ Nothing -> _pred_minBound "Fin.Int8" -- cf, @GHC.Word.predError@
+ {-# INLINE pred #-}
+
+ toEnum i =
+ case SE.toEnum i of
+ Just y -> y
+ Nothing -> _toEnum_OOR "Fin.Int8" -- cf, @GHC.Word.toEnumError@
+ {-# INLINE toEnum #-}
+
+ fromEnum = fromIntegral . fromFin
+ {-# INLINE fromEnum #-}
+
+ -- Hopefully list fusion will get rid of the map, and preserve
+ -- the fusion tricks in GHC.Enum...
+ enumFrom x@(Fin i) = map Fin (enumFromTo i (maxBoundOf x))
+ enumFromThen x@(Fin i) (Fin j)
+ | j >= i = map Fin (enumFromThenTo i j (maxBoundOf x))
+ | otherwise = map Fin (enumFromThenTo i j (minBoundOf x))
+ enumFromTo (Fin i) (Fin k) = map Fin (enumFromTo i k)
+ enumFromThenTo (Fin i) (Fin j) (Fin k) = map Fin (enumFromThenTo i j k)
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromTo #-}
+ {-# INLINE enumFromThenTo #-}
+
+{-
+_pred_succ :: Nat n => Fin n -> Fin n
+_pred_succ x = if x == maxBound then _succ_maxBound "Fin.Int8" else x
+{-# INLINE _pred_succ #-}
+
+_succ_pred :: Nat n => Fin n -> Fin n
+_succ_pred x = if x == minBound then _pred_minBound "Fin.Int8" else x
+{-# INLINE _succ_pred #-}
+
+-- BUG: how can we introduce the (Nat n) constraint? Floating out the RHSs to give them signatures doesn't help.
+{-# RULES
+"pred (succ x) :: Fin n" forall x. pred (succ x) = _pred_succ x
+"pred . succ :: Fin n -> Fin n" pred . succ = _pred_succ
+
+"succ (pred x) :: Fin n" forall x. succ (pred x) = _succ_pred x
+"succ . pred :: Fin n -> Fin n" succ . pred = _succ_pred
+ #-}
+-}
+
+instance (NatLE n MaxBoundInt8, Nat n) => SE.UpwardEnum (Fin n) where
+ succ x@(Fin i)
+ | x < maxBound = Just $! Fin (i + 1)
+ | otherwise = Nothing
+ succeeds = (>)
+ enumFrom = enumFrom
+ enumFromTo = enumFromTo
+ {-# INLINE succ #-}
+ {-# INLINE succeeds #-}
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromTo #-}
+
+instance (NatLE n MaxBoundInt8, Nat n) => SE.DownwardEnum (Fin n) where
+ pred (Fin i)
+ | 0 < i = Just $! Fin (i - 1)
+ | otherwise = Nothing
+ precedes = (<)
+ enumDownFrom (Fin i) = map Fin (enumFromThenTo i (i-1) 0)
+ enumDownFromTo (Fin i) (Fin k) = map Fin (enumFromThenTo i (i-1) (max 0 k))
+ {-# INLINE pred #-}
+ {-# INLINE precedes #-}
+ {-# INLINE enumDownFrom #-}
+ {-# INLINE enumDownFromTo #-}
+
+instance (NatLE n MaxBoundInt8, Nat n) => SE.Enum (Fin n) where
+ toEnum i
+ | 0 <= j && j <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ j = fromIntegral i
+ x = Fin j :: Fin n
+ fromEnum x = Just $! (fromIntegral . fromFin) x
+ enumFromThen = enumFromThen
+ enumFromThenTo = enumFromThenTo
+ {-# INLINE toEnum #-}
+ {-# INLINE fromEnum #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromThenTo #-}
+
+
+-- TODO: can we trust the validity of the input arguments?
+instance (NatLE n MaxBoundInt8, Nat n) => Ix (Fin n) where
+ index (Fin i, Fin j) (Fin k) = index (i,j) k
+ range (Fin i, Fin j) = map Fin (range (i,j))
+ inRange (Fin i, Fin j) (Fin k) = inRange (i,j) k
+ rangeSize (Fin i, Fin j) = rangeSize (i,j)
+
+
+----------------------------------------------------------------
+-- TODO: define Num, Real, Integral? (N.B., Can't derive them safely.)
+
+
+----------------------------------------------------------------
+-- TODO: why was the checking stuff done using exceptions instead of Maybe?
+-- TODO: can we successfully ensure that invalid values can *never* be constructed?
+
+
+-- | A version of 'const' which checks that the second argument is
+-- in fact valid for its type before returning the first argument.
+-- Throws an exception if the @Fin n@ is invalid. The name and
+-- argument ordering are indended for infix use.
+checking :: (NatLE n MaxBoundInt8, Nat n) => a -> Fin n -> a
+checking a x
+ | minBound <= x && x <= maxBound = a
+ | otherwise = _checking_OOR x
+{-# INLINE checking #-}
+
+
+-- TODO: use extensible-exceptions instead of 'error'
+_checking_OOR :: (NatLE n MaxBoundInt8, Nat n) => Fin n -> a
+_checking_OOR x = error
+ . ("The value "++)
+ . shows x
+ . (" is out of bounds for "++)
+ . showsFinType x
+ $ ". This is a library error; contact the maintainer."
+
+
+-- | Extract the value of a @Fin n@.
+--
+-- /N.B.,/ if somehow the @Fin n@ value was constructed invalidly,
+-- then this function will throw an exception. However, this should
+-- /never/ 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
+fromFin x@(Fin i) = i `checking` x
+{-# INLINE fromFin #-}
+
+
+-- | Safely embed a number into @Fin n@. Use of this function will
+-- generally require an explicit type signature in order to know
+-- which @n@ to use.
+toFin :: (NatLE n MaxBoundInt8, Nat n) => Int8 -> Maybe (Fin n)
+toFin = toFin_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous?
+ toFin_ :: forall n. (NatLE n MaxBoundInt8, Nat n)
+ => Int8 -> Maybe (Fin n)
+ toFin_ i
+ | 0 <= i && i <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ x = Fin i :: Fin n
+ {-# INLINE toFin_ #-}
+{-# INLINE toFin #-}
+
+-- TODO: RULES for toFin.fromFin and fromFin.toFin
+
+
+-- | Safely embed a number into @Fin n@. This variant of 'toFin'
+-- uses a proxy to avoid the need for type signatures.
+toFinProxy :: (NatLE n MaxBoundInt8, Nat n)
+ => Proxy n -> Int8 -> Maybe (Fin n)
+toFinProxy _ = toFin
+{-# INLINE toFinProxy #-}
+
+
+-- | Safely embed integers into @Fin n@, where @n@ is the first
+-- argument. We use rank-2 polymorphism to render the type-level
+-- @n@ existentially quantified, thereby hiding the dependent type
+-- from the compiler. However, @n@ will in fact be a skolem, so we
+-- can't provide the continuation with proof that @Nat n@ ---
+-- unfortunately, rendering this function of little use.
+--
+-- > toFinCPS n k i
+-- > | 0 <= i && i < n = Just (k i) -- morally speaking...
+-- > | otherwise = Nothing
+--
+toFinCPS :: Int8 -> (forall n. Reifies n Integer => Fin n -> r) -> Int8 -> Maybe r
+toFinCPS n k i
+ | 0 <= i && i < n = Just (reify (toInteger n) $ \(_ :: Proxy n) -> k (Fin i :: Fin n))
+ | otherwise = Nothing
+{-# INLINE toFinCPS #-}
+-- BUG: can't use @Nat n@ because: Could not deduce (Nat_ n) from the context (Reifies n Integer)
+-- TODO: how can we get Data.Number.Fin.TyDecimal.reifyNat to work?
+
+
+----------------------------------------------------------------
+instance (NatLE n MaxBoundInt8, Nat n) => QC.Arbitrary (Fin n) where
+ shrink = tail . SE.enumDownFrom
+ arbitrary
+ | x >= 0 = (Fin . fromInteger) `liftM` QC.choose (0,x)
+ | otherwise =
+ -- BUG: there's no way to say it's impossible...
+ error . ("Arbitrary.arbitrary{"++)
+ . showsFinType (__ :: Fin n)
+ $ "}: this type is empty"
+ -- TODO: use extensible-exceptions instead of 'error'
+ where
+ -- BUG: no instance Random Int8
+ x = toInteger (maxBoundOf (__ :: Fin n))
+
+
+
+instance (NatLE n MaxBoundInt8, Nat n) => QC.CoArbitrary (Fin n) where
+ coarbitrary (Fin n) = QC.variant n
+
+
+instance (NatLE n MaxBoundInt8, Nat n) => SC.Serial (Fin n) where
+ series d
+ | d < 0 = [] -- paranoia.
+ | otherwise =
+ case toFin (fromIntegral d) of
+ Nothing -> enumFromTo minBound maxBound
+ Just n -> enumFromTo minBound n
+
+ coseries rs d =
+ [ \(Fin i) ->
+ if i > 0
+ then let j = Fin (i-1) :: Fin n
+ in f j `checking` j -- more paranoia; in case n==0 or i>n
+ else z
+ | z <- SC.alts0 rs d
+ , f <- SC.alts1 rs d
+ ]
+
+instance (NatLE n MaxBoundInt8, Nat n) => LSC.Serial (Fin n) where
+ series = LSC.drawnFrom . SC.series
+
+
+----------------------------------------------------------------
+-- TODO: do we care about <http://ncatlab.org/nlab/show/decalage>?
+
+
+-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe?
+{- -- Agda's version:
+data MaxView {n : Nat} : Fin (suc n) -> Set where
+ theMax : MaxView (fromNat n)
+ notMax : (i : Fin n) -> MaxView (weaken i)
+
+maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i
+maxView {zero} zero = theMax
+maxView {zero} (suc ())
+maxView {suc n} zero = notMax zero
+maxView {suc n} (suc i) with maxView i
+maxView {suc n} (suc .(fromNat n)) | theMax = theMax
+maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i)
+-}
+-- | The maximum-element view. This strengthens the type by removing
+-- the maximum element:
+--
+-- > maxView maxBound = Nothing
+-- > maxView x = Just x -- morally speaking...
+--
+-- The opposite of this function is 'weaken'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+maxView
+ :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, Succ m n)
+ => Fin n -> Maybe (Fin m)
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n); so can't use maxViewLE as the implementation.
+-- BUG: Could not deduce (NatLE m MaxBoundInt8) from the context (NatLE n MaxBoundInt8, Succ m n); so we have to add it.
+maxView = maxView_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@...
+ maxView_ :: forall m n. (NatLE m MaxBoundInt8) => Fin n -> Maybe (Fin m)
+ maxView_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxView_ #-}
+{-# INLINE maxView #-}
+
+
+-- | A variant of 'maxView' which allows strengthening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @m@ to use.
+--
+-- The opposite of this function is 'weakenLE'. When the choice of
+-- @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+maxViewLE
+ :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE m n)
+ => Fin n -> Maybe (Fin m)
+-- BUG: Could not deduce (NatLE m MaxBoundInt8) from the context (NatLE n MaxBoundInt8, Succ m n); so we have to add it.
+maxViewLE = maxViewLE_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ maxViewLE_ :: forall m n. (NatLE m MaxBoundInt8) => Fin n -> Maybe (Fin m)
+ maxViewLE_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxViewLE_ #-}
+{-# INLINE maxViewLE #-}
+
+
+-- TODO: maxViewPlus?
+
+
+-- This type-restricted version is a~la Agda.
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'minBound'. That is,
+--
+-- > fromFin (weaken x) == fromFin x
+--
+-- The opposite of this function is 'maxView'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+weaken :: (NatLE n MaxBoundInt8, Succ m n) => Fin m -> Fin n
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n)
+weaken (Fin i) = Fin i
+{-# INLINE weaken #-}
+
+
+-- | A variant of 'weaken' which allows weakening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @n@ to use.
+--
+-- The opposite of this function is 'maxViewLE'. When the choice
+-- of @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+weakenLE :: (NatLE n MaxBoundInt8, NatLE m n) => Fin m -> Fin n
+weakenLE (Fin i) = Fin i
+{-# INLINE weakenLE #-}
+
+
+----------------------------------------------------------------
+-- | The predecessor view. This strengthens the type by shifting
+-- everything down by one:
+--
+-- > predView 0 = Nothing
+-- > predView x = Just (x-1) -- morally speaking...
+--
+-- The opposite of this function is 'widen'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+predView :: (NatLE n MaxBoundInt8, Succ m n) => Fin n -> Maybe (Fin m)
+predView (Fin i)
+ | i <= 0 = Nothing
+ | otherwise = Just $! Fin (i-1)
+{-# INLINE predView #-}
+
+
+-- TODO: predViewLE? predViewPlus?
+
+
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'maxBound'. That is, we shift everything
+-- up by one:
+--
+-- > fromFin (widen x) == 1 + fromFin x
+--
+-- The opposite of this function is 'predView'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+widen :: (NatLE n MaxBoundInt8, Succ m n) => Fin m -> Fin n
+widen (Fin i) = Fin (i+1)
+{-# INLINE widen #-}
+
+
+-- | Embed a finite domain into any larger one, keeping the same
+-- position relative to 'maxBound'. That is,
+--
+-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
+-- > where y = widenLE x
+--
+-- Use of this function will generally require an explicit type
+-- signature in order to know which @n@ to use.
+widenLE
+ :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE m n)
+ => Fin m -> Fin n
+-- BUG: Could not deduce (NatLE m MaxBoundInt8) from the context (NatLE n MaxBoundInt8, NatLE m n); so we have to add it.
+widenLE x@(Fin i) = y
+ where
+ y = Fin (maxBoundOf y - maxBoundOf x + i)
+{-# INLINE widenLE #-}
+
+
+----------------------------------------------------------------
+-- BUG: Could not deduce (NatLE m o) from the context (Add m n o)
+-- | A type-signature variant of 'weakenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE m o@. This is the
+-- left half of 'plus'.
+weakenPlus :: (NatLE o MaxBoundInt8, Add m n o) => Fin m -> Fin o
+weakenPlus (Fin i) = Fin i
+{-# INLINE weakenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE n o) from the context (Add m n o)
+-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it.
+-- | A type-signature variant of 'widenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE n o@. This is the
+-- right half of 'plus'.
+widenPlus
+ :: ( NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8
+ , Add m n o)
+ => Fin n -> Fin o
+widenPlus = widenPlus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ widenPlus_ :: forall m n o
+ . (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, Add m n o)
+ => Fin n -> Fin o
+ widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y)
+ {-# INLINE widenPlus_ #-}
+{-# INLINE widenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it.
+-- | The ordinal-sum functor, on objects. This internalizes the
+-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ 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
+plus = either weakenPlus widenPlus
+{-# INLINE plus #-}
+
+
+-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it.
+-- | The inverse of 'plus'.
+unplus
+ :: ( NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8
+ , Add m n o)
+ => Fin o -> Either (Fin m) (Fin n)
+unplus = unplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ unplus_ :: forall m n o. (NatLE m MaxBoundInt8)
+ => Fin o -> Either (Fin m) (Fin n)
+ unplus_ (Fin i)
+ | i <= x = Left $! Fin i
+ | otherwise = Right $! Fin (i-x)
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE unplus_ #-}
+{-# INLINE unplus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- BUG: Ditto for (Add m' n' o')
+-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it.
+-- | 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
+-- @(+++)@ from "Control.Arrow".
+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') -- ^ The left morphism
+ -> (Fin n -> Fin n') -- ^ The right morphism
+ -> (Fin o -> Fin o') -- ^
+fplus = fplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ fplus_ :: forall m n o m' n' o'
+ . ( 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'
+ fplus_ f g (Fin i)
+ | i <= x = weakenPlus (f $! Fin i)
+ | otherwise = widenPlus (g $! Fin (i-x))
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE fplus_ #-}
+{-# INLINE fplus #-}
+
+
+-- TODO: (Fin m, Fin n) <-> Fin (Times m n)
+
+----------------------------------------------------------------
+{- -- Agda's version:
+thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n)
+thin zero j = suc j
+thin (suc i) zero = zero
+thin (suc i) (suc j) = suc (thin i j)
+-}
+-- | The \"face maps\" for @Fin@ viewed as the standard simplices
+-- (aka: the thinning view). Traditionally spelled with delta or
+-- epsilon. For each @i@, it is the unique injective monotonic map
+-- that skips @i@. That is,
+--
+-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thin i j /= i
+--
+thin :: (NatLE n MaxBoundInt8, Succ m n) => Fin n -> Fin m -> Fin n
+thin i j
+ | weaken j < i = weaken j
+ | otherwise = succ (weaken j)
+{-# INLINE thin #-}
+
+
+-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it.
+-- | The \"degeneracy maps\" for @Fin@ viewed as the standard
+-- simplices. Traditionally spelled with sigma or eta. For each
+-- @i@, it is the unique surjective monotonic map that covers @i@
+-- twice. That is,
+--
+-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thick i (i+1) == i
+--
+thick
+ :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, Succ m n)
+ => Fin m -> Fin n -> Fin m
+thick i j =
+ case maxView (if j <= weaken i then j else pred j) of
+ Just j' -> j'
+ Nothing -> _thick_impossible
+{-# INLINE thick #-}
+
+
+
+{-
+-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne?
+-- The non zero view, which is used for defining compare...
+data NonEmptyView : {n : Nat} -> Fin n -> Set where
+ ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i
+
+nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i
+nonEmpty zero = ne
+nonEmpty (suc _) = ne
+
+
+data EqView : {n : Nat} -> Fin n -> Fin n -> Set where
+ equal : {n : Nat}{i : Fin n} -> EqView i i
+ notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j)
+
+compare : {n : Nat}(i j : Fin n) -> EqView i j
+compare zero zero = equal
+compare zero (suc j) = notequal j
+compare (suc i) zero with nonEmpty i
+... | ne = notequal zero
+compare (suc i) (suc j) with compare i j
+compare (suc i) (suc .i) | equal = equal
+compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j)
+-}
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- Error messages
+
+__ :: a
+__ = error "Data.Number.Fin.Int8: attempted to evaluate type token"
+{-# NOINLINE __ #-}
+-- TODO: use extensible-exceptions instead of 'error'
+-- TODO: use Proxy instead of these undefined values...
+
+_thick_impossible :: a
+_thick_impossible =
+ error "Data.Number.Fin.Int8.thick: the impossible happened"
+{-# NOINLINE _thick_impossible #-}
+-- TODO: use extensible-exceptions instead of 'error'
+
+_succ_maxBound :: String -> a
+_succ_maxBound ty =
+ error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound"
+{-# NOINLINE _succ_maxBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_pred_minBound :: String -> a
+_pred_minBound ty =
+ error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound"
+{-# NOINLINE _pred_minBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_toEnum_OOR :: String -> a
+_toEnum_OOR ty =
+ error $ "Enum.toEnum{"++ty++"}: argument out of range"
+{-# NOINLINE _toEnum_OOR #-}
+-- TODO: is there an extensible-exception for this?
+
+----------------------------------------------------------------
+----------------------------------------------------------- fin.
diff --git a/src/Data/Number/Fin/Integer.hs b/src/Data/Number/Fin/Integer.hs
new file mode 100644
index 0000000..835d6fe
--- /dev/null
+++ b/src/Data/Number/Fin/Integer.hs
@@ -0,0 +1,828 @@
+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+{-# LANGUAGE ScopedTypeVariables
+ , DeriveDataTypeable
+ , MultiParamTypeClasses
+ , FlexibleContexts
+ , CPP
+ , Rank2Types
+ #-}
+
+#if __GLASGOW_HASKELL__ >= 701
+-- N.B., Data.Proxy and Test.QuickCheck aren't "safe".
+{-# LANGUAGE Trustworthy #-}
+#endif
+----------------------------------------------------------------
+-- 2013.07.20
+-- |
+-- Module : Data.Number.Fin.Integer
+-- Copyright : 2012--2013 wren ng thornton
+-- License : BSD3
+-- Maintainer : wren@community.haskell.org
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- A newtype of 'Integer' for finite subsets of the natural numbers.
+----------------------------------------------------------------
+module Data.Number.Fin.Integer
+ (
+ -- * @Fin@, finite sets of natural numbers
+ Fin()
+
+ -- ** Showing types
+ , showFinType
+ , showsFinType
+
+ -- ** Convenience functions
+ , minBoundOf
+ , maxBoundOf
+
+ -- ** Introduction and elimination
+ , toFin
+ , toFinProxy
+ , toFinCPS
+ , fromFin
+
+ -- ** Views and coersions
+ -- *** Weakening and maximum views
+ , weaken
+ , weakenLE
+ , weakenPlus
+ , maxView
+ , maxViewLE
+
+ -- *** Widening and the predecessor view
+ , widen
+ , widenLE
+ , widenPlus
+ , predView
+
+ -- *** The ordinal-sum functor
+ , plus
+ , unplus
+ , fplus
+
+ -- *** Face- and degeneracy-maps
+ , thin
+ , thick
+ -- TODO: is there any way to get equality to work right?
+ ) where
+
+import qualified Prelude.SafeEnum as SE
+import Data.Ix
+import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE)
+import Data.Typeable (Typeable)
+import Data.Proxy (Proxy(Proxy))
+import Data.Reflection (Reifies(reflect), reify)
+import Control.Monad (liftM)
+
+import qualified Test.QuickCheck as QC
+#if (MIN_VERSION_smallcheck(0,6,0))
+import qualified Test.SmallCheck.Series as SC
+#else
+import qualified Test.SmallCheck as SC
+#endif
+import qualified Test.LazySmallCheck as LSC
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- | A finite set of integers @Fin n = { i :: Integer | 0 <= i < n }@
+-- with the usual ordering. This is typed as if using the standard
+-- GADT presentation of @Fin n@, however it is actually implemented
+-- by a plain 'Integer'.
+--
+-- If you care more about performance than mathematical accuracy,
+-- see "Data.Number.Fin.Int32" for an alternative implementation
+-- as a newtype of 'Int32'. Note, however, that doing so makes it
+-- harder to reason about code since it introduces many corner
+-- cases.
+newtype Fin n = Fin Integer
+ deriving Typeable
+ -- WART: to give additional constraints (e.g., Nat n) on derived
+ -- instances (e.g., Show, Eq, Ord), we need to specify the
+ -- constraints on the data type declaration; however, giving of
+ -- data-type constraints is deprecated and will be removed from
+ -- the language...
+
+{-
+-- Some fusion rules for treating newtypes like 'id', or as close
+-- as we can. We only have these fire in the last stage so that
+-- they don't inhibit the usual list-fusion rules. Hopefully there's
+-- nothing important which is defined to not fire at [0].
+--
+-- TODO: add other laws regarding 'id'
+{-# RULES
+"map Fin" [0] map Fin = unsafeCoerce
+"fmap Fin" [0] fmap Fin = unsafeCoerce
+"liftM Fin" [0] liftM Fin = unsafeCoerce
+"liftA Fin" [0] liftA Fin = unsafeCoerce
+ #-}
+-}
+
+{- TODO:
+-- also: <http://paczesiowa.blogspot.com/2010/01/pure-extensible-exceptions-and-self.html>
+
+-- | An error for attempts to evaluate an undefined value which is
+-- passed around as a type token. The string should give the source
+-- where the token was generated, or some other helpful information
+-- for tracking the problem down.
+data EvaluatedTypeTokenException = EvaluatedTypeTokenException String
+ deriving (Typeable, Show)
+
+instance Exception EvaluatedTypeTokenException
+
+-- | Construct a type token with the given message.
+__ :: String -> a
+__ here = throw (EvaluatedTypeTokenException here)
+
+
+-- TODO: use Control.Exception.assert instead?
+data FinException = FinOOB (Fin n)
+ deriving (Typeable)
+
+instance Show FinException where
+ show (FinOOB x) =
+ "Value "++show x++" out of bounds for "++showFinType x
+
+instance Exception FinException
+-}
+
+
+-- | Often, we don't want to use the @Fin n@ as a proxy, since that
+-- would introduce spurious data dependencies. This function ignores
+-- its argument (other than for type propagation) so, hopefully,
+-- via massive inlining this function will avoid that spurious
+-- dependency. Hopefully...
+--
+-- Also, this lets us minimize the use of @-XScopedTypeVariables@
+-- which makes the Haddocks ugly. And so it lets us avoid the hacks
+-- to hide our use of @-XScopedTypeVariables@.
+--
+-- TODO: is this enough to ensure reflection is/can-be done at compile-time?
+-- TODO: is there any way to tell GHC that this function should /never/ appear in the output of compilation?
+fin2proxy :: Nat n => fin n -> Proxy n
+fin2proxy _ = Proxy
+{-# INLINE fin2proxy #-}
+
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance Nat n => Show (Fin n) where
+ showsPrec d (Fin i) =
+ showParen (d > 10) $ ("Fin "++) . shows i
+
+
+-- | Like 'show', except it shows the type itself instead of the
+-- value.
+showFinType :: Nat n => Fin n -> String
+showFinType x = showsFinType x []
+{-# INLINE showFinType #-}
+-- Should never fire, due to inlining
+{- RULES
+"showFinType/++" forall x s. showFinType x ++ s = showsFinType x s
+ -}
+
+
+-- | Like 'shows', except it shows the type itself instead of the
+-- value.
+showsFinType :: Nat n => Fin n -> ShowS
+showsFinType x = ("Fin "++) . shows (reflect (fin2proxy x))
+{-# INLINE [0] showsFinType #-}
+-- TODO: Is [0] the best level to start inlining showsFinType?
+{-# RULES
+"showsFinType/++" forall x s1 s2.
+ showsFinType x s1 ++ s2 = showsFinType x (s1 ++ s2)
+ #-}
+
+-- TODO: showsPrecFinType?
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Read, since that would inject invalid numbers!
+instance Nat n => Read (Fin n) where
+ readsPrec d =
+ readParen (d > 10) $ \s0 -> do
+ ("Fin", s1) <- lex s0
+ (i, s2) <- readsPrec 11 s1
+ maybe [] (\n -> [(n,s2)]) (toFin i)
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance Nat n => Eq (Fin n) where
+ Fin i == Fin j = i == j
+ Fin i /= Fin j = i /= j
+ {-# INLINE (==) #-}
+ {-# INLINE (/=) #-}
+
+----------------------------------------------------------------
+-- HACK: Not derived, just so we can add the @Nat n@ constraint...
+instance Nat n => Ord (Fin n) where
+ Fin i < Fin j = i < j
+ Fin i <= Fin j = i <= j
+ Fin i > Fin j = i > j
+ Fin i >= Fin j = i >= j
+ compare (Fin i) (Fin j) = compare i j
+ min (Fin i) (Fin j) = Fin (min i j)
+ max (Fin i) (Fin j) = Fin (max i j)
+ {-# INLINE (<) #-}
+ {-# INLINE (<=) #-}
+ {-# INLINE (>) #-}
+ {-# INLINE (>=) #-}
+ {-# INLINE compare #-}
+ {-# INLINE min #-}
+ {-# INLINE max #-}
+
+----------------------------------------------------------------
+instance Nat n => Bounded (Fin n) where
+ minBound = Fin 0
+ maxBound = Fin (reflect (Proxy :: Proxy n) - 1)
+ {-# INLINE minBound #-}
+ {-# INLINE maxBound #-}
+
+
+-- | Return the 'minBound' of @Fin n@ as a plain integer. This is
+-- always zero, but is provided for symmetry with 'maxBoundOf'.
+minBoundOf :: Nat n => Fin n -> Integer
+minBoundOf _ = 0
+{-# INLINE minBoundOf #-}
+
+
+-- | Return the 'maxBound' of @Fin n@ as a plain integer. This is
+-- always @n-1@, but it's helpful because you may not know what
+-- @n@ is at the time.
+maxBoundOf :: Nat n => Fin n -> Integer
+maxBoundOf x = reflect (fin2proxy x) - 1
+{-# INLINE maxBoundOf #-}
+
+
+----------------------------------------------------------------
+-- N.B., we cannot derive Enum, since that would inject invalid numbers!
+-- N.B., we're using partial functions, because H98 requires it!
+instance Nat n => Enum (Fin n) where
+ succ x =
+ case SE.succ x of
+ Just y -> y
+ Nothing -> _succ_maxBound "Fin" -- cf, @GHC.Word.succError@
+ {-# INLINE succ #-}
+
+ pred x =
+ case SE.pred x of
+ Just y -> y
+ Nothing -> _pred_minBound "Fin" -- cf, @GHC.Word.predError@
+ {-# INLINE pred #-}
+
+ toEnum i =
+ case SE.toEnum i of
+ Just y -> y
+ Nothing -> _toEnum_OOR "Fin" -- cf, @GHC.Word.toEnumError@
+ {-# INLINE toEnum #-}
+
+ fromEnum = fromInteger . fromFin
+ {-# INLINE fromEnum #-}
+
+ -- Hopefully list fusion will get rid of the map, and preserve
+ -- the fusion tricks in GHC.Enum...
+ enumFrom x@(Fin i) = map Fin (enumFromTo i (maxBoundOf x))
+ enumFromThen x@(Fin i) (Fin j)
+ | j >= i = map Fin (enumFromThenTo i j (maxBoundOf x))
+ | otherwise = map Fin (enumFromThenTo i j (minBoundOf x))
+ enumFromTo (Fin i) (Fin k) = map Fin (enumFromTo i k)
+ enumFromThenTo (Fin i) (Fin j) (Fin k) = map Fin (enumFromThenTo i j k)
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromTo #-}
+ {-# INLINE enumFromThenTo #-}
+
+{-
+_pred_succ :: Nat n => Fin n -> Fin n
+_pred_succ x = if x == maxBound then _succ_maxBound "Fin" else x
+{-# INLINE _pred_succ #-}
+
+_succ_pred :: Nat n => Fin n -> Fin n
+_succ_pred x = if x == minBound then _pred_minBound "Fin" else x
+{-# INLINE _succ_pred #-}
+
+-- BUG: how can we introduce the (Nat n) constraint? Floating out the RHSs to give them signatures doesn't help.
+{-# RULES
+"pred (succ x) :: Fin n" forall x. pred (succ x) = _pred_succ x
+"pred . succ :: Fin n -> Fin n" pred . succ = _pred_succ
+
+"succ (pred x) :: Fin n" forall x. succ (pred x) = _succ_pred x
+"succ . pred :: Fin n -> Fin n" succ . pred = _succ_pred
+ #-}
+-}
+
+instance Nat n => SE.UpwardEnum (Fin n) where
+ succ x@(Fin i)
+ | x < maxBound = Just $! Fin (i + 1)
+ | otherwise = Nothing
+ succeeds = (>)
+ enumFrom = enumFrom
+ enumFromTo = enumFromTo
+ {-# INLINE succ #-}
+ {-# INLINE succeeds #-}
+ {-# INLINE enumFrom #-}
+ {-# INLINE enumFromTo #-}
+
+instance Nat n => SE.DownwardEnum (Fin n) where
+ pred (Fin i)
+ | 0 < i = Just $! Fin (i - 1)
+ | otherwise = Nothing
+ precedes = (<)
+ enumDownFrom (Fin i) = map Fin (enumFromThenTo i (i-1) 0)
+ enumDownFromTo (Fin i) (Fin k) = map Fin (enumFromThenTo i (i-1) (max 0 k))
+ {-# INLINE pred #-}
+ {-# INLINE precedes #-}
+ {-# INLINE enumDownFrom #-}
+ {-# INLINE enumDownFromTo #-}
+
+instance Nat n => SE.Enum (Fin n) where
+ toEnum i
+ | 0 <= j && j <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ j = toInteger i
+ x = Fin j :: Fin n
+ fromEnum x = Just $! (fromInteger . fromFin) x
+ enumFromThen = enumFromThen
+ enumFromThenTo = enumFromThenTo
+ {-# INLINE toEnum #-}
+ {-# INLINE fromEnum #-}
+ {-# INLINE enumFromThen #-}
+ {-# INLINE enumFromThenTo #-}
+
+
+-- TODO: can we trust the validity of the input arguments?
+instance Nat n => Ix (Fin n) where
+ index (Fin i, Fin j) (Fin k) = index (i,j) k
+ range (Fin i, Fin j) = map Fin (range (i,j))
+ inRange (Fin i, Fin j) (Fin k) = inRange (i,j) k
+ rangeSize (Fin i, Fin j) = rangeSize (i,j)
+
+
+----------------------------------------------------------------
+-- TODO: define Num, Real, Integral? (N.B., Can't derive them safely.)
+
+
+----------------------------------------------------------------
+-- TODO: why was the checking stuff done using exceptions instead of Maybe?
+-- TODO: can we successfully ensure that invalid values can *never* be constructed?
+
+
+-- | A version of 'const' which checks that the second argument is
+-- in fact valid for its type before returning the first argument.
+-- Throws an exception if the @Fin n@ is invalid. The name and
+-- argument ordering are indended for infix use.
+checking :: Nat n => a -> Fin n -> a
+checking a x
+ | minBound <= x && x <= maxBound = a
+ | otherwise = _checking_OOR x
+{-# INLINE checking #-}
+
+
+-- TODO: use extensible-exceptions instead of 'error'
+_checking_OOR :: Nat n => Fin n -> a
+_checking_OOR x = error
+ . ("The value "++)
+ . shows x
+ . (" is out of bounds for "++)
+ . showsFinType x
+ $ ". This is a library error; contact the maintainer."
+
+
+-- | Extract the value of a @Fin n@.
+--
+-- /N.B.,/ if somehow the @Fin n@ value was constructed invalidly,
+-- then this function will throw an exception. However, this should
+-- /never/ happen. If it does, contact the maintainer since this
+-- indicates a bug\/insecurity in this library.
+fromFin :: Nat n => Fin n -> Integer
+fromFin x@(Fin i) = i `checking` x
+{-# INLINE fromFin #-}
+
+
+-- | Safely embed a number into @Fin n@. Use of this function will
+-- generally require an explicit type signature in order to know
+-- which @n@ to use.
+toFin :: Nat n => Integer -> Maybe (Fin n)
+toFin = toFin_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous?
+ toFin_ :: forall n. Nat n => Integer -> Maybe (Fin n)
+ toFin_ i
+ | 0 <= i && i <= maxBoundOf x = Just x
+ | otherwise = Nothing
+ where
+ x = Fin i :: Fin n
+ {-# INLINE toFin_ #-}
+{-# INLINE toFin #-}
+
+-- TODO: RULES for toFin.fromFin and fromFin.toFin
+
+
+-- | Safely embed a number into @Fin n@. This variant of 'toFin'
+-- uses a proxy to avoid the need for type signatures.
+toFinProxy :: Nat n => proxy n -> Integer -> Maybe (Fin n)
+toFinProxy _ = toFin
+{-# INLINE toFinProxy #-}
+
+
+-- | Safely embed integers into @Fin n@, where @n@ is the first
+-- argument. We use rank-2 polymorphism to render the type-level
+-- @n@ existentially quantified, thereby hiding the dependent type
+-- from the compiler. However, @n@ will in fact be a skolem, so we
+-- can't provide the continuation with proof that @Nat n@ ---
+-- unfortunately, rendering this function of little use.
+--
+-- > toFinCPS n k i
+-- > | 0 <= i && i < n = Just (k i) -- morally speaking...
+-- > | otherwise = Nothing
+--
+toFinCPS :: Integer -> (forall n. Reifies n Integer => Fin n -> r) -> Integer -> Maybe r
+toFinCPS n k i
+ | 0 <= i && i < n = Just (reify n $ \(_ :: Proxy n) -> k (Fin i :: Fin n))
+ | otherwise = Nothing
+{-# INLINE toFinCPS #-}
+-- BUG: can't use @Nat n@ because: Could not deduce (Nat_ n) from the context (Reifies n Integer)
+-- TODO: how can we get Data.Number.Fin.TyDecimal.reifyNat to work?
+
+
+----------------------------------------------------------------
+instance Nat n => QC.Arbitrary (Fin n) where
+ shrink = tail . SE.enumDownFrom
+ arbitrary
+ | x >= 0 = Fin `liftM` QC.choose (0,x)
+ | otherwise =
+ -- BUG: there's no way to say it's impossible...
+ error . ("Arbitrary.arbitrary{"++)
+ . showsFinType (__ :: Fin n)
+ $ "}: this type is empty"
+ -- TODO: use extensible-exceptions instead of 'error'
+ where
+ x = maxBoundOf (__ :: Fin n)
+
+
+
+instance Nat n => QC.CoArbitrary (Fin n) where
+ coarbitrary (Fin n) = QC.variant n
+
+
+instance Nat n => SC.Serial (Fin n) where
+ series d
+ | d < 0 = [] -- paranoia.
+ | otherwise =
+ case toFin (toInteger d) of
+ Nothing -> enumFromTo minBound maxBound
+ Just n -> enumFromTo minBound n
+
+ coseries rs d =
+ [ \(Fin i) ->
+ if i > 0
+ then let j = Fin (i-1) :: Fin n
+ in f j `checking` j -- more paranoia; in case n==0 or i>n
+ else z
+ | z <- SC.alts0 rs d
+ , f <- SC.alts1 rs d
+ ]
+
+instance Nat n => LSC.Serial (Fin n) where
+ series = LSC.drawnFrom . SC.series
+
+
+----------------------------------------------------------------
+-- TODO: do we care about <http://ncatlab.org/nlab/show/decalage>?
+
+
+-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe?
+{- -- Agda's version:
+data MaxView {n : Nat} : Fin (suc n) -> Set where
+ theMax : MaxView (fromNat n)
+ notMax : (i : Fin n) -> MaxView (weaken i)
+
+maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i
+maxView {zero} zero = theMax
+maxView {zero} (suc ())
+maxView {suc n} zero = notMax zero
+maxView {suc n} (suc i) with maxView i
+maxView {suc n} (suc .(fromNat n)) | theMax = theMax
+maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i)
+-}
+-- | The maximum-element view. This strengthens the type by removing
+-- the maximum element:
+--
+-- > maxView maxBound = Nothing
+-- > maxView x = Just x -- morally speaking...
+--
+-- The opposite of this function is 'weaken'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+maxView :: Succ m n => Fin n -> Maybe (Fin m)
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n)
+maxView = maxView_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@...
+ maxView_ :: forall m n. Succ m n => Fin n -> Maybe (Fin m)
+ maxView_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxView_ #-}
+{-# INLINE maxView #-}
+
+
+-- | A variant of 'maxView' which allows strengthening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @m@ to use.
+--
+-- The opposite of this function is 'weakenLE'. When the choice of
+-- @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+maxViewLE :: NatLE m n => Fin n -> Maybe (Fin m)
+maxViewLE = maxViewLE_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ maxViewLE_ :: forall m n. NatLE m n => Fin n -> Maybe (Fin m)
+ maxViewLE_ (Fin i)
+ | i <= maxBoundOf y = Just y
+ | otherwise = Nothing
+ where
+ y = Fin i :: Fin m
+ {-# INLINE maxViewLE_ #-}
+{-# INLINE maxViewLE #-}
+
+
+-- TODO: maxViewPlus?
+
+
+-- This type-restricted version is a~la Agda.
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'minBound'. That is,
+--
+-- > fromFin (weaken x) == fromFin x
+--
+-- The opposite of this function is 'maxView'.
+--
+-- > maxView . weaken == Just
+-- > maybe maxBound weaken . maxView == id
+--
+weaken :: Succ m n => Fin m -> Fin n
+-- BUG: Could not deduce (NatLE m n) from the context (Succ m n)
+weaken (Fin i) = Fin i
+{-# INLINE weaken #-}
+
+
+-- | A variant of 'weaken' which allows weakening the type by
+-- multiple steps. Use of this function will generally require an
+-- explicit type signature in order to know which @n@ to use.
+--
+-- The opposite of this function is 'maxViewLE'. When the choice
+-- of @m@ and @n@ is held constant, we have that:
+--
+-- > maxViewLE . weakenLE == Just
+-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)
+--
+weakenLE :: NatLE m n => Fin m -> Fin n
+weakenLE (Fin i) = Fin i
+{-# INLINE weakenLE #-}
+
+
+----------------------------------------------------------------
+-- | The predecessor view. This strengthens the type by shifting
+-- everything down by one:
+--
+-- > predView 0 = Nothing
+-- > predView x = Just (x-1) -- morally speaking...
+--
+-- The opposite of this function is 'widen'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+predView :: Succ m n => Fin n -> Maybe (Fin m)
+predView (Fin i)
+ | i <= 0 = Nothing
+ | otherwise = Just $! Fin (i-1)
+{-# INLINE predView #-}
+
+
+-- TODO: predViewLE? predViewPlus?
+
+
+-- | Embed a finite domain into the next larger one, keeping the
+-- same position relative to 'maxBound'. That is, we shift everything
+-- up by one:
+--
+-- > fromFin (widen x) == 1 + fromFin x
+--
+-- The opposite of this function is 'predView'.
+--
+-- > predView . widen == Just
+-- > maybe 0 widen . predView == id
+--
+widen :: Succ m n => Fin m -> Fin n
+widen (Fin i) = Fin (i+1)
+{-# INLINE widen #-}
+
+
+-- | Embed a finite domain into any larger one, keeping the same
+-- position relative to 'maxBound'. That is,
+--
+-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
+-- > where y = widenLE x
+--
+-- Use of this function will generally require an explicit type
+-- signature in order to know which @n@ to use.
+widenLE :: NatLE m n => Fin m -> Fin n
+widenLE x@(Fin i) = y
+ where
+ y = Fin (maxBoundOf y - maxBoundOf x + i)
+{-# INLINE widenLE #-}
+
+
+----------------------------------------------------------------
+-- BUG: Could not deduce (NatLE m o) from the context (Add m n o)
+-- | A type-signature variant of 'weakenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE m o@. This is the
+-- left half of 'plus'.
+weakenPlus :: Add m n o => Fin m -> Fin o
+weakenPlus (Fin i) = Fin i
+{-# INLINE weakenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE n o) from the context (Add m n o)
+-- | A type-signature variant of 'widenLE' because we cannot
+-- automatically deduce that @Add m n o ==> NatLE n o@. This is the
+-- right half of 'plus'.
+widenPlus :: Add m n o => Fin n -> Fin o
+widenPlus = widenPlus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ widenPlus_ :: forall m n o. Add m n o => Fin n -> Fin o
+ widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y)
+ {-# INLINE widenPlus_ #-}
+{-# INLINE widenPlus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- | The ordinal-sum functor, on objects. This internalizes the
+-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ 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
+plus = either weakenPlus widenPlus
+{-# INLINE plus #-}
+
+
+-- | The inverse of 'plus'.
+unplus :: Add m n o => Fin o -> Either (Fin m) (Fin n)
+unplus = unplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ unplus_ :: forall m n o. Add m n o => Fin o -> Either (Fin m) (Fin n)
+ unplus_ (Fin i)
+ | i <= x = Left $! Fin i
+ | otherwise = Right $! Fin (i-x)
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE unplus_ #-}
+{-# INLINE unplus #-}
+
+
+-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o)
+-- BUG: Ditto for (Add m' n' o')
+-- | 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
+-- @(+++)@ from "Control.Arrow".
+fplus :: (Add m n o, Add m' n' o')
+ => (Fin m -> Fin m') -- ^ The left morphism
+ -> (Fin n -> Fin n') -- ^ The right morphism
+ -> (Fin o -> Fin o') -- ^
+fplus = fplus_
+ where
+ -- HACK: Hiding the use of -XScopedTypeVariables from Haddock
+ fplus_ :: forall m n o m' n' o'. (Add m n o, Add m' n' o')
+ => (Fin m -> Fin m') -> (Fin n -> Fin n') -> Fin o -> Fin o'
+ fplus_ f g (Fin i)
+ | i <= x = weakenPlus (f $! Fin i)
+ | otherwise = widenPlus (g $! Fin (i-x))
+ where
+ x = maxBoundOf (__ :: Fin m)
+ {-# INLINE fplus_ #-}
+{-# INLINE fplus #-}
+
+-- TODO: unfplus :: (Fin o -> Fin o') -> (Fin m -> Fin m', Fin n -> Fin n')
+
+-- TODO: (Fin m, Fin n) <-> Fin (Times m n)
+
+----------------------------------------------------------------
+{- -- Agda's version:
+thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n)
+thin zero j = suc j
+thin (suc i) zero = zero
+thin (suc i) (suc j) = suc (thin i j)
+-}
+-- | The \"face maps\" for @Fin@ viewed as the standard simplices
+-- (aka: the thinning view). Traditionally spelled with delta or
+-- epsilon. For each @i@, it is the unique injective monotonic map
+-- that skips @i@. That is,
+--
+-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thin i j /= i
+--
+thin :: Succ m n => Fin n -> Fin m -> Fin n
+thin i j
+ | weaken j < i = weaken j
+ | otherwise = succ (weaken j)
+{-# INLINE thin #-}
+
+
+-- | The \"degeneracy maps\" for @Fin@ viewed as the standard
+-- simplices. Traditionally spelled with sigma or eta. For each
+-- @i@, it is the unique surjective monotonic map that covers @i@
+-- twice. That is,
+--
+-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking...
+--
+-- Which has the important universal property that:
+--
+-- > thick i (i+1) == i
+--
+thick :: Succ m n => Fin m -> Fin n -> Fin m
+thick i j =
+ case maxView (if j <= weaken i then j else pred j) of
+ Just j' -> j'
+ Nothing -> _thick_impossible
+{-# INLINE thick #-}
+
+
+
+{-
+-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne?
+-- The non zero view, which is used for defining compare...
+data NonEmptyView : {n : Nat} -> Fin n -> Set where
+ ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i
+
+nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i
+nonEmpty zero = ne
+nonEmpty (suc _) = ne
+
+
+data EqView : {n : Nat} -> Fin n -> Fin n -> Set where
+ equal : {n : Nat}{i : Fin n} -> EqView i i
+ notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j)
+
+compare : {n : Nat}(i j : Fin n) -> EqView i j
+compare zero zero = equal
+compare zero (suc j) = notequal j
+compare (suc i) zero with nonEmpty i
+... | ne = notequal zero
+compare (suc i) (suc j) with compare i j
+compare (suc i) (suc .i) | equal = equal
+compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j)
+-}
+
+----------------------------------------------------------------
+----------------------------------------------------------------
+-- Error messages
+
+__ :: a
+__ = error "Data.Number.Fin: attempted to evaluate type token"
+{-# NOINLINE __ #-}
+-- TODO: use extensible-exceptions instead of 'error'
+-- TODO: use Proxy instead of these undefined values...
+
+_thick_impossible :: a
+_thick_impossible = error "Data.Number.Fin.thick: the impossible happened"
+{-# NOINLINE _thick_impossible #-}
+-- TODO: use extensible-exceptions instead of 'error'
+
+_succ_maxBound :: String -> a
+_succ_maxBound ty =
+ error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound"
+{-# NOINLINE _succ_maxBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_pred_minBound :: String -> a
+_pred_minBound ty =
+ error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound"
+{-# NOINLINE _pred_minBound #-}
+-- TODO: is there an extensible-exception for this?
+
+_toEnum_OOR :: String -> a
+_toEnum_OOR ty =
+ error $ "Enum.toEnum{"++ty++"}: argument out of range"
+{-# NOINLINE _toEnum_OOR #-}
+-- TODO: is there an extensible-exception for this?
+
+----------------------------------------------------------------
+----------------------------------------------------------- fin.
diff --git a/src/Data/Number/Fin/TyDecimal.hs b/src/Data/Number/Fin/TyDecimal.hs
new file mode 100644
index 0000000..725afb1
--- /dev/null
+++ b/src/Data/Number/Fin/TyDecimal.hs
@@ -0,0 +1,941 @@
+-- TODO: see also <http://okmij.org/ftp/Haskell/PeanoArithm.lhs>
+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+{-# LANGUAGE EmptyDataDecls
+ , DeriveDataTypeable
+ , MultiParamTypeClasses
+ , FlexibleContexts
+ , FlexibleInstances
+ , UndecidableInstances
+ , FunctionalDependencies
+ , TypeOperators
+ #-}
+{-
+-- for reifyNat...
+{-# LANGUAGE RankNTypes #-}
+-}
+
+{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ >= 701
+-- N.B., Data.Proxy isn't "safe".
+{-# LANGUAGE Trustworthy #-}
+#endif
+----------------------------------------------------------------
+-- 2013.05.29
+-- |
+-- Module : Data.Number.Fin.TyDecimal
+-- Copyright : 2012--2013 wren ng thornton,
+-- 2004--2007 Oleg Kiselyov and Chung-chieh Shan
+-- License : BSD3
+-- Maintainer : wren@community.haskell.org
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- Type-level decimal natural numbers. This is based on [1], and is
+-- intended to work with [2] (though we use the @reflection@ 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 @HList:Data.HList.FakePrelude@[3], which is (or should be)
+-- obviated by the new data kinds extension.
+--
+-- [1] Oleg Kiselyov and Chung-chieh Shan. (2007) /Lightweight/
+-- /static resources: Sexy types for embedded and systems/
+-- /programming/. Proc. Trends in Functional Programming.
+-- New York, 2--4 April 2007.
+-- <http://okmij.org/ftp/Haskell/types.html#binary-arithm>
+--
+-- [2] Oleg Kiselyov and Chung-chieh Shan. (2004) /Implicit/
+-- /configurations: or, type classes reflect the values of/
+-- /types/. Proc. ACM SIGPLAN 2004 workshop on Haskell.
+-- Snowbird, Utah, USA, 22 September 2004. pp.33--44.
+-- <http://okmij.org/ftp/Haskell/types.html#Prepose>
+--
+-- [3] <http://hackage.haskell.org/package/HList>
+----------------------------------------------------------------
+module Data.Number.Fin.TyDecimal
+ (
+ -- * Representation
+ -- ** Type-level decimal natural numbers
+ D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, (:.)
+ -- ** Type-level 'Ordering'
+ , LT_, EQ_, GT_
+
+ -- * Kind predicates
+ , Nat, NatNE0
+ -- * Proxies for some small numbers
+ , nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9
+ -- * Aliases for some large numbers
+ , MaxBoundInt8
+ , MaxBoundInt16
+ , MaxBoundInt32
+ , MaxBoundInt64
+ , MaxBoundWord8
+ , MaxBoundWord16
+ , MaxBoundWord32
+ , MaxBoundWord64
+
+ -- * Arithmetic
+ -- ** successor\/predecessor
+ , Succ, succ, pred
+ -- ** addition\/subtraction
+ , Add, add, minus, subtract
+ -- ** comparison
+ , Compare, compare, NatLE, NatLT, assert_NatLE, min, max
+ {-
+ -- ** multiplication\/division
+ , Mul, mul, div, div10 -- mul10 ?
+ -- ** exponentiation\/logarithm
+ , Exp10, exp10, log10
+ -- ** GCD
+ , GCD, gcd
+ -}
+ ) where
+
+import Prelude hiding (succ, pred, subtract, compare, div, gcd, max, min)
+import Data.Typeable (Typeable)
+import Data.Proxy (Proxy(Proxy))
+import Data.Reflection (Reifies(reflect))
+import Data.Number.Fin.TyOrdering
+----------------------------------------------------------------
+
+-- | The digit 0.
+data D0 deriving Typeable
+-- | The digit 1.
+data D1 deriving Typeable
+-- | The digit 2.
+data D2 deriving Typeable
+-- | The digit 3.
+data D3 deriving Typeable
+-- | The digit 4.
+data D4 deriving Typeable
+-- | The digit 5.
+data D5 deriving Typeable
+-- | The digit 6.
+data D6 deriving Typeable
+-- | The digit 7.
+data D7 deriving Typeable
+-- | The digit 8.
+data D8 deriving Typeable
+-- | The digit 9.
+data D9 deriving Typeable
+
+-- | 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 deriving Typeable
+infixl 5 :.
+
+
+-- | Is @n@ a well-formed type of kind @Nat@? The only well-formed
+-- types of kind @Nat@ are type-level natural numbers in structurally
+-- little-endian decimal.
+--
+-- The hidden type class @(Nat_ n)@ entails @(Reifies n Integer)@.
+class Nat_ n => Nat n
+instance Nat_ n => Nat n -- this instance is "undecidable"
+
+
+-- | Is @n@ a well-formed type of kind @NatNE0@? The only well-formed
+-- types of kind @NatNE0@ are the non-zero well-formed types of
+-- kind @Nat@;, i.e., the type-level whole numbers in structurally
+-- little-endian decimal.
+--
+-- The hidden type class @(NatNE0_ n)@ entails @(Nat_ n)@ and
+-- @(Reifies n Integer)@.
+class NatNE0_ n => NatNE0 n
+instance NatNE0_ n => NatNE0 n -- this instance is "undecidable"
+
+
+-- for internal use only.
+class Digit_ d
+instance Digit_ D0
+instance Digit_ D1
+instance Digit_ D2
+instance Digit_ D3
+instance Digit_ D4
+instance Digit_ D5
+instance Digit_ D6
+instance Digit_ D7
+instance Digit_ D8
+instance Digit_ D9
+
+-- for internal use only.
+class (Reifies n Integer, Nat_ n) => NatNE0_ n
+instance NatNE0_ D1
+instance NatNE0_ D2
+instance NatNE0_ D3
+instance NatNE0_ D4
+instance NatNE0_ D5
+instance NatNE0_ D6
+instance NatNE0_ D7
+instance NatNE0_ D8
+instance NatNE0_ D9
+instance NatNE0_ n => NatNE0_ (n:.D0)
+instance NatNE0_ n => NatNE0_ (n:.D1)
+instance NatNE0_ n => NatNE0_ (n:.D2)
+instance NatNE0_ n => NatNE0_ (n:.D3)
+instance NatNE0_ n => NatNE0_ (n:.D4)
+instance NatNE0_ n => NatNE0_ (n:.D5)
+instance NatNE0_ n => NatNE0_ (n:.D6)
+instance NatNE0_ n => NatNE0_ (n:.D7)
+instance NatNE0_ n => NatNE0_ (n:.D8)
+instance NatNE0_ n => NatNE0_ (n:.D9)
+
+-- for internal use only.
+class (Reifies n Integer) => Nat_ n
+instance Nat_ D0
+instance Nat_ D1
+instance Nat_ D2
+instance Nat_ D3
+instance Nat_ D4
+instance Nat_ D5
+instance Nat_ D6
+instance Nat_ D7
+instance Nat_ D8
+instance Nat_ D9
+instance NatNE0_ x => Nat_ (x:.D0)
+instance NatNE0_ x => Nat_ (x:.D1)
+instance NatNE0_ x => Nat_ (x:.D2)
+instance NatNE0_ x => Nat_ (x:.D3)
+instance NatNE0_ x => Nat_ (x:.D4)
+instance NatNE0_ x => Nat_ (x:.D5)
+instance NatNE0_ x => Nat_ (x:.D6)
+instance NatNE0_ x => Nat_ (x:.D7)
+instance NatNE0_ x => Nat_ (x:.D8)
+instance NatNE0_ x => Nat_ (x:.D9)
+
+
+-- BUG: stack overflow issues, unlike the big-endian notation?
+instance Reifies D0 Integer where reflect _ = 0
+instance Reifies D1 Integer where reflect _ = 1
+instance Reifies D2 Integer where reflect _ = 2
+instance Reifies D3 Integer where reflect _ = 3
+instance Reifies D4 Integer where reflect _ = 4
+instance Reifies D5 Integer where reflect _ = 5
+instance Reifies D6 Integer where reflect _ = 6
+instance Reifies D7 Integer where reflect _ = 7
+instance Reifies D8 Integer where reflect _ = 8
+instance Reifies D9 Integer where reflect _ = 9
+instance NatNE0_ x => Reifies (x:.D0) Integer where
+ reflect p = 10 * reflect (div10 p)
+instance NatNE0_ x => Reifies (x:.D1) Integer where
+ reflect p = 10 * reflect (div10 p) + 1
+instance NatNE0_ x => Reifies (x:.D2) Integer where
+ reflect p = 10 * reflect (div10 p) + 2
+instance NatNE0_ x => Reifies (x:.D3) Integer where
+ reflect p = 10 * reflect (div10 p) + 3
+instance NatNE0_ x => Reifies (x:.D4) Integer where
+ reflect p = 10 * reflect (div10 p) + 4
+instance NatNE0_ x => Reifies (x:.D5) Integer where
+ reflect p = 10 * reflect (div10 p) + 5
+instance NatNE0_ x => Reifies (x:.D6) Integer where
+ reflect p = 10 * reflect (div10 p) + 6
+instance NatNE0_ x => Reifies (x:.D7) Integer where
+ reflect p = 10 * reflect (div10 p) + 7
+instance NatNE0_ x => Reifies (x:.D8) Integer where
+ reflect p = 10 * reflect (div10 p) + 8
+instance NatNE0_ x => Reifies (x:.D9) Integer where
+ reflect p = 10 * reflect (div10 p) + 9
+
+-- HACK: we can't actually monomorphize the input, given our use case.
+-- | Return a 'Proxy' for the floor of the input divided by 10. Using
+-- @div10 n@ differs from using @n \`div\` nat10@ in that we take the
+-- floor of the result rather than being ill-typed; also in that
+-- @div10@ isn't defined on single-digit numbers.
+div10 :: proxy (h:.t) -> Proxy h
+div10 _ = Proxy
+{-# INLINE div10 #-}
+
+
+{-
+-- BUG: how can we do this CPS version which properly constrains @x@ to Nat_? It wasn't so hard with the big-endian notation...
+reifyNat :: Integer -> (forall x. Nat_ x => Proxy x -> r) -> r
+reifyNat i k
+ | i <= 0 = k (Proxy :: Proxy D0)
+ | otherwise =
+ let (d,m) = divMod i 10 in
+ case m of
+ 0 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D0)))
+ 1 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D1)))
+ 2 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D2)))
+ 3 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D3)))
+ 4 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D4)))
+ 5 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D5)))
+ 6 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D6)))
+ 7 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D7)))
+ 8 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D8)))
+ 9 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D9)))
+ _ -> error "Data.Number.Fin.TyDecimal.reifyNat: the impossible happened"
+ where
+ -- BUG: Could not deduce (Snoc x10 D0 x) from the context (Nat_ x10) [etc]
+ snoc :: Snoc x d y => Proxy x -> Proxy d -> Proxy y
+ snoc _ _ = Proxy
+-}
+
+
+
+nat0 :: Proxy D0; nat0 = Proxy
+nat1 :: Proxy D1; nat1 = Proxy
+nat2 :: Proxy D2; nat2 = Proxy
+nat3 :: Proxy D3; nat3 = Proxy
+nat4 :: Proxy D4; nat4 = Proxy
+nat5 :: Proxy D5; nat5 = Proxy
+nat6 :: Proxy D6; nat6 = Proxy
+nat7 :: Proxy D7; nat7 = Proxy
+nat8 :: Proxy D8; nat8 = Proxy
+nat9 :: Proxy D9; nat9 = Proxy
+
+
+-- type MinBoundInt8 = Negative (D1:.D2:.D8)
+-- type MinBoundInt16 = Negative (D3:.D2:. D7:.D6:.D8)
+-- type MinBoundInt32 = Negative (D2:. D1:.D4:.D7:. D4:.D8:.D3:. D6:.D4:.D8)
+-- type MinBoundInt64 =
+-- Negative (D9:. D2:.D2:.D3:. D3:.D7:.D2:. D0:.D3:.D6:. D8:.D5:.D4:. D7:.D7:.D5:. D8:.D0:.D8)
+-- TODO: MinBoundInt
+
+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
+-- TODO: MaxBoundInt
+
+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
+-- TODO: MaxBoundWord
+
+
+----------------------------------------------------------------
+-- BUG: We can't automatically deduce (NatLE x y) nor (NatLT x y) from (Succ x y). We can add them as additional constraints on the instances; and that works to get everything in this package to typecheck, but it causes infinite loops whenever we actually try to use Succ as a type-function in real code...
+
+-- | The successor\/predecessor relation; by structural induction
+-- on the first argument. Modes:
+--
+-- > 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
+--
+class (Nat_ x, NatNE0_ y) => Succ x y | x -> y, y -> x
+instance Succ D0 D1
+instance Succ D1 D2
+instance Succ D2 D3
+instance Succ D3 D4
+instance Succ D4 D5
+instance Succ D5 D6
+instance Succ D6 D7
+instance Succ D7 D8
+instance Succ D8 D9
+instance Succ D9 (D1:.D0)
+instance (NatNE0_ x) => Succ (x:.D0) (x :.D1)
+instance (NatNE0_ x) => Succ (x:.D1) (x :.D2)
+instance (NatNE0_ x) => Succ (x:.D2) (x :.D3)
+instance (NatNE0_ x) => Succ (x:.D3) (x :.D4)
+instance (NatNE0_ x) => Succ (x:.D4) (x :.D5)
+instance (NatNE0_ x) => Succ (x:.D5) (x :.D6)
+instance (NatNE0_ x) => Succ (x:.D6) (x :.D7)
+instance (NatNE0_ x) => Succ (x:.D7) (x :.D8)
+instance (NatNE0_ x) => Succ (x:.D8) (x :.D9)
+instance (NatNE0_ x, Succ x (y:.d)) => Succ (x:.D9) (y :.d :.D0)
+-- this last case triggers the need for undecidable instances <sigh>
+
+succ :: Succ x y => Proxy x -> Proxy y
+succ _ = Proxy
+{-# INLINE succ #-}
+
+pred :: Succ x y => Proxy y -> Proxy x
+pred _ = Proxy
+{-# INLINE pred #-}
+
+
+-- | Assert @10*x + d == y@ where @d@ is a decimal digit and both @x@
+-- and @y@ are decimal numbers. @x@ may be zero. Essentially, this
+-- is the general, non-structural, constructor\/deconstructor of a
+-- decimal number. This is like the assertion @x:.d ~ y@ except that
+-- we trim leading zeros of @y@ in order to ensure that it is
+-- well-formed.
+class (Digit_ d, Nat_ x, Nat_ y) => Snoc x d y | x d -> y, y -> x d
+instance Snoc D0 D0 D0
+instance Snoc D0 D1 D1
+instance Snoc D0 D2 D2
+instance Snoc D0 D3 D3
+instance Snoc D0 D4 D4
+instance Snoc D0 D5 D5
+instance Snoc D0 D6 D6
+instance Snoc D0 D7 D7
+instance Snoc D0 D8 D8
+instance Snoc D0 D9 D9
+instance (Digit_ d, Nat_ (D1:.d)) => Snoc D1 d (D1:.d)
+instance (Digit_ d, Nat_ (D2:.d)) => Snoc D2 d (D2:.d)
+instance (Digit_ d, Nat_ (D3:.d)) => Snoc D3 d (D3:.d)
+instance (Digit_ d, Nat_ (D4:.d)) => Snoc D4 d (D4:.d)
+instance (Digit_ d, Nat_ (D5:.d)) => Snoc D5 d (D5:.d)
+instance (Digit_ d, Nat_ (D6:.d)) => Snoc D6 d (D6:.d)
+instance (Digit_ d, Nat_ (D7:.d)) => Snoc D7 d (D7:.d)
+instance (Digit_ d, Nat_ (D8:.d)) => Snoc D8 d (D8:.d)
+instance (Digit_ d, Nat_ (D9:.d)) => Snoc D9 d (D9:.d)
+instance (Digit_ d', Nat_ (x:.d), Nat_ (x:.d:.d')) => Snoc (x:.d) d' (x:.d:.d')
+
+
+-- | The primitive addition relation; by structural induction on
+-- the first argument. Modes:
+--
+-- > Add_ x y (x+y)
+-- > Add_ x (z-x) z -- when it's defined.
+--
+class (Nat_ x, Nat_ y, Nat_ z) => Add_ x y z | x y -> z, z x -> y
+instance (Nat_ y) => Add_ D0 y y
+instance (Succ y y1) => Add_ D1 y y1
+instance (Succ y y1, Succ y1 y2) => Add_ D2 y y2
+instance (Succ y y1, Succ y1 y2, Succ y2 y3) => Add_ D3 y y3
+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
+ , Succ y3 y4, Succ y4 y5
+ ) => Add_ D5 y y5
+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, 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
+ , 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, Succ y7 y8, Succ y8 y9
+ ) => Add_ D9 y y9
+instance (NatNE0_ x, NatNE0_ (z:.dz), Add_ x y' z, Snoc y' dz y)
+ => Add_ (x:.D0) y (z:.dz)
+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, 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_ D3 (zh:.dy) z)
+ => Add_ (x:.D3) 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_ D5 (zh:.dy) z)
+ => Add_ (x:.D5) 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_ D7 (zh:.dy) z)
+ => Add_ (x:.D7) 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_ D9 (zh:.dy) z)
+ => Add_ (x:.D9) y z
+
+
+-- | The addition relation with full dependencies. Modes:
+--
+-- > Add x y (x+y)
+-- > Add x (z-x) z -- when it's defined.
+-- > Add (z-y) y z -- when it's defined.
+--
+class (Add_ x y z, Add_ y x z) => Add x y z | x y -> z, z x -> y, z y -> x
+instance (Add_ x y z, Add_ y x z) => Add x y z
+
+add :: Add x y z => Proxy x -> Proxy y -> Proxy z
+add _ _ = Proxy
+{-# INLINE add #-}
+
+-- | N.B., this will be ill-typed if @x@ is greater than @z@.
+minus :: Add x y z => Proxy z -> Proxy x -> Proxy y
+minus _ _ = Proxy
+{-# INLINE minus #-}
+
+-- | N.B., this will be ill-typed if @x@ is greater than @z@.
+subtract :: Add x y z => Proxy x -> Proxy z -> Proxy y
+subtract _ _ = Proxy
+{-# INLINE subtract #-}
+
+----------------------------------------------------------------
+-- Equality and order: the comparison relation
+
+-- | Assert that the comparison relation @r@ (@LT_@, @EQ_@, or
+-- @GT_@) holds between @x@ and @y@; by structural induction on the
+-- first, and then the second argument.
+class (Nat_ x, Nat_ y) => Compare x y r | x y -> r
+instance Compare D0 D0 EQ_
+instance Compare D0 D1 LT_
+instance Compare D0 D2 LT_
+instance Compare D0 D3 LT_
+instance Compare D0 D4 LT_
+instance Compare D0 D5 LT_
+instance Compare D0 D6 LT_
+instance Compare D0 D7 LT_
+instance Compare D0 D8 LT_
+instance Compare D0 D9 LT_
+instance NatNE0_ (y:.dy) => Compare D0 (y:.dy) LT_
+instance Compare D1 D0 GT_
+instance Compare D1 D1 EQ_
+instance Compare D1 D2 LT_
+instance Compare D1 D3 LT_
+instance Compare D1 D4 LT_
+instance Compare D1 D5 LT_
+instance Compare D1 D6 LT_
+instance Compare D1 D7 LT_
+instance Compare D1 D8 LT_
+instance Compare D1 D9 LT_
+instance NatNE0_ (y:.dy) => Compare D1 (y:.dy) LT_
+instance Compare D2 D0 GT_
+instance Compare D2 D1 GT_
+instance Compare D2 D2 EQ_
+instance Compare D2 D3 LT_
+instance Compare D2 D4 LT_
+instance Compare D2 D5 LT_
+instance Compare D2 D6 LT_
+instance Compare D2 D7 LT_
+instance Compare D2 D8 LT_
+instance Compare D2 D9 LT_
+instance NatNE0_ (y:.dy) => Compare D2 (y:.dy) LT_
+instance Compare D3 D0 GT_
+instance Compare D3 D1 GT_
+instance Compare D3 D2 GT_
+instance Compare D3 D3 EQ_
+instance Compare D3 D4 LT_
+instance Compare D3 D5 LT_
+instance Compare D3 D6 LT_
+instance Compare D3 D7 LT_
+instance Compare D3 D8 LT_
+instance Compare D3 D9 LT_
+instance NatNE0_ (y:.dy) => Compare D3 (y:.dy) LT_
+instance Compare D4 D0 GT_
+instance Compare D4 D1 GT_
+instance Compare D4 D2 GT_
+instance Compare D4 D3 GT_
+instance Compare D4 D4 EQ_
+instance Compare D4 D5 LT_
+instance Compare D4 D6 LT_
+instance Compare D4 D7 LT_
+instance Compare D4 D8 LT_
+instance Compare D4 D9 LT_
+instance NatNE0_ (y:.dy) => Compare D4 (y:.dy) LT_
+instance Compare D5 D0 GT_
+instance Compare D5 D1 GT_
+instance Compare D5 D2 GT_
+instance Compare D5 D3 GT_
+instance Compare D5 D4 GT_
+instance Compare D5 D5 EQ_
+instance Compare D5 D6 LT_
+instance Compare D5 D7 LT_
+instance Compare D5 D8 LT_
+instance Compare D5 D9 LT_
+instance NatNE0_ (y:.dy) => Compare D5 (y:.dy) LT_
+instance Compare D6 D0 GT_
+instance Compare D6 D1 GT_
+instance Compare D6 D2 GT_
+instance Compare D6 D3 GT_
+instance Compare D6 D4 GT_
+instance Compare D6 D5 GT_
+instance Compare D6 D6 EQ_
+instance Compare D6 D7 LT_
+instance Compare D6 D8 LT_
+instance Compare D6 D9 LT_
+instance NatNE0_ (y:.dy) => Compare D6 (y:.dy) LT_
+instance Compare D7 D0 GT_
+instance Compare D7 D1 GT_
+instance Compare D7 D2 GT_
+instance Compare D7 D3 GT_
+instance Compare D7 D4 GT_
+instance Compare D7 D5 GT_
+instance Compare D7 D6 GT_
+instance Compare D7 D7 EQ_
+instance Compare D7 D8 LT_
+instance Compare D7 D9 LT_
+instance NatNE0_ (y:.dy) => Compare D7 (y:.dy) LT_
+instance Compare D8 D0 GT_
+instance Compare D8 D1 GT_
+instance Compare D8 D2 GT_
+instance Compare D8 D3 GT_
+instance Compare D8 D4 GT_
+instance Compare D8 D5 GT_
+instance Compare D8 D6 GT_
+instance Compare D8 D7 GT_
+instance Compare D8 D8 EQ_
+instance Compare D8 D9 LT_
+instance NatNE0_ (y:.dy) => Compare D8 (y:.dy) LT_
+instance Compare D9 D0 GT_
+instance Compare D9 D1 GT_
+instance Compare D9 D2 GT_
+instance Compare D9 D3 GT_
+instance Compare D9 D4 GT_
+instance Compare D9 D5 GT_
+instance Compare D9 D6 GT_
+instance Compare D9 D7 GT_
+instance Compare D9 D8 GT_
+instance Compare D9 D9 EQ_
+instance NatNE0_ (y:.dy) => Compare D9 (y:.dy) LT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D0 GT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D1 GT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D2 GT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D3 GT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D4 GT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D5 GT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D6 GT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D7 GT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D8 GT_
+instance NatNE0_ (x:.dx) => Compare (x:.dx) D9 GT_
+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
+
+compare :: Compare x y r => Proxy x -> Proxy y -> Proxy r
+compare _ _ = Proxy
+{-# INLINE compare #-}
+
+
+-- BUG: is this still an optimization now that there's a combinatorial explosion?
+-- | Assert that @x <= y@. This is a popular constraint, so we
+-- implement it specially. We could have said that @Add n x y =>
+-- NatLE x y@, but the following inductive definition is a bit
+-- more optimal.
+class (Nat_ x, Nat_ y) => NatLE x y
+instance NatLE D0 D0
+instance NatLE D0 D1
+instance NatLE D0 D2
+instance NatLE D0 D3
+instance NatLE D0 D4
+instance NatLE D0 D5
+instance NatLE D0 D6
+instance NatLE D0 D7
+instance NatLE D0 D8
+instance NatLE D0 D9
+instance NatNE0_ (y:.dy) => NatLE D0 (y:.dy)
+instance NatLE D1 D1
+instance NatLE D1 D2
+instance NatLE D1 D3
+instance NatLE D1 D4
+instance NatLE D1 D5
+instance NatLE D1 D6
+instance NatLE D1 D7
+instance NatLE D1 D8
+instance NatLE D1 D9
+instance NatNE0_ (y:.dy) => NatLE D1 (y:.dy)
+instance NatLE D2 D2
+instance NatLE D2 D3
+instance NatLE D2 D4
+instance NatLE D2 D5
+instance NatLE D2 D6
+instance NatLE D2 D7
+instance NatLE D2 D8
+instance NatLE D2 D9
+instance NatNE0_ (y:.dy) => NatLE D2 (y:.dy)
+instance NatLE D3 D3
+instance NatLE D3 D4
+instance NatLE D3 D5
+instance NatLE D3 D6
+instance NatLE D3 D7
+instance NatLE D3 D8
+instance NatLE D3 D9
+instance NatNE0_ (y:.dy) => NatLE D3 (y:.dy)
+instance NatLE D4 D4
+instance NatLE D4 D5
+instance NatLE D4 D6
+instance NatLE D4 D7
+instance NatLE D4 D8
+instance NatLE D4 D9
+instance NatNE0_ (y:.dy) => NatLE D4 (y:.dy)
+instance NatLE D5 D5
+instance NatLE D5 D6
+instance NatLE D5 D7
+instance NatLE D5 D8
+instance NatLE D5 D9
+instance NatNE0_ (y:.dy) => NatLE D5 (y:.dy)
+instance NatLE D6 D6
+instance NatLE D6 D7
+instance NatLE D6 D8
+instance NatLE D6 D9
+instance NatNE0_ (y:.dy) => NatLE D6 (y:.dy)
+instance NatLE D7 D7
+instance NatLE D7 D8
+instance NatLE D7 D9
+instance NatNE0_ (y:.dy) => NatLE D7 (y:.dy)
+instance NatLE D8 D8
+instance NatLE D8 D9
+instance NatNE0_ (y:.dy) => NatLE D8 (y:.dy)
+instance NatLE D9 D9
+instance NatNE0_ (y:.dy) => NatLE D9 (y:.dy)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D0)
+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:.D2)
+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:.D4)
+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:.D6)
+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:.D8)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D9)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D1) (y:.D0)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D1)
+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:.D3)
+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:.D5)
+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:.D7)
+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:.D9)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D2) (y:.D0)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D2) (y:.D1)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D2)
+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:.D4)
+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:.D6)
+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:.D8)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D9)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D0)
+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:.D2)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D3)
+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:.D5)
+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:.D7)
+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:.D9)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D0)
+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:.D2)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D3)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D4)
+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:.D6)
+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:.D8)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D9)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D0)
+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:.D2)
+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:.D4)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D5)
+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:.D7)
+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:.D9)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D0)
+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:.D2)
+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:.D4)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D5)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D6)
+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:.D8)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D9)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D0)
+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:.D2)
+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:.D4)
+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:.D6)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D7)
+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:.D9)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D0)
+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:.D2)
+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:.D4)
+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:.D6)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D7)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D8) (y:.D8)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D8) (y:.D9)
+instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D0)
+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:.D2)
+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:.D4)
+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:.D6)
+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:.D8)
+instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D9) (y:.D9)
+
+
+-- | N.B., this will be ill-typed if @x@ is greater than @y@.
+assert_NatLE :: NatLE x y => Proxy x -> Proxy y -> ()
+assert_NatLE Proxy Proxy = ()
+
+
+-- | Assert that @x < y@. This is just a shorthand for @x <= pred y@.
+class (Nat_ x, NatNE0_ y) => NatLT x y
+instance (Succ y' y, NatLE x y') => NatLT x y
+
+
+-- | Choose the larger of @x@ and @y@ according to the order @r@.
+class Max_ x y r z | x y r -> z
+instance Max_ x y LT_ y
+instance Max_ x y EQ_ y -- doesn't matter which we pick
+instance Max_ x y GT_ x
+
+-- | Choose the larger of @x@ and @y@.
+max :: (Compare x y r, Max_ x y r z) => Proxy x -> Proxy y -> Proxy z
+max _ _ = Proxy
+{-# INLINE max #-}
+
+
+-- | Choose the smaller of @x@ and @y@ according to the order @r@.
+class Min_ x y r z | x y r -> z
+instance Min_ x y LT_ x
+instance Min_ x y EQ_ x -- doesn't matter which we pick
+instance Min_ x y GT_ y
+
+-- | Choose the smaller of @x@ and @y@.
+min :: (Compare x y r, Min_ x y r z) => Proxy x -> Proxy y -> Proxy z
+min _ _ = Proxy
+{-# INLINE min #-}
+
+
+{-
+----------------------------------------------------------------
+-- TODO: should we offer @((floor.). div)@, @((ceiling.). div)@, @divMod@ ?
+
+
+-- | Assert that @x * y == z@ where @x > 0@; by structural induction
+-- on the first argument.
+class (NatNE0_ x, Nat_ y, Nat_ z) => Mul_ x y z | x y -> z, x z -> y
+instance Nat_ y => Mul_ B1 y y
+instance (Mul_ x y zh, Snoc zh B0 z) => Mul_ (x:.B0) y z
+instance (Mul_F x y z, Mul_B x y z) => Mul_ (x:.B1) y z
+
+
+-- | Assert that @(2x+1) * y == z@ where @x > 0@.
+class (NatNE0_ x, Nat_ y, Nat_ z) => Mul_F x y z | x y -> z
+instance NatNE0_ x => Mul_F x B0 B0
+instance NatNE0_ x => Mul_F x B1 (x:.B1)
+-- (2x+1) * 2y
+instance (Mul_F x y z, NatNE0_ x, NatNE0_ y, NatNE0_ z)
+ => Mul_F x (y:.B0) (z:.B0)
+-- (2x+1) * (2y+1) = 2*( (2x+1)*y + x ) + 1, y > 0
+instance (Mul_F x y z', Add x z' z, NatNE0_ x, NatNE0_ y, NatNE0_ z)
+ => Mul_F x (y:.B1) (z:.B1)
+
+
+-- | Assert that @(2x+1) * y == z@ where @x > 0@. The functional
+-- dependencies go the other way though.
+class (NatNE0_ x, Nat_ y, Nat_ z) => Mul_B x y z | z x -> y
+instance NatNE0_ x => Mul_B x B0 B0
+-- instance NatNE0_ x => Mul_B x y B1 -- cannot happen
+-- (2x+1) * 2y
+instance (Mul_B x y z, NatNE0_ x, NatNE0_ y, NatNE0_ z)
+ => Mul_B x (y:.B0) (z:.B0)
+-- (2x+1) * (2y+1) = 2*( (2x+1)*y + x ) + 1, y >= 0
+instance (Snoc y B1 yt, Mul_B x y z', Add x z' z, NatNE0_ x, NatNE0_ z)
+ => Mul_B x yt (z:.B1)
+
+
+-- | The multiplication relation with full dependencies. Modes:
+--
+-- > Mul x y (x*y)
+-- > Mul x (z/x) z -- when it's defined.
+-- > Mul (z/y) y z -- when it's defined.
+--
+class (Mul_ x y z, Mul_ y x z) => Mul x y z | x y -> z, x z -> y, y z -> x
+instance (Mul_ x y z, Mul_ y x z) => Mul x y z
+
+mul :: Mul x y z => Proxy x -> Proxy y -> Proxy z
+mul _ _ = Proxy
+{-# INLINE mul #-}
+
+-- | N.B., this will be ill-typed if @z@ is not a multiple of @x@.
+div :: Mul x y z => Proxy z -> Proxy x -> Proxy y
+div _ _ = Proxy
+{-# INLINE div #-}
+
+-- tm1 = mul nat2 nat8
+-- tm2 = reflect $ mul nat8 nat2
+-- tm3 = reflect $ mul (succ nat2) nat2
+-- tm4 = reflect $ mul nat2 (succ nat2)
+-- tm5 = reflect $ mul (succ nat4) (succ nat2)
+-- tm6 = reflect $ mul (succ nat2) (succ nat4)
+-- tm7 = reflect $ div (mul (succ nat8) nat2) (succ nat2) -- 18/3
+
+
+----------------------------------------------------------------
+-- TODO: should we offer @(floor . logBase 2)@ and @(ceiling . logBase 2)@ ?
+-- TODO: general exponentiation/logarithm
+
+
+-- | Power-of-two exponentiation\/logarithm relation. Modes:
+--
+-- > Exp2 x (2^x)
+-- > Exp2 (logBase 2 y) y -- when it's defined.
+--
+class (Nat_ x, NatNE0_ y) => Exp2 x y | x -> y, y -> x
+instance Exp2 B0 B1
+instance Exp2 B1 (B1:.B0)
+instance (Succ x1 (x:.d), Exp2 x1 (y:.B0)) => Exp2 (x:.d) (y:.B0:.B0)
+
+exp2 :: Exp2 x y => Proxy x -> Proxy y
+exp2 _ = Proxy
+{-# INLINE exp2 #-}
+
+-- | N.B., this will be ill-typed if @y@ is not a power of 2.
+log2 :: Exp2 x y => Proxy y -> Proxy x
+log2 _ = Proxy
+{-# INLINE log2 #-}
+
+-- te1 = exp2 (succ (succ nat8))
+-- te1' = reflect $ exp2 (succ (succ nat8))
+-- te2 = reflect $ log2 nat8
+
+
+----------------------------------------------------------------
+-- Do we need the full dependency? If we know x and we know z,
+-- we can't tell what y exactly (except being the multiple of z)
+
+-- | Get the gcd by Euclid's algorithm. Modes:
+--
+-- > GCD x y (gcd x y)
+--
+class (Nat_ x, Nat_ y, Nat_ z) => GCD x y z | x y -> z
+instance Nat_ y => GCD B0 y y
+instance Nat_ y => GCD B1 y B1
+instance (Compare (x:.dx) y r, GCD_ r (x:.dx) y z) => GCD (x:.dx) y z
+
+class (NatNE0_ x, Nat_ y, Nat_ z) => GCD_ r x y z | r x y -> z
+instance NatNE0_ x => GCD_ EQ_ x x x
+instance (GCD y x z, NatNE0_ x) => GCD_ GT_ x y z
+instance (Add x y1 y, GCD y1 x z, NatNE0_ x) => GCD_ LT_ x y z
+
+gcd :: GCD x y z => Proxy x -> Proxy y -> Proxy z
+gcd _ _ = Proxy
+{-# INLINE gcd #-}
+
+-- tg1 = reflect $ gcd nat8 nat8
+-- tg2 = reflect $ gcd nat8 (pred nat8)
+-- tg3 = reflect $ gcd nat8 (pred (pred nat8))
+-- tg4 = reflect $ gcd (pred (pred nat8)) nat8
+-- tg5 = reflect $ gcd nat4 nat8
+-- tg6 = reflect $ gcd (pred nat4) (succ nat8)
+-- tg7 = reflect $ gcd (succ nat8) (pred nat4)
+-}
+
+----------------------------------------------------------------
+----------------------------------------------------------- fin.
diff --git a/src/Data/Number/Fin/TyOrdering.hs b/src/Data/Number/Fin/TyOrdering.hs
new file mode 100644
index 0000000..24ff508
--- /dev/null
+++ b/src/Data/Number/Fin/TyOrdering.hs
@@ -0,0 +1,79 @@
+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+{-# LANGUAGE EmptyDataDecls
+ , DeriveDataTypeable
+ , MultiParamTypeClasses
+ , FlexibleInstances
+ , FunctionalDependencies
+ #-}
+
+{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ >= 701
+{-# LANGUAGE Safe #-}
+#endif
+----------------------------------------------------------------
+-- 2013.05.29
+-- |
+-- Module : Data.Number.Fin.TyOrdering
+-- Copyright : 2012--2013 wren ng thornton,
+-- 2004--2007 Oleg Kiselyov and Chung-chieh Shan
+-- License : BSD3
+-- Maintainer : wren@community.haskell.org
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- Type-level 'Ordering'. This is based on [1], and is intended to
+-- work with [2] (though we use the @reflection@ package for the
+-- actual reification part).
+--
+-- A lot of this also duplicates the functionality in
+-- @HList:Data.HList.FakePrelude@[3], which is (or should be)
+-- obviated by the new data kinds extension. However, we don't want
+-- to restrict this module to the newer versions of GHC which support
+-- data kinds.
+--
+-- [1] Oleg Kiselyov and Chung-chieh Shan. (2007) /Lightweight/
+-- /static resources: Sexy types for embedded and systems/
+-- /programming/. Proc. Trends in Functional Programming.
+-- New York, 2--4 April 2007.
+-- <http://okmij.org/ftp/Haskell/types.html#binary-arithm>
+--
+-- [2] Oleg Kiselyov and Chung-chieh Shan. (2004) /Implicit/
+-- /configurations: or, type classes reflect the values of/
+-- /types/. Proc. ACM SIGPLAN 2004 workshop on Haskell.
+-- Snowbird, Utah, USA, 22 September 2004. pp.33--44.
+-- <http://okmij.org/ftp/Haskell/types.html#Prepose>
+--
+-- [3] <http://hackage.haskell.org/package/HList>
+----------------------------------------------------------------
+module Data.Number.Fin.TyOrdering
+ (
+ -- * Type-level 'Ordering'
+ LT_, EQ_, GT_
+ -- * The 'NCS' class
+ , NCS()
+ ) where
+
+import Data.Typeable (Typeable)
+import Data.Reflection (Reifies(reflect))
+----------------------------------------------------------------
+
+-- Equality and order: the comparison relation
+data LT_ deriving Typeable
+data EQ_ deriving Typeable
+data GT_ deriving Typeable
+
+instance Reifies LT_ Ordering where reflect _ = LT
+instance Reifies EQ_ Ordering where reflect _ = EQ
+instance Reifies GT_ Ordering where reflect _ = GT
+
+
+-- | Compose comparison relations. Perform the first comparison,
+-- and if it's not definitive, then fall through to perform the
+-- second comparison.
+class NCS r1 r2 r3 | r1 r2 -> r3
+instance NCS EQ_ r r
+instance NCS GT_ r GT_
+instance NCS LT_ r LT_
+
+----------------------------------------------------------------
+----------------------------------------------------------- fin.