data-fin (empty) → 0.1.0

raw patch · 14 files changed

+5537/−0 lines, 14 filesdep +QuickCheckdep +basedep +lazysmallchecksetup-changed

Dependencies added: QuickCheck, base, lazysmallcheck, prelude-safeenum, reflection, smallcheck, tagged

Files

• AUTHORS +4/−0
• LICENSE +33/−0
• README +49/−0
• Setup.hs +7/−0
• VERSION +2/−0
• data-fin.cabal +81/−0
• src/Data/Number/Fin.hs +53/−0
• src/Data/Number/Fin/Int16.hs +865/−0
• src/Data/Number/Fin/Int32.hs +865/−0
• src/Data/Number/Fin/Int64.hs +865/−0
• src/Data/Number/Fin/Int8.hs +865/−0
• src/Data/Number/Fin/Integer.hs +828/−0
• src/Data/Number/Fin/TyDecimal.hs +941/−0
• src/Data/Number/Fin/TyOrdering.hs +79/−0

@@ -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.

@@ -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.+

@@ -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.

@@ -0,0 +1,7 @@+#!/usr/bin/env runhaskell++module Main (main) where+import Distribution.Simple++main :: IO ()+main  = defaultMain

@@ -0,0 +1,2 @@+0.1.0 (2013.07.20):+	- Initial release

@@ -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.

@@ -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.

@@ -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.

@@ -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.

@@ -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.

@@ -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.

@@ -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.

@@ -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.

@@ -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.