diff --git a/AUTHORS b/AUTHORS new file mode 100644 --- /dev/null +++ b/AUTHORS @@ -0,0 +1,4 @@ +=== Haskell data-fin package AUTHORS/THANKS file === + +The data-fin package was written by wren ng thornton and is released +under the terms in the LICENSE file. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,33 @@ +Copyright (c) 2012, 2013 wren ng thornton. +ALL RIGHTS RESERVED. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of the copyright holders nor the names of + other contributors may be used to endorse or promote products + derived from this software without specific prior written + permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS +FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, +INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, +BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. + diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,49 @@ +data-fin +======== + +While this package uses complex type machinery, it should be easy +to install. You should be able to use one of the following standard +methods to install it. + + -- With cabal-install and without the source: + $> cabal install data-fin + + -- With cabal-install and with the source already: + $> cd data-fin + $> cabal install + + -- Without cabal-install, but with the source already: + $> cd data-fin + $> runhaskell Setup.hs configure --user + $> runhaskell Setup.hs build + $> runhaskell Setup.hs test + $> runhaskell Setup.hs haddock --hyperlink-source + $> runhaskell Setup.hs copy + $> runhaskell Setup.hs register + +The test step is optional and currently does nothing. The Haddock +step is also optional. + + +Portability +=========== + +While I usually try to keep things as portable as possible, this +package relies on many GHC language extensions. Thus, no claim of +portability ot non-GHC copilers is made. All the required language +extensions are: + +CPP +DeriveDataTypeable +EmptyDataDecls +FlexibleContexts +FlexibleInstances +FunctionalDependencies +MultiParamTypeClasses +Rank2Types +ScopedTypeVariables +TypeOperators +Trustworthy -- GHC >= 7.1 only +UndecidableInstances + +----------------------------------------------------------- fin. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,7 @@ +#!/usr/bin/env runhaskell + +module Main (main) where +import Distribution.Simple + +main :: IO () +main = defaultMain diff --git a/VERSION b/VERSION new file mode 100644 --- /dev/null +++ b/VERSION @@ -0,0 +1,2 @@ +0.1.0 (2013.07.20): + - Initial release diff --git a/data-fin.cabal b/data-fin.cabal new file mode 100644 --- /dev/null +++ b/data-fin.cabal @@ -0,0 +1,81 @@ +---------------------------------------------------------------- +-- wren ng thornton ~ 2013.07.20 +---------------------------------------------------------------- + +-- By and large Cabal >=1.2 is fine; but >= 1.6 gives tested-with: +-- and source-repository:. +Cabal-Version: >= 1.6 +Build-Type: Simple + +Name: data-fin +Version: 0.1.0 +Stability: experimental +Homepage: http://code.haskell.org/~wren/ +Author: wren ng thornton +Maintainer: wren@community.haskell.org +Copyright: Copyright (c) 2012--2013 wren ng thornton +License: BSD3 +License-File: LICENSE + +Category: Data +Synopsis: + Finite totally ordered sets +Description: + Finite totally ordered sets + + +Tested-With: + GHC ==6.12.1 +Extra-source-files: + AUTHORS, README, VERSION +Source-Repository head + Type: darcs + Location: http://community.haskell.org/~wren/data-fin + +---------------------------------------------------------------- +Flag base4 + Default: True + Description: base-4.0 emits "Prelude deprecated" messages in + order to get people to be explicit about which + version of base they use. +Flag splitBase + Default: True + Description: base-3.0 (GHC 6.8) broke out the packages: array, + bytestring, containers, directory, old-locale, + old-time, packedstring, pretty, process, random. +---------------------------------------------------------------- +Library + Hs-Source-Dirs: src + Exposed-Modules: Data.Number.Fin + , Data.Number.Fin.Integer + , Data.Number.Fin.Int8 + , Data.Number.Fin.Int16 + , Data.Number.Fin.Int32 + , Data.Number.Fin.Int64 + -- Data.Number.Fin.Word8 + -- Data.Number.Fin.Word16 + -- Data.Number.Fin.Word32 + -- Data.Number.Fin.Word64 + -- Data.Number.Fin.TyInteger + -- Data.Number.Fin.TyBinary + , Data.Number.Fin.TyDecimal + -- TODO: OfType should be moved elsewhere if we don't use it... + -- Data.Reflection.OfType + Other-Modules: Data.Number.Fin.TyOrdering + + Build-Depends: tagged >= 0.2.3 && < 0.7 + , reflection >= 1.1.6 && < 1.4 + , prelude-safeenum < 0.2 + -- N.B., major smallcheck API break between 0.5 and 0.6 + , smallcheck >= 0.4 && < 0.7 + , lazysmallcheck >= 0.5 && < 0.7 + , QuickCheck >= 2.4.1.1 && < 2.7 + + -- I think this is all that needs doing to get rid of the warnings? + if flag(base4) + Build-Depends: base >= 4 && < 5 + else + Build-Depends: base < 4 + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Data/Number/Fin.hs b/src/Data/Number/Fin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Number/Fin.hs @@ -0,0 +1,53 @@ +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- 2013.07.20 +-- | +-- Module : Data.Number.Fin +-- Copyright : 2012--2013 wren ng thornton +-- License : BSD3 +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : non-portable +-- +-- Newtypes of built-in numeric types for finite subsets of the +-- natural numbers. The default implementation is the newtype of +-- 'Integer', since the type-level numbers are unbounded so this +-- is the most natural. Alternative implementations are available +-- as nearly drop-in replacements. The reason for using modules +-- that provide the same API, rather than using type classes or +-- type families, is that those latter approaches introduce a lot +-- of additional complexity for very little benefit. Using multiple +-- different representations of finite sets in the same module seems +-- like an uncommon use case. Albeit, this impedes writing +-- representation-agnostic functions... +-- +-- When the underlying type can only represent finitely many values, +-- this introduces many corner cases which makes reasoning about +-- programs more difficult. However, the main use case for these +-- finite representations is because we know we'll only be dealing +-- with \"small\" sets, so we'll never actually encounter the corner +-- cases. Thus, this library does not try to handle the corner +-- cases, but rather rules them out with the type system. +-- +-- Many of the operations on finite sets arise from the (skeleton +-- of the) augmented simplex category. For example, the ordinal-sum +-- functor provides the monoidal structure of that category. For +-- more details on the mathematics, see +-- . +---------------------------------------------------------------- +module Data.Number.Fin (module Data.Number.Fin.Integer) where +import Data.Number.Fin.Integer + +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- TODO: offer a newtype of 'Fin' (e.g., @IntMod@) which offers a 'Num' instance for modular arithmetic. + +{- +-- TODO: make Fin a newtype family indexed by the representation type it's a newtype of (e.g., "Data.Number.Fin.Integer" would be @Fin Integer n@)? That would allow people to be polymorphic over the different representations. This would also work great with @Int `Mod` n@ for the modular arithmetic! + +However, note that this means we can't use the @reflection@ package because the 'Reifies' class has a fundep. Unless we always want to reflect as 'Integer' and then do 'fromInteger' everywhere... surely the fundep is there for a reason, but why? We could get around this with the 'OfType' branch of reflection we've been working on... +-} + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Data/Number/Fin/Int16.hs b/src/Data/Number/Fin/Int16.hs new file mode 100644 --- /dev/null +++ b/src/Data/Number/Fin/Int16.hs @@ -0,0 +1,865 @@ +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +{-# LANGUAGE ScopedTypeVariables + , DeriveDataTypeable + , MultiParamTypeClasses + , FlexibleContexts + , CPP + , Rank2Types + , UndecidableInstances + #-} + +#if __GLASGOW_HASKELL__ >= 701 +-- N.B., Data.Proxy and Test.QuickCheck aren't "safe". +{-# LANGUAGE Trustworthy #-} +#endif +---------------------------------------------------------------- +-- 2013.05.29 +-- | +-- Module : Data.Number.Fin.Int16 +-- Copyright : 2012--2013 wren ng thornton +-- License : BSD3 +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : non-portable +-- +-- A newtype of 'Int16' for finite subsets of the natural numbers. +---------------------------------------------------------------- +module Data.Number.Fin.Int16 + ( + -- * @Fin@, finite sets of natural numbers + Fin() + + -- ** Showing types + , showFinType + , showsFinType + + -- ** Convenience functions + , minBoundOf + , maxBoundOf + + -- ** Introduction and elimination + , toFin + , toFinProxy + , toFinCPS + , fromFin + + -- ** Views and coersions + -- *** Weakening and maximum views + , weaken + , weakenLE + , weakenPlus + , maxView + , maxViewLE + + -- *** Widening and the predecessor view + , widen + , widenLE + , widenPlus + , predView + + -- *** The ordinal-sum functor + , plus + , unplus + , fplus + + -- *** Face- and degeneracy-maps + , thin + , thick + -- TODO: is there any way to get equality to work right? + ) where + +import qualified Prelude.SafeEnum as SE +import Data.Int (Int16) +import Data.Ix +import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE, MaxBoundInt16) +import Data.Typeable (Typeable) +import Data.Proxy (Proxy(Proxy)) +import Data.Reflection (Reifies(reflect), reify) +import Control.Monad (liftM) + +import qualified Test.QuickCheck as QC +#if (MIN_VERSION_smallcheck(0,6,0)) +import qualified Test.SmallCheck.Series as SC +#else +import qualified Test.SmallCheck as SC +#endif +import qualified Test.LazySmallCheck as LSC + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- | A finite set of integers @Fin n = { i :: Int16 | 0 <= i < n }@ +-- with the usual ordering. This is typed as if using the standard +-- GADT presentation of @Fin n@, however it is actually implemented +-- by a plain 'Int16'. +newtype Fin n = Fin Int16 + deriving Typeable + -- WART: to give additional constraints (e.g., Nat n) on derived + -- instances (e.g., Show, Eq, Ord), we need to specify the + -- constraints on the data type declaration; however, giving of + -- data-type constraints is deprecated and will be removed from + -- the language... + +{- +-- Some fusion rules for treating newtypes like 'id', or as close +-- as we can. We only have these fire in the last stage so that +-- they don't inhibit the usual list-fusion rules. Hopefully there's +-- nothing important which is defined to not fire at [0]. +-- +-- TODO: add other laws regarding 'id' +{-# RULES +"map Fin" [0] map Fin = unsafeCoerce +"fmap Fin" [0] fmap Fin = unsafeCoerce +"liftM Fin" [0] liftM Fin = unsafeCoerce +"liftA Fin" [0] liftA Fin = unsafeCoerce + #-} +-} + +{- TODO: +-- also: + +-- | 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 ? + + +-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe? +{- -- Agda's version: +data MaxView {n : Nat} : Fin (suc n) -> Set where + theMax : MaxView (fromNat n) + notMax : (i : Fin n) -> MaxView (weaken i) + +maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i +maxView {zero} zero = theMax +maxView {zero} (suc ()) +maxView {suc n} zero = notMax zero +maxView {suc n} (suc i) with maxView i +maxView {suc n} (suc .(fromNat n)) | theMax = theMax +maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i) +-} +-- | The maximum-element view. This strengthens the type by removing +-- the maximum element: +-- +-- > maxView maxBound = Nothing +-- > maxView x = Just x -- morally speaking... +-- +-- The opposite of this function is 'weaken'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +maxView + :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, Succ m n) + => Fin n -> Maybe (Fin m) +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n); so can't use maxViewLE as the implementation. +-- BUG: Could not deduce (NatLE m MaxBoundInt16) from the context (NatLE n MaxBoundInt16, Succ m n); so we have to add it. +maxView = maxView_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@... + maxView_ :: forall m n. (NatLE m MaxBoundInt16) => Fin n -> Maybe (Fin m) + maxView_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxView_ #-} +{-# INLINE maxView #-} + + +-- | A variant of 'maxView' which allows strengthening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @m@ to use. +-- +-- The opposite of this function is 'weakenLE'. When the choice of +-- @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +maxViewLE + :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE m n) + => Fin n -> Maybe (Fin m) +-- BUG: Could not deduce (NatLE m MaxBoundInt16) from the context (NatLE n MaxBoundInt16, Succ m n); so we have to add it. +maxViewLE = maxViewLE_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + maxViewLE_ :: forall m n. (NatLE m MaxBoundInt16) => Fin n -> Maybe (Fin m) + maxViewLE_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxViewLE_ #-} +{-# INLINE maxViewLE #-} + + +-- TODO: maxViewPlus? + + +-- This type-restricted version is a~la Agda. +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'minBound'. That is, +-- +-- > fromFin (weaken x) == fromFin x +-- +-- The opposite of this function is 'maxView'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +weaken :: (NatLE n MaxBoundInt16, Succ m n) => Fin m -> Fin n +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n) +weaken (Fin i) = Fin i +{-# INLINE weaken #-} + + +-- | A variant of 'weaken' which allows weakening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @n@ to use. +-- +-- The opposite of this function is 'maxViewLE'. When the choice +-- of @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +weakenLE :: (NatLE n MaxBoundInt16, NatLE m n) => Fin m -> Fin n +weakenLE (Fin i) = Fin i +{-# INLINE weakenLE #-} + + +---------------------------------------------------------------- +-- | The predecessor view. This strengthens the type by shifting +-- everything down by one: +-- +-- > predView 0 = Nothing +-- > predView x = Just (x-1) -- morally speaking... +-- +-- The opposite of this function is 'widen'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +predView :: (NatLE n MaxBoundInt16, Succ m n) => Fin n -> Maybe (Fin m) +predView (Fin i) + | i <= 0 = Nothing + | otherwise = Just $! Fin (i-1) +{-# INLINE predView #-} + + +-- TODO: predViewLE? predViewPlus? + + +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'maxBound'. That is, we shift everything +-- up by one: +-- +-- > fromFin (widen x) == 1 + fromFin x +-- +-- The opposite of this function is 'predView'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +widen :: (NatLE n MaxBoundInt16, Succ m n) => Fin m -> Fin n +widen (Fin i) = Fin (i+1) +{-# INLINE widen #-} + + +-- | Embed a finite domain into any larger one, keeping the same +-- position relative to 'maxBound'. That is, +-- +-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x +-- > where y = widenLE x +-- +-- Use of this function will generally require an explicit type +-- signature in order to know which @n@ to use. +widenLE + :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE m n) + => Fin m -> Fin n +-- BUG: Could not deduce (NatLE m MaxBoundInt16) from the context (NatLE n MaxBoundInt16, NatLE m n); so we have to add it. +widenLE x@(Fin i) = y + where + y = Fin (maxBoundOf y - maxBoundOf x + i) +{-# INLINE widenLE #-} + + +---------------------------------------------------------------- +-- BUG: Could not deduce (NatLE m o) from the context (Add m n o) +-- | A type-signature variant of 'weakenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE m o@. This is the +-- left half of 'plus'. +weakenPlus :: (NatLE o MaxBoundInt16, Add m n o) => Fin m -> Fin o +weakenPlus (Fin i) = Fin i +{-# INLINE weakenPlus #-} + + +-- BUG: Could not deduce (NatLE n o) from the context (Add m n o) +-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it. +-- | A type-signature variant of 'widenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE n o@. This is the +-- right half of 'plus'. +widenPlus + :: ( NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16 + , Add m n o) + => Fin n -> Fin o +widenPlus = widenPlus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + widenPlus_ :: forall m n o + . (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, Add m n o) + => Fin n -> Fin o + widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y) + {-# INLINE widenPlus_ #-} +{-# INLINE widenPlus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it. +-- | The ordinal-sum functor, on objects. This internalizes the +-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ by +-- placing the image of the summands next to one another in the +-- codomain, thereby preserving the structure of both summands. +plus + :: ( NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16 + , Add m n o) + => Either (Fin m) (Fin n) -> Fin o +plus = either weakenPlus widenPlus +{-# INLINE plus #-} + + +-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it. +-- | The inverse of 'plus'. +unplus + :: ( NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16 + , Add m n o) + => Fin o -> Either (Fin m) (Fin n) +unplus = unplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + unplus_ :: forall m n o. (NatLE m MaxBoundInt16) + => Fin o -> Either (Fin m) (Fin n) + unplus_ (Fin i) + | i <= x = Left $! Fin i + | otherwise = Right $! Fin (i-x) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE unplus_ #-} +{-# INLINE unplus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- BUG: Ditto for (Add m' n' o') +-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it. +-- | The ordinal-sum functor, on morphisms. If we view the maps as +-- bipartite graphs, then the new map is the result of placing the +-- left and right maps next to one another. This is similar to +-- @(+++)@ from "Control.Arrow". +fplus + :: ( NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, NatLE o MaxBoundInt16 + , NatLE m' MaxBoundInt16, NatLE n' MaxBoundInt16, NatLE o' MaxBoundInt16 + , Add m n o, Add m' n' o') + => (Fin m -> Fin m') -- ^ The left morphism + -> (Fin n -> Fin n') -- ^ The right morphism + -> (Fin o -> Fin o') -- ^ +fplus = fplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + fplus_ :: forall m n o m' n' o' + . ( NatLE m MaxBoundInt16 + , NatLE n MaxBoundInt16 + , NatLE o MaxBoundInt16 + , NatLE m' MaxBoundInt16 + , NatLE n' MaxBoundInt16 + , NatLE o' MaxBoundInt16 + , Add m n o, Add m' n' o') + => (Fin m -> Fin m') -> (Fin n -> Fin n') -> Fin o -> Fin o' + fplus_ f g (Fin i) + | i <= x = weakenPlus (f $! Fin i) + | otherwise = widenPlus (g $! Fin (i-x)) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE fplus_ #-} +{-# INLINE fplus #-} + + +-- TODO: (Fin m, Fin n) <-> Fin (Times m n) + +---------------------------------------------------------------- +{- -- Agda's version: +thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n) +thin zero j = suc j +thin (suc i) zero = zero +thin (suc i) (suc j) = suc (thin i j) +-} +-- | The \"face maps\" for @Fin@ viewed as the standard simplices +-- (aka: the thinning view). Traditionally spelled with delta or +-- epsilon. For each @i@, it is the unique injective monotonic map +-- that skips @i@. That is, +-- +-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thin i j /= i +-- +thin :: (NatLE n MaxBoundInt16, Succ m n) => Fin n -> Fin m -> Fin n +thin i j + | weaken j < i = weaken j + | otherwise = succ (weaken j) +{-# INLINE thin #-} + + +-- BUG: Could not deduce (NatLE m MaxBoundInt16),...; so we have to add it. +-- | The \"degeneracy maps\" for @Fin@ viewed as the standard +-- simplices. Traditionally spelled with sigma or eta. For each +-- @i@, it is the unique surjective monotonic map that covers @i@ +-- twice. That is, +-- +-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thick i (i+1) == i +-- +thick + :: (NatLE m MaxBoundInt16, NatLE n MaxBoundInt16, Succ m n) + => Fin m -> Fin n -> Fin m +thick i j = + case maxView (if j <= weaken i then j else pred j) of + Just j' -> j' + Nothing -> _thick_impossible +{-# INLINE thick #-} + + + +{- +-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne? +-- The non zero view, which is used for defining compare... +data NonEmptyView : {n : Nat} -> Fin n -> Set where + ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i + +nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i +nonEmpty zero = ne +nonEmpty (suc _) = ne + + +data EqView : {n : Nat} -> Fin n -> Fin n -> Set where + equal : {n : Nat}{i : Fin n} -> EqView i i + notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j) + +compare : {n : Nat}(i j : Fin n) -> EqView i j +compare zero zero = equal +compare zero (suc j) = notequal j +compare (suc i) zero with nonEmpty i +... | ne = notequal zero +compare (suc i) (suc j) with compare i j +compare (suc i) (suc .i) | equal = equal +compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j) +-} + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- Error messages + +__ :: a +__ = error "Data.Number.Fin.Int16: attempted to evaluate type token" +{-# NOINLINE __ #-} +-- TODO: use extensible-exceptions instead of 'error' +-- TODO: use Proxy instead of these undefined values... + +_thick_impossible :: a +_thick_impossible = + error "Data.Number.Fin.Int16.thick: the impossible happened" +{-# NOINLINE _thick_impossible #-} +-- TODO: use extensible-exceptions instead of 'error' + +_succ_maxBound :: String -> a +_succ_maxBound ty = + error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound" +{-# NOINLINE _succ_maxBound #-} +-- TODO: is there an extensible-exception for this? + +_pred_minBound :: String -> a +_pred_minBound ty = + error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound" +{-# NOINLINE _pred_minBound #-} +-- TODO: is there an extensible-exception for this? + +_toEnum_OOR :: String -> a +_toEnum_OOR ty = + error $ "Enum.toEnum{"++ty++"}: argument out of range" +{-# NOINLINE _toEnum_OOR #-} +-- TODO: is there an extensible-exception for this? + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Data/Number/Fin/Int32.hs b/src/Data/Number/Fin/Int32.hs new file mode 100644 --- /dev/null +++ b/src/Data/Number/Fin/Int32.hs @@ -0,0 +1,865 @@ +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +{-# LANGUAGE ScopedTypeVariables + , DeriveDataTypeable + , MultiParamTypeClasses + , FlexibleContexts + , CPP + , Rank2Types + , UndecidableInstances + #-} + +#if __GLASGOW_HASKELL__ >= 701 +-- N.B., Data.Proxy and Test.QuickCheck aren't "safe". +{-# LANGUAGE Trustworthy #-} +#endif +---------------------------------------------------------------- +-- 2013.05.29 +-- | +-- Module : Data.Number.Fin.Int32 +-- Copyright : 2012--2013 wren ng thornton +-- License : BSD3 +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : non-portable +-- +-- A newtype of 'Int32' for finite subsets of the natural numbers. +---------------------------------------------------------------- +module Data.Number.Fin.Int32 + ( + -- * @Fin@, finite sets of natural numbers + Fin() + + -- ** Showing types + , showFinType + , showsFinType + + -- ** Convenience functions + , minBoundOf + , maxBoundOf + + -- ** Introduction and elimination + , toFin + , toFinProxy + , toFinCPS + , fromFin + + -- ** Views and coersions + -- *** Weakening and maximum views + , weaken + , weakenLE + , weakenPlus + , maxView + , maxViewLE + + -- *** Widening and the predecessor view + , widen + , widenLE + , widenPlus + , predView + + -- *** The ordinal-sum functor + , plus + , unplus + , fplus + + -- *** Face- and degeneracy-maps + , thin + , thick + -- TODO: is there any way to get equality to work right? + ) where + +import qualified Prelude.SafeEnum as SE +import Data.Int (Int32) +import Data.Ix +import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE, MaxBoundInt32) +import Data.Typeable (Typeable) +import Data.Proxy (Proxy(Proxy)) +import Data.Reflection (Reifies(reflect), reify) +import Control.Monad (liftM) + +import qualified Test.QuickCheck as QC +#if (MIN_VERSION_smallcheck(0,6,0)) +import qualified Test.SmallCheck.Series as SC +#else +import qualified Test.SmallCheck as SC +#endif +import qualified Test.LazySmallCheck as LSC + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- | A finite set of integers @Fin n = { i :: Int32 | 0 <= i < n }@ +-- with the usual ordering. This is typed as if using the standard +-- GADT presentation of @Fin n@, however it is actually implemented +-- by a plain 'Int32'. +newtype Fin n = Fin Int32 + deriving Typeable + -- WART: to give additional constraints (e.g., Nat n) on derived + -- instances (e.g., Show, Eq, Ord), we need to specify the + -- constraints on the data type declaration; however, giving of + -- data-type constraints is deprecated and will be removed from + -- the language... + +{- +-- Some fusion rules for treating newtypes like 'id', or as close +-- as we can. We only have these fire in the last stage so that +-- they don't inhibit the usual list-fusion rules. Hopefully there's +-- nothing important which is defined to not fire at [0]. +-- +-- TODO: add other laws regarding 'id' +{-# RULES +"map Fin" [0] map Fin = unsafeCoerce +"fmap Fin" [0] fmap Fin = unsafeCoerce +"liftM Fin" [0] liftM Fin = unsafeCoerce +"liftA Fin" [0] liftA Fin = unsafeCoerce + #-} +-} + +{- TODO: +-- also: + +-- | 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 ? + + +-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe? +{- -- Agda's version: +data MaxView {n : Nat} : Fin (suc n) -> Set where + theMax : MaxView (fromNat n) + notMax : (i : Fin n) -> MaxView (weaken i) + +maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i +maxView {zero} zero = theMax +maxView {zero} (suc ()) +maxView {suc n} zero = notMax zero +maxView {suc n} (suc i) with maxView i +maxView {suc n} (suc .(fromNat n)) | theMax = theMax +maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i) +-} +-- | The maximum-element view. This strengthens the type by removing +-- the maximum element: +-- +-- > maxView maxBound = Nothing +-- > maxView x = Just x -- morally speaking... +-- +-- The opposite of this function is 'weaken'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +maxView + :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, Succ m n) + => Fin n -> Maybe (Fin m) +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n); so can't use maxViewLE as the implementation. +-- BUG: Could not deduce (NatLE m MaxBoundInt32) from the context (NatLE n MaxBoundInt32, Succ m n); so we have to add it. +maxView = maxView_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@... + maxView_ :: forall m n. (NatLE m MaxBoundInt32) => Fin n -> Maybe (Fin m) + maxView_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxView_ #-} +{-# INLINE maxView #-} + + +-- | A variant of 'maxView' which allows strengthening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @m@ to use. +-- +-- The opposite of this function is 'weakenLE'. When the choice of +-- @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +maxViewLE + :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE m n) + => Fin n -> Maybe (Fin m) +-- BUG: Could not deduce (NatLE m MaxBoundInt32) from the context (NatLE n MaxBoundInt32, Succ m n); so we have to add it. +maxViewLE = maxViewLE_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + maxViewLE_ :: forall m n. (NatLE m MaxBoundInt32) => Fin n -> Maybe (Fin m) + maxViewLE_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxViewLE_ #-} +{-# INLINE maxViewLE #-} + + +-- TODO: maxViewPlus? + + +-- This type-restricted version is a~la Agda. +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'minBound'. That is, +-- +-- > fromFin (weaken x) == fromFin x +-- +-- The opposite of this function is 'maxView'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +weaken :: (NatLE n MaxBoundInt32, Succ m n) => Fin m -> Fin n +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n) +weaken (Fin i) = Fin i +{-# INLINE weaken #-} + + +-- | A variant of 'weaken' which allows weakening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @n@ to use. +-- +-- The opposite of this function is 'maxViewLE'. When the choice +-- of @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +weakenLE :: (NatLE n MaxBoundInt32, NatLE m n) => Fin m -> Fin n +weakenLE (Fin i) = Fin i +{-# INLINE weakenLE #-} + + +---------------------------------------------------------------- +-- | The predecessor view. This strengthens the type by shifting +-- everything down by one: +-- +-- > predView 0 = Nothing +-- > predView x = Just (x-1) -- morally speaking... +-- +-- The opposite of this function is 'widen'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +predView :: (NatLE n MaxBoundInt32, Succ m n) => Fin n -> Maybe (Fin m) +predView (Fin i) + | i <= 0 = Nothing + | otherwise = Just $! Fin (i-1) +{-# INLINE predView #-} + + +-- TODO: predViewLE? predViewPlus? + + +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'maxBound'. That is, we shift everything +-- up by one: +-- +-- > fromFin (widen x) == 1 + fromFin x +-- +-- The opposite of this function is 'predView'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +widen :: (NatLE n MaxBoundInt32, Succ m n) => Fin m -> Fin n +widen (Fin i) = Fin (i+1) +{-# INLINE widen #-} + + +-- | Embed a finite domain into any larger one, keeping the same +-- position relative to 'maxBound'. That is, +-- +-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x +-- > where y = widenLE x +-- +-- Use of this function will generally require an explicit type +-- signature in order to know which @n@ to use. +widenLE + :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE m n) + => Fin m -> Fin n +-- BUG: Could not deduce (NatLE m MaxBoundInt32) from the context (NatLE n MaxBoundInt32, NatLE m n); so we have to add it. +widenLE x@(Fin i) = y + where + y = Fin (maxBoundOf y - maxBoundOf x + i) +{-# INLINE widenLE #-} + + +---------------------------------------------------------------- +-- BUG: Could not deduce (NatLE m o) from the context (Add m n o) +-- | A type-signature variant of 'weakenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE m o@. This is the +-- left half of 'plus'. +weakenPlus :: (NatLE o MaxBoundInt32, Add m n o) => Fin m -> Fin o +weakenPlus (Fin i) = Fin i +{-# INLINE weakenPlus #-} + + +-- BUG: Could not deduce (NatLE n o) from the context (Add m n o) +-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it. +-- | A type-signature variant of 'widenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE n o@. This is the +-- right half of 'plus'. +widenPlus + :: ( NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32 + , Add m n o) + => Fin n -> Fin o +widenPlus = widenPlus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + widenPlus_ :: forall m n o + . (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, Add m n o) + => Fin n -> Fin o + widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y) + {-# INLINE widenPlus_ #-} +{-# INLINE widenPlus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it. +-- | The ordinal-sum functor, on objects. This internalizes the +-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ by +-- placing the image of the summands next to one another in the +-- codomain, thereby preserving the structure of both summands. +plus + :: ( NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32 + , Add m n o) + => Either (Fin m) (Fin n) -> Fin o +plus = either weakenPlus widenPlus +{-# INLINE plus #-} + + +-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it. +-- | The inverse of 'plus'. +unplus + :: ( NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32 + , Add m n o) + => Fin o -> Either (Fin m) (Fin n) +unplus = unplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + unplus_ :: forall m n o. (NatLE m MaxBoundInt32) + => Fin o -> Either (Fin m) (Fin n) + unplus_ (Fin i) + | i <= x = Left $! Fin i + | otherwise = Right $! Fin (i-x) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE unplus_ #-} +{-# INLINE unplus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- BUG: Ditto for (Add m' n' o') +-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it. +-- | The ordinal-sum functor, on morphisms. If we view the maps as +-- bipartite graphs, then the new map is the result of placing the +-- left and right maps next to one another. This is similar to +-- @(+++)@ from "Control.Arrow". +fplus + :: ( NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, NatLE o MaxBoundInt32 + , NatLE m' MaxBoundInt32, NatLE n' MaxBoundInt32, NatLE o' MaxBoundInt32 + , Add m n o, Add m' n' o') + => (Fin m -> Fin m') -- ^ The left morphism + -> (Fin n -> Fin n') -- ^ The right morphism + -> (Fin o -> Fin o') -- ^ +fplus = fplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + fplus_ :: forall m n o m' n' o' + . ( NatLE m MaxBoundInt32 + , NatLE n MaxBoundInt32 + , NatLE o MaxBoundInt32 + , NatLE m' MaxBoundInt32 + , NatLE n' MaxBoundInt32 + , NatLE o' MaxBoundInt32 + , Add m n o, Add m' n' o') + => (Fin m -> Fin m') -> (Fin n -> Fin n') -> Fin o -> Fin o' + fplus_ f g (Fin i) + | i <= x = weakenPlus (f $! Fin i) + | otherwise = widenPlus (g $! Fin (i-x)) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE fplus_ #-} +{-# INLINE fplus #-} + + +-- TODO: (Fin m, Fin n) <-> Fin (Times m n) + +---------------------------------------------------------------- +{- -- Agda's version: +thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n) +thin zero j = suc j +thin (suc i) zero = zero +thin (suc i) (suc j) = suc (thin i j) +-} +-- | The \"face maps\" for @Fin@ viewed as the standard simplices +-- (aka: the thinning view). Traditionally spelled with delta or +-- epsilon. For each @i@, it is the unique injective monotonic map +-- that skips @i@. That is, +-- +-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thin i j /= i +-- +thin :: (NatLE n MaxBoundInt32, Succ m n) => Fin n -> Fin m -> Fin n +thin i j + | weaken j < i = weaken j + | otherwise = succ (weaken j) +{-# INLINE thin #-} + + +-- BUG: Could not deduce (NatLE m MaxBoundInt32),...; so we have to add it. +-- | The \"degeneracy maps\" for @Fin@ viewed as the standard +-- simplices. Traditionally spelled with sigma or eta. For each +-- @i@, it is the unique surjective monotonic map that covers @i@ +-- twice. That is, +-- +-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thick i (i+1) == i +-- +thick + :: (NatLE m MaxBoundInt32, NatLE n MaxBoundInt32, Succ m n) + => Fin m -> Fin n -> Fin m +thick i j = + case maxView (if j <= weaken i then j else pred j) of + Just j' -> j' + Nothing -> _thick_impossible +{-# INLINE thick #-} + + + +{- +-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne? +-- The non zero view, which is used for defining compare... +data NonEmptyView : {n : Nat} -> Fin n -> Set where + ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i + +nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i +nonEmpty zero = ne +nonEmpty (suc _) = ne + + +data EqView : {n : Nat} -> Fin n -> Fin n -> Set where + equal : {n : Nat}{i : Fin n} -> EqView i i + notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j) + +compare : {n : Nat}(i j : Fin n) -> EqView i j +compare zero zero = equal +compare zero (suc j) = notequal j +compare (suc i) zero with nonEmpty i +... | ne = notequal zero +compare (suc i) (suc j) with compare i j +compare (suc i) (suc .i) | equal = equal +compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j) +-} + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- Error messages + +__ :: a +__ = error "Data.Number.Fin.Int32: attempted to evaluate type token" +{-# NOINLINE __ #-} +-- TODO: use extensible-exceptions instead of 'error' +-- TODO: use Proxy instead of these undefined values... + +_thick_impossible :: a +_thick_impossible = + error "Data.Number.Fin.Int32.thick: the impossible happened" +{-# NOINLINE _thick_impossible #-} +-- TODO: use extensible-exceptions instead of 'error' + +_succ_maxBound :: String -> a +_succ_maxBound ty = + error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound" +{-# NOINLINE _succ_maxBound #-} +-- TODO: is there an extensible-exception for this? + +_pred_minBound :: String -> a +_pred_minBound ty = + error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound" +{-# NOINLINE _pred_minBound #-} +-- TODO: is there an extensible-exception for this? + +_toEnum_OOR :: String -> a +_toEnum_OOR ty = + error $ "Enum.toEnum{"++ty++"}: argument out of range" +{-# NOINLINE _toEnum_OOR #-} +-- TODO: is there an extensible-exception for this? + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Data/Number/Fin/Int64.hs b/src/Data/Number/Fin/Int64.hs new file mode 100644 --- /dev/null +++ b/src/Data/Number/Fin/Int64.hs @@ -0,0 +1,865 @@ +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +{-# LANGUAGE ScopedTypeVariables + , DeriveDataTypeable + , MultiParamTypeClasses + , FlexibleContexts + , CPP + , Rank2Types + , UndecidableInstances + #-} + +#if __GLASGOW_HASKELL__ >= 701 +-- N.B., Data.Proxy and Test.QuickCheck aren't "safe". +{-# LANGUAGE Trustworthy #-} +#endif +---------------------------------------------------------------- +-- 2013.05.29 +-- | +-- Module : Data.Number.Fin.Int64 +-- Copyright : 2012--2013 wren ng thornton +-- License : BSD3 +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : non-portable +-- +-- A newtype of 'Int64' for finite subsets of the natural numbers. +---------------------------------------------------------------- +module Data.Number.Fin.Int64 + ( + -- * @Fin@, finite sets of natural numbers + Fin() + + -- ** Showing types + , showFinType + , showsFinType + + -- ** Convenience functions + , minBoundOf + , maxBoundOf + + -- ** Introduction and elimination + , toFin + , toFinProxy + , toFinCPS + , fromFin + + -- ** Views and coersions + -- *** Weakening and maximum views + , weaken + , weakenLE + , weakenPlus + , maxView + , maxViewLE + + -- *** Widening and the predecessor view + , widen + , widenLE + , widenPlus + , predView + + -- *** The ordinal-sum functor + , plus + , unplus + , fplus + + -- *** Face- and degeneracy-maps + , thin + , thick + -- TODO: is there any way to get equality to work right? + ) where + +import qualified Prelude.SafeEnum as SE +import Data.Int (Int64) +import Data.Ix +import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE, MaxBoundInt64) +import Data.Typeable (Typeable) +import Data.Proxy (Proxy(Proxy)) +import Data.Reflection (Reifies(reflect), reify) +import Control.Monad (liftM) + +import qualified Test.QuickCheck as QC +#if (MIN_VERSION_smallcheck(0,6,0)) +import qualified Test.SmallCheck.Series as SC +#else +import qualified Test.SmallCheck as SC +#endif +import qualified Test.LazySmallCheck as LSC + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- | A finite set of integers @Fin n = { i :: Int64 | 0 <= i < n }@ +-- with the usual ordering. This is typed as if using the standard +-- GADT presentation of @Fin n@, however it is actually implemented +-- by a plain 'Int64'. +newtype Fin n = Fin Int64 + deriving Typeable + -- WART: to give additional constraints (e.g., Nat n) on derived + -- instances (e.g., Show, Eq, Ord), we need to specify the + -- constraints on the data type declaration; however, giving of + -- data-type constraints is deprecated and will be removed from + -- the language... + +{- +-- Some fusion rules for treating newtypes like 'id', or as close +-- as we can. We only have these fire in the last stage so that +-- they don't inhibit the usual list-fusion rules. Hopefully there's +-- nothing important which is defined to not fire at [0]. +-- +-- TODO: add other laws regarding 'id' +{-# RULES +"map Fin" [0] map Fin = unsafeCoerce +"fmap Fin" [0] fmap Fin = unsafeCoerce +"liftM Fin" [0] liftM Fin = unsafeCoerce +"liftA Fin" [0] liftA Fin = unsafeCoerce + #-} +-} + +{- TODO: +-- also: + +-- | 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 ? + + +-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe? +{- -- Agda's version: +data MaxView {n : Nat} : Fin (suc n) -> Set where + theMax : MaxView (fromNat n) + notMax : (i : Fin n) -> MaxView (weaken i) + +maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i +maxView {zero} zero = theMax +maxView {zero} (suc ()) +maxView {suc n} zero = notMax zero +maxView {suc n} (suc i) with maxView i +maxView {suc n} (suc .(fromNat n)) | theMax = theMax +maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i) +-} +-- | The maximum-element view. This strengthens the type by removing +-- the maximum element: +-- +-- > maxView maxBound = Nothing +-- > maxView x = Just x -- morally speaking... +-- +-- The opposite of this function is 'weaken'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +maxView + :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, Succ m n) + => Fin n -> Maybe (Fin m) +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n); so can't use maxViewLE as the implementation. +-- BUG: Could not deduce (NatLE m MaxBoundInt64) from the context (NatLE n MaxBoundInt64, Succ m n); so we have to add it. +maxView = maxView_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@... + maxView_ :: forall m n. (NatLE m MaxBoundInt64) => Fin n -> Maybe (Fin m) + maxView_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxView_ #-} +{-# INLINE maxView #-} + + +-- | A variant of 'maxView' which allows strengthening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @m@ to use. +-- +-- The opposite of this function is 'weakenLE'. When the choice of +-- @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +maxViewLE + :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE m n) + => Fin n -> Maybe (Fin m) +-- BUG: Could not deduce (NatLE m MaxBoundInt64) from the context (NatLE n MaxBoundInt64, Succ m n); so we have to add it. +maxViewLE = maxViewLE_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + maxViewLE_ :: forall m n. (NatLE m MaxBoundInt64) => Fin n -> Maybe (Fin m) + maxViewLE_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxViewLE_ #-} +{-# INLINE maxViewLE #-} + + +-- TODO: maxViewPlus? + + +-- This type-restricted version is a~la Agda. +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'minBound'. That is, +-- +-- > fromFin (weaken x) == fromFin x +-- +-- The opposite of this function is 'maxView'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +weaken :: (NatLE n MaxBoundInt64, Succ m n) => Fin m -> Fin n +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n) +weaken (Fin i) = Fin i +{-# INLINE weaken #-} + + +-- | A variant of 'weaken' which allows weakening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @n@ to use. +-- +-- The opposite of this function is 'maxViewLE'. When the choice +-- of @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +weakenLE :: (NatLE n MaxBoundInt64, NatLE m n) => Fin m -> Fin n +weakenLE (Fin i) = Fin i +{-# INLINE weakenLE #-} + + +---------------------------------------------------------------- +-- | The predecessor view. This strengthens the type by shifting +-- everything down by one: +-- +-- > predView 0 = Nothing +-- > predView x = Just (x-1) -- morally speaking... +-- +-- The opposite of this function is 'widen'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +predView :: (NatLE n MaxBoundInt64, Succ m n) => Fin n -> Maybe (Fin m) +predView (Fin i) + | i <= 0 = Nothing + | otherwise = Just $! Fin (i-1) +{-# INLINE predView #-} + + +-- TODO: predViewLE? predViewPlus? + + +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'maxBound'. That is, we shift everything +-- up by one: +-- +-- > fromFin (widen x) == 1 + fromFin x +-- +-- The opposite of this function is 'predView'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +widen :: (NatLE n MaxBoundInt64, Succ m n) => Fin m -> Fin n +widen (Fin i) = Fin (i+1) +{-# INLINE widen #-} + + +-- | Embed a finite domain into any larger one, keeping the same +-- position relative to 'maxBound'. That is, +-- +-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x +-- > where y = widenLE x +-- +-- Use of this function will generally require an explicit type +-- signature in order to know which @n@ to use. +widenLE + :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE m n) + => Fin m -> Fin n +-- BUG: Could not deduce (NatLE m MaxBoundInt64) from the context (NatLE n MaxBoundInt64, NatLE m n); so we have to add it. +widenLE x@(Fin i) = y + where + y = Fin (maxBoundOf y - maxBoundOf x + i) +{-# INLINE widenLE #-} + + +---------------------------------------------------------------- +-- BUG: Could not deduce (NatLE m o) from the context (Add m n o) +-- | A type-signature variant of 'weakenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE m o@. This is the +-- left half of 'plus'. +weakenPlus :: (NatLE o MaxBoundInt64, Add m n o) => Fin m -> Fin o +weakenPlus (Fin i) = Fin i +{-# INLINE weakenPlus #-} + + +-- BUG: Could not deduce (NatLE n o) from the context (Add m n o) +-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it. +-- | A type-signature variant of 'widenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE n o@. This is the +-- right half of 'plus'. +widenPlus + :: ( NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64 + , Add m n o) + => Fin n -> Fin o +widenPlus = widenPlus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + widenPlus_ :: forall m n o + . (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, Add m n o) + => Fin n -> Fin o + widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y) + {-# INLINE widenPlus_ #-} +{-# INLINE widenPlus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it. +-- | The ordinal-sum functor, on objects. This internalizes the +-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ by +-- placing the image of the summands next to one another in the +-- codomain, thereby preserving the structure of both summands. +plus + :: ( NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64 + , Add m n o) + => Either (Fin m) (Fin n) -> Fin o +plus = either weakenPlus widenPlus +{-# INLINE plus #-} + + +-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it. +-- | The inverse of 'plus'. +unplus + :: ( NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64 + , Add m n o) + => Fin o -> Either (Fin m) (Fin n) +unplus = unplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + unplus_ :: forall m n o. (NatLE m MaxBoundInt64) + => Fin o -> Either (Fin m) (Fin n) + unplus_ (Fin i) + | i <= x = Left $! Fin i + | otherwise = Right $! Fin (i-x) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE unplus_ #-} +{-# INLINE unplus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- BUG: Ditto for (Add m' n' o') +-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it. +-- | The ordinal-sum functor, on morphisms. If we view the maps as +-- bipartite graphs, then the new map is the result of placing the +-- left and right maps next to one another. This is similar to +-- @(+++)@ from "Control.Arrow". +fplus + :: ( NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, NatLE o MaxBoundInt64 + , NatLE m' MaxBoundInt64, NatLE n' MaxBoundInt64, NatLE o' MaxBoundInt64 + , Add m n o, Add m' n' o') + => (Fin m -> Fin m') -- ^ The left morphism + -> (Fin n -> Fin n') -- ^ The right morphism + -> (Fin o -> Fin o') -- ^ +fplus = fplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + fplus_ :: forall m n o m' n' o' + . ( NatLE m MaxBoundInt64 + , NatLE n MaxBoundInt64 + , NatLE o MaxBoundInt64 + , NatLE m' MaxBoundInt64 + , NatLE n' MaxBoundInt64 + , NatLE o' MaxBoundInt64 + , Add m n o, Add m' n' o') + => (Fin m -> Fin m') -> (Fin n -> Fin n') -> Fin o -> Fin o' + fplus_ f g (Fin i) + | i <= x = weakenPlus (f $! Fin i) + | otherwise = widenPlus (g $! Fin (i-x)) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE fplus_ #-} +{-# INLINE fplus #-} + + +-- TODO: (Fin m, Fin n) <-> Fin (Times m n) + +---------------------------------------------------------------- +{- -- Agda's version: +thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n) +thin zero j = suc j +thin (suc i) zero = zero +thin (suc i) (suc j) = suc (thin i j) +-} +-- | The \"face maps\" for @Fin@ viewed as the standard simplices +-- (aka: the thinning view). Traditionally spelled with delta or +-- epsilon. For each @i@, it is the unique injective monotonic map +-- that skips @i@. That is, +-- +-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thin i j /= i +-- +thin :: (NatLE n MaxBoundInt64, Succ m n) => Fin n -> Fin m -> Fin n +thin i j + | weaken j < i = weaken j + | otherwise = succ (weaken j) +{-# INLINE thin #-} + + +-- BUG: Could not deduce (NatLE m MaxBoundInt64),...; so we have to add it. +-- | The \"degeneracy maps\" for @Fin@ viewed as the standard +-- simplices. Traditionally spelled with sigma or eta. For each +-- @i@, it is the unique surjective monotonic map that covers @i@ +-- twice. That is, +-- +-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thick i (i+1) == i +-- +thick + :: (NatLE m MaxBoundInt64, NatLE n MaxBoundInt64, Succ m n) + => Fin m -> Fin n -> Fin m +thick i j = + case maxView (if j <= weaken i then j else pred j) of + Just j' -> j' + Nothing -> _thick_impossible +{-# INLINE thick #-} + + + +{- +-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne? +-- The non zero view, which is used for defining compare... +data NonEmptyView : {n : Nat} -> Fin n -> Set where + ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i + +nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i +nonEmpty zero = ne +nonEmpty (suc _) = ne + + +data EqView : {n : Nat} -> Fin n -> Fin n -> Set where + equal : {n : Nat}{i : Fin n} -> EqView i i + notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j) + +compare : {n : Nat}(i j : Fin n) -> EqView i j +compare zero zero = equal +compare zero (suc j) = notequal j +compare (suc i) zero with nonEmpty i +... | ne = notequal zero +compare (suc i) (suc j) with compare i j +compare (suc i) (suc .i) | equal = equal +compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j) +-} + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- Error messages + +__ :: a +__ = error "Data.Number.Fin.Int64: attempted to evaluate type token" +{-# NOINLINE __ #-} +-- TODO: use extensible-exceptions instead of 'error' +-- TODO: use Proxy instead of these undefined values... + +_thick_impossible :: a +_thick_impossible = + error "Data.Number.Fin.Int64.thick: the impossible happened" +{-# NOINLINE _thick_impossible #-} +-- TODO: use extensible-exceptions instead of 'error' + +_succ_maxBound :: String -> a +_succ_maxBound ty = + error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound" +{-# NOINLINE _succ_maxBound #-} +-- TODO: is there an extensible-exception for this? + +_pred_minBound :: String -> a +_pred_minBound ty = + error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound" +{-# NOINLINE _pred_minBound #-} +-- TODO: is there an extensible-exception for this? + +_toEnum_OOR :: String -> a +_toEnum_OOR ty = + error $ "Enum.toEnum{"++ty++"}: argument out of range" +{-# NOINLINE _toEnum_OOR #-} +-- TODO: is there an extensible-exception for this? + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Data/Number/Fin/Int8.hs b/src/Data/Number/Fin/Int8.hs new file mode 100644 --- /dev/null +++ b/src/Data/Number/Fin/Int8.hs @@ -0,0 +1,865 @@ +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +{-# LANGUAGE ScopedTypeVariables + , DeriveDataTypeable + , MultiParamTypeClasses + , FlexibleContexts + , CPP + , Rank2Types + , UndecidableInstances + #-} + +#if __GLASGOW_HASKELL__ >= 701 +-- N.B., Data.Proxy and Test.QuickCheck aren't "safe". +{-# LANGUAGE Trustworthy #-} +#endif +---------------------------------------------------------------- +-- 2013.05.29 +-- | +-- Module : Data.Number.Fin.Int8 +-- Copyright : 2012--2013 wren ng thornton +-- License : BSD3 +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : non-portable +-- +-- A newtype of 'Int8' for finite subsets of the natural numbers. +---------------------------------------------------------------- +module Data.Number.Fin.Int8 + ( + -- * @Fin@, finite sets of natural numbers + Fin() + + -- ** Showing types + , showFinType + , showsFinType + + -- ** Convenience functions + , minBoundOf + , maxBoundOf + + -- ** Introduction and elimination + , toFin + , toFinProxy + , toFinCPS + , fromFin + + -- ** Views and coersions + -- *** Weakening and maximum views + , weaken + , weakenLE + , weakenPlus + , maxView + , maxViewLE + + -- *** Widening and the predecessor view + , widen + , widenLE + , widenPlus + , predView + + -- *** The ordinal-sum functor + , plus + , unplus + , fplus + + -- *** Face- and degeneracy-maps + , thin + , thick + -- TODO: is there any way to get equality to work right? + ) where + +import qualified Prelude.SafeEnum as SE +import Data.Int (Int8) +import Data.Ix +import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE, MaxBoundInt8) +import Data.Typeable (Typeable) +import Data.Proxy (Proxy(Proxy)) +import Data.Reflection (Reifies(reflect), reify) +import Control.Monad (liftM) + +import qualified Test.QuickCheck as QC +#if (MIN_VERSION_smallcheck(0,6,0)) +import qualified Test.SmallCheck.Series as SC +#else +import qualified Test.SmallCheck as SC +#endif +import qualified Test.LazySmallCheck as LSC + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- | A finite set of integers @Fin n = { i :: Int8 | 0 <= i < n }@ +-- with the usual ordering. This is typed as if using the standard +-- GADT presentation of @Fin n@, however it is actually implemented +-- by a plain 'Int8'. +newtype Fin n = Fin Int8 + deriving Typeable + -- WART: to give additional constraints (e.g., Nat n) on derived + -- instances (e.g., Show, Eq, Ord), we need to specify the + -- constraints on the data type declaration; however, giving of + -- data-type constraints is deprecated and will be removed from + -- the language... + +{- +-- Some fusion rules for treating newtypes like 'id', or as close +-- as we can. We only have these fire in the last stage so that +-- they don't inhibit the usual list-fusion rules. Hopefully there's +-- nothing important which is defined to not fire at [0]. +-- +-- TODO: add other laws regarding 'id' +{-# RULES +"map Fin" [0] map Fin = unsafeCoerce +"fmap Fin" [0] fmap Fin = unsafeCoerce +"liftM Fin" [0] liftM Fin = unsafeCoerce +"liftA Fin" [0] liftA Fin = unsafeCoerce + #-} +-} + +{- TODO: +-- also: + +-- | 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 ? + + +-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe? +{- -- Agda's version: +data MaxView {n : Nat} : Fin (suc n) -> Set where + theMax : MaxView (fromNat n) + notMax : (i : Fin n) -> MaxView (weaken i) + +maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i +maxView {zero} zero = theMax +maxView {zero} (suc ()) +maxView {suc n} zero = notMax zero +maxView {suc n} (suc i) with maxView i +maxView {suc n} (suc .(fromNat n)) | theMax = theMax +maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i) +-} +-- | The maximum-element view. This strengthens the type by removing +-- the maximum element: +-- +-- > maxView maxBound = Nothing +-- > maxView x = Just x -- morally speaking... +-- +-- The opposite of this function is 'weaken'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +maxView + :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, Succ m n) + => Fin n -> Maybe (Fin m) +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n); so can't use maxViewLE as the implementation. +-- BUG: Could not deduce (NatLE m MaxBoundInt8) from the context (NatLE n MaxBoundInt8, Succ m n); so we have to add it. +maxView = maxView_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@... + maxView_ :: forall m n. (NatLE m MaxBoundInt8) => Fin n -> Maybe (Fin m) + maxView_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxView_ #-} +{-# INLINE maxView #-} + + +-- | A variant of 'maxView' which allows strengthening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @m@ to use. +-- +-- The opposite of this function is 'weakenLE'. When the choice of +-- @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +maxViewLE + :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE m n) + => Fin n -> Maybe (Fin m) +-- BUG: Could not deduce (NatLE m MaxBoundInt8) from the context (NatLE n MaxBoundInt8, Succ m n); so we have to add it. +maxViewLE = maxViewLE_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + maxViewLE_ :: forall m n. (NatLE m MaxBoundInt8) => Fin n -> Maybe (Fin m) + maxViewLE_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxViewLE_ #-} +{-# INLINE maxViewLE #-} + + +-- TODO: maxViewPlus? + + +-- This type-restricted version is a~la Agda. +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'minBound'. That is, +-- +-- > fromFin (weaken x) == fromFin x +-- +-- The opposite of this function is 'maxView'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +weaken :: (NatLE n MaxBoundInt8, Succ m n) => Fin m -> Fin n +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n) +weaken (Fin i) = Fin i +{-# INLINE weaken #-} + + +-- | A variant of 'weaken' which allows weakening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @n@ to use. +-- +-- The opposite of this function is 'maxViewLE'. When the choice +-- of @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +weakenLE :: (NatLE n MaxBoundInt8, NatLE m n) => Fin m -> Fin n +weakenLE (Fin i) = Fin i +{-# INLINE weakenLE #-} + + +---------------------------------------------------------------- +-- | The predecessor view. This strengthens the type by shifting +-- everything down by one: +-- +-- > predView 0 = Nothing +-- > predView x = Just (x-1) -- morally speaking... +-- +-- The opposite of this function is 'widen'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +predView :: (NatLE n MaxBoundInt8, Succ m n) => Fin n -> Maybe (Fin m) +predView (Fin i) + | i <= 0 = Nothing + | otherwise = Just $! Fin (i-1) +{-# INLINE predView #-} + + +-- TODO: predViewLE? predViewPlus? + + +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'maxBound'. That is, we shift everything +-- up by one: +-- +-- > fromFin (widen x) == 1 + fromFin x +-- +-- The opposite of this function is 'predView'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +widen :: (NatLE n MaxBoundInt8, Succ m n) => Fin m -> Fin n +widen (Fin i) = Fin (i+1) +{-# INLINE widen #-} + + +-- | Embed a finite domain into any larger one, keeping the same +-- position relative to 'maxBound'. That is, +-- +-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x +-- > where y = widenLE x +-- +-- Use of this function will generally require an explicit type +-- signature in order to know which @n@ to use. +widenLE + :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE m n) + => Fin m -> Fin n +-- BUG: Could not deduce (NatLE m MaxBoundInt8) from the context (NatLE n MaxBoundInt8, NatLE m n); so we have to add it. +widenLE x@(Fin i) = y + where + y = Fin (maxBoundOf y - maxBoundOf x + i) +{-# INLINE widenLE #-} + + +---------------------------------------------------------------- +-- BUG: Could not deduce (NatLE m o) from the context (Add m n o) +-- | A type-signature variant of 'weakenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE m o@. This is the +-- left half of 'plus'. +weakenPlus :: (NatLE o MaxBoundInt8, Add m n o) => Fin m -> Fin o +weakenPlus (Fin i) = Fin i +{-# INLINE weakenPlus #-} + + +-- BUG: Could not deduce (NatLE n o) from the context (Add m n o) +-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it. +-- | A type-signature variant of 'widenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE n o@. This is the +-- right half of 'plus'. +widenPlus + :: ( NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8 + , Add m n o) + => Fin n -> Fin o +widenPlus = widenPlus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + widenPlus_ :: forall m n o + . (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, Add m n o) + => Fin n -> Fin o + widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y) + {-# INLINE widenPlus_ #-} +{-# INLINE widenPlus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it. +-- | The ordinal-sum functor, on objects. This internalizes the +-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ by +-- placing the image of the summands next to one another in the +-- codomain, thereby preserving the structure of both summands. +plus + :: ( NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8 + , Add m n o) + => Either (Fin m) (Fin n) -> Fin o +plus = either weakenPlus widenPlus +{-# INLINE plus #-} + + +-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it. +-- | The inverse of 'plus'. +unplus + :: ( NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8 + , Add m n o) + => Fin o -> Either (Fin m) (Fin n) +unplus = unplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + unplus_ :: forall m n o. (NatLE m MaxBoundInt8) + => Fin o -> Either (Fin m) (Fin n) + unplus_ (Fin i) + | i <= x = Left $! Fin i + | otherwise = Right $! Fin (i-x) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE unplus_ #-} +{-# INLINE unplus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- BUG: Ditto for (Add m' n' o') +-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it. +-- | The ordinal-sum functor, on morphisms. If we view the maps as +-- bipartite graphs, then the new map is the result of placing the +-- left and right maps next to one another. This is similar to +-- @(+++)@ from "Control.Arrow". +fplus + :: ( NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, NatLE o MaxBoundInt8 + , NatLE m' MaxBoundInt8, NatLE n' MaxBoundInt8, NatLE o' MaxBoundInt8 + , Add m n o, Add m' n' o') + => (Fin m -> Fin m') -- ^ The left morphism + -> (Fin n -> Fin n') -- ^ The right morphism + -> (Fin o -> Fin o') -- ^ +fplus = fplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + fplus_ :: forall m n o m' n' o' + . ( NatLE m MaxBoundInt8 + , NatLE n MaxBoundInt8 + , NatLE o MaxBoundInt8 + , NatLE m' MaxBoundInt8 + , NatLE n' MaxBoundInt8 + , NatLE o' MaxBoundInt8 + , Add m n o, Add m' n' o') + => (Fin m -> Fin m') -> (Fin n -> Fin n') -> Fin o -> Fin o' + fplus_ f g (Fin i) + | i <= x = weakenPlus (f $! Fin i) + | otherwise = widenPlus (g $! Fin (i-x)) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE fplus_ #-} +{-# INLINE fplus #-} + + +-- TODO: (Fin m, Fin n) <-> Fin (Times m n) + +---------------------------------------------------------------- +{- -- Agda's version: +thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n) +thin zero j = suc j +thin (suc i) zero = zero +thin (suc i) (suc j) = suc (thin i j) +-} +-- | The \"face maps\" for @Fin@ viewed as the standard simplices +-- (aka: the thinning view). Traditionally spelled with delta or +-- epsilon. For each @i@, it is the unique injective monotonic map +-- that skips @i@. That is, +-- +-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thin i j /= i +-- +thin :: (NatLE n MaxBoundInt8, Succ m n) => Fin n -> Fin m -> Fin n +thin i j + | weaken j < i = weaken j + | otherwise = succ (weaken j) +{-# INLINE thin #-} + + +-- BUG: Could not deduce (NatLE m MaxBoundInt8),...; so we have to add it. +-- | The \"degeneracy maps\" for @Fin@ viewed as the standard +-- simplices. Traditionally spelled with sigma or eta. For each +-- @i@, it is the unique surjective monotonic map that covers @i@ +-- twice. That is, +-- +-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thick i (i+1) == i +-- +thick + :: (NatLE m MaxBoundInt8, NatLE n MaxBoundInt8, Succ m n) + => Fin m -> Fin n -> Fin m +thick i j = + case maxView (if j <= weaken i then j else pred j) of + Just j' -> j' + Nothing -> _thick_impossible +{-# INLINE thick #-} + + + +{- +-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne? +-- The non zero view, which is used for defining compare... +data NonEmptyView : {n : Nat} -> Fin n -> Set where + ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i + +nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i +nonEmpty zero = ne +nonEmpty (suc _) = ne + + +data EqView : {n : Nat} -> Fin n -> Fin n -> Set where + equal : {n : Nat}{i : Fin n} -> EqView i i + notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j) + +compare : {n : Nat}(i j : Fin n) -> EqView i j +compare zero zero = equal +compare zero (suc j) = notequal j +compare (suc i) zero with nonEmpty i +... | ne = notequal zero +compare (suc i) (suc j) with compare i j +compare (suc i) (suc .i) | equal = equal +compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j) +-} + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- Error messages + +__ :: a +__ = error "Data.Number.Fin.Int8: attempted to evaluate type token" +{-# NOINLINE __ #-} +-- TODO: use extensible-exceptions instead of 'error' +-- TODO: use Proxy instead of these undefined values... + +_thick_impossible :: a +_thick_impossible = + error "Data.Number.Fin.Int8.thick: the impossible happened" +{-# NOINLINE _thick_impossible #-} +-- TODO: use extensible-exceptions instead of 'error' + +_succ_maxBound :: String -> a +_succ_maxBound ty = + error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound" +{-# NOINLINE _succ_maxBound #-} +-- TODO: is there an extensible-exception for this? + +_pred_minBound :: String -> a +_pred_minBound ty = + error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound" +{-# NOINLINE _pred_minBound #-} +-- TODO: is there an extensible-exception for this? + +_toEnum_OOR :: String -> a +_toEnum_OOR ty = + error $ "Enum.toEnum{"++ty++"}: argument out of range" +{-# NOINLINE _toEnum_OOR #-} +-- TODO: is there an extensible-exception for this? + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Data/Number/Fin/Integer.hs b/src/Data/Number/Fin/Integer.hs new file mode 100644 --- /dev/null +++ b/src/Data/Number/Fin/Integer.hs @@ -0,0 +1,828 @@ +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +{-# LANGUAGE ScopedTypeVariables + , DeriveDataTypeable + , MultiParamTypeClasses + , FlexibleContexts + , CPP + , Rank2Types + #-} + +#if __GLASGOW_HASKELL__ >= 701 +-- N.B., Data.Proxy and Test.QuickCheck aren't "safe". +{-# LANGUAGE Trustworthy #-} +#endif +---------------------------------------------------------------- +-- 2013.07.20 +-- | +-- Module : Data.Number.Fin.Integer +-- Copyright : 2012--2013 wren ng thornton +-- License : BSD3 +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : non-portable +-- +-- A newtype of 'Integer' for finite subsets of the natural numbers. +---------------------------------------------------------------- +module Data.Number.Fin.Integer + ( + -- * @Fin@, finite sets of natural numbers + Fin() + + -- ** Showing types + , showFinType + , showsFinType + + -- ** Convenience functions + , minBoundOf + , maxBoundOf + + -- ** Introduction and elimination + , toFin + , toFinProxy + , toFinCPS + , fromFin + + -- ** Views and coersions + -- *** Weakening and maximum views + , weaken + , weakenLE + , weakenPlus + , maxView + , maxViewLE + + -- *** Widening and the predecessor view + , widen + , widenLE + , widenPlus + , predView + + -- *** The ordinal-sum functor + , plus + , unplus + , fplus + + -- *** Face- and degeneracy-maps + , thin + , thick + -- TODO: is there any way to get equality to work right? + ) where + +import qualified Prelude.SafeEnum as SE +import Data.Ix +import Data.Number.Fin.TyDecimal (Nat, Succ, Add, NatLE) +import Data.Typeable (Typeable) +import Data.Proxy (Proxy(Proxy)) +import Data.Reflection (Reifies(reflect), reify) +import Control.Monad (liftM) + +import qualified Test.QuickCheck as QC +#if (MIN_VERSION_smallcheck(0,6,0)) +import qualified Test.SmallCheck.Series as SC +#else +import qualified Test.SmallCheck as SC +#endif +import qualified Test.LazySmallCheck as LSC + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- | A finite set of integers @Fin n = { i :: Integer | 0 <= i < n }@ +-- with the usual ordering. This is typed as if using the standard +-- GADT presentation of @Fin n@, however it is actually implemented +-- by a plain 'Integer'. +-- +-- If you care more about performance than mathematical accuracy, +-- see "Data.Number.Fin.Int32" for an alternative implementation +-- as a newtype of 'Int32'. Note, however, that doing so makes it +-- harder to reason about code since it introduces many corner +-- cases. +newtype Fin n = Fin Integer + deriving Typeable + -- WART: to give additional constraints (e.g., Nat n) on derived + -- instances (e.g., Show, Eq, Ord), we need to specify the + -- constraints on the data type declaration; however, giving of + -- data-type constraints is deprecated and will be removed from + -- the language... + +{- +-- Some fusion rules for treating newtypes like 'id', or as close +-- as we can. We only have these fire in the last stage so that +-- they don't inhibit the usual list-fusion rules. Hopefully there's +-- nothing important which is defined to not fire at [0]. +-- +-- TODO: add other laws regarding 'id' +{-# RULES +"map Fin" [0] map Fin = unsafeCoerce +"fmap Fin" [0] fmap Fin = unsafeCoerce +"liftM Fin" [0] liftM Fin = unsafeCoerce +"liftA Fin" [0] liftA Fin = unsafeCoerce + #-} +-} + +{- TODO: +-- also: + +-- | 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 ? + + +-- TODO: define @Surely a = Only a | Everything@ instead of reusing Maybe? +{- -- Agda's version: +data MaxView {n : Nat} : Fin (suc n) -> Set where + theMax : MaxView (fromNat n) + notMax : (i : Fin n) -> MaxView (weaken i) + +maxView : {n : Nat} (i : Fin (suc n)) -> MaxView i +maxView {zero} zero = theMax +maxView {zero} (suc ()) +maxView {suc n} zero = notMax zero +maxView {suc n} (suc i) with maxView i +maxView {suc n} (suc .(fromNat n)) | theMax = theMax +maxView {suc n} (suc .(weaken i)) | notMax i = notMax (suc i) +-} +-- | The maximum-element view. This strengthens the type by removing +-- the maximum element: +-- +-- > maxView maxBound = Nothing +-- > maxView x = Just x -- morally speaking... +-- +-- The opposite of this function is 'weaken'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +maxView :: Succ m n => Fin n -> Maybe (Fin m) +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n) +maxView = maxView_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + -- TODO: why is the choice of @n@ ambiguous? Even using @y<=maxBound@ we still need the signature on @y@... + maxView_ :: forall m n. Succ m n => Fin n -> Maybe (Fin m) + maxView_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxView_ #-} +{-# INLINE maxView #-} + + +-- | A variant of 'maxView' which allows strengthening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @m@ to use. +-- +-- The opposite of this function is 'weakenLE'. When the choice of +-- @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +maxViewLE :: NatLE m n => Fin n -> Maybe (Fin m) +maxViewLE = maxViewLE_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + maxViewLE_ :: forall m n. NatLE m n => Fin n -> Maybe (Fin m) + maxViewLE_ (Fin i) + | i <= maxBoundOf y = Just y + | otherwise = Nothing + where + y = Fin i :: Fin m + {-# INLINE maxViewLE_ #-} +{-# INLINE maxViewLE #-} + + +-- TODO: maxViewPlus? + + +-- This type-restricted version is a~la Agda. +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'minBound'. That is, +-- +-- > fromFin (weaken x) == fromFin x +-- +-- The opposite of this function is 'maxView'. +-- +-- > maxView . weaken == Just +-- > maybe maxBound weaken . maxView == id +-- +weaken :: Succ m n => Fin m -> Fin n +-- BUG: Could not deduce (NatLE m n) from the context (Succ m n) +weaken (Fin i) = Fin i +{-# INLINE weaken #-} + + +-- | A variant of 'weaken' which allows weakening the type by +-- multiple steps. Use of this function will generally require an +-- explicit type signature in order to know which @n@ to use. +-- +-- The opposite of this function is 'maxViewLE'. When the choice +-- of @m@ and @n@ is held constant, we have that: +-- +-- > maxViewLE . weakenLE == Just +-- > fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) +-- +weakenLE :: NatLE m n => Fin m -> Fin n +weakenLE (Fin i) = Fin i +{-# INLINE weakenLE #-} + + +---------------------------------------------------------------- +-- | The predecessor view. This strengthens the type by shifting +-- everything down by one: +-- +-- > predView 0 = Nothing +-- > predView x = Just (x-1) -- morally speaking... +-- +-- The opposite of this function is 'widen'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +predView :: Succ m n => Fin n -> Maybe (Fin m) +predView (Fin i) + | i <= 0 = Nothing + | otherwise = Just $! Fin (i-1) +{-# INLINE predView #-} + + +-- TODO: predViewLE? predViewPlus? + + +-- | Embed a finite domain into the next larger one, keeping the +-- same position relative to 'maxBound'. That is, we shift everything +-- up by one: +-- +-- > fromFin (widen x) == 1 + fromFin x +-- +-- The opposite of this function is 'predView'. +-- +-- > predView . widen == Just +-- > maybe 0 widen . predView == id +-- +widen :: Succ m n => Fin m -> Fin n +widen (Fin i) = Fin (i+1) +{-# INLINE widen #-} + + +-- | Embed a finite domain into any larger one, keeping the same +-- position relative to 'maxBound'. That is, +-- +-- > maxBoundOf y - fromFin y == maxBoundOf x - fromFin x +-- > where y = widenLE x +-- +-- Use of this function will generally require an explicit type +-- signature in order to know which @n@ to use. +widenLE :: NatLE m n => Fin m -> Fin n +widenLE x@(Fin i) = y + where + y = Fin (maxBoundOf y - maxBoundOf x + i) +{-# INLINE widenLE #-} + + +---------------------------------------------------------------- +-- BUG: Could not deduce (NatLE m o) from the context (Add m n o) +-- | A type-signature variant of 'weakenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE m o@. This is the +-- left half of 'plus'. +weakenPlus :: Add m n o => Fin m -> Fin o +weakenPlus (Fin i) = Fin i +{-# INLINE weakenPlus #-} + + +-- BUG: Could not deduce (NatLE n o) from the context (Add m n o) +-- | A type-signature variant of 'widenLE' because we cannot +-- automatically deduce that @Add m n o ==> NatLE n o@. This is the +-- right half of 'plus'. +widenPlus :: Add m n o => Fin n -> Fin o +widenPlus = widenPlus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + widenPlus_ :: forall m n o. Add m n o => Fin n -> Fin o + widenPlus_ y = Fin (maxBoundOf (__::Fin m) + fromFin y) + {-# INLINE widenPlus_ #-} +{-# INLINE widenPlus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- | The ordinal-sum functor, on objects. This internalizes the +-- disjoint union, mapping @Fin m + Fin n@ into @Fin(m+n)@ by +-- placing the image of the summands next to one another in the +-- codomain, thereby preserving the structure of both summands. +plus :: Add m n o => Either (Fin m) (Fin n) -> Fin o +plus = either weakenPlus widenPlus +{-# INLINE plus #-} + + +-- | The inverse of 'plus'. +unplus :: Add m n o => Fin o -> Either (Fin m) (Fin n) +unplus = unplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + unplus_ :: forall m n o. Add m n o => Fin o -> Either (Fin m) (Fin n) + unplus_ (Fin i) + | i <= x = Left $! Fin i + | otherwise = Right $! Fin (i-x) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE unplus_ #-} +{-# INLINE unplus #-} + + +-- BUG: Could not deduce (NatLE m o, NatLE n o) from the context (Add m n o) +-- BUG: Ditto for (Add m' n' o') +-- | The ordinal-sum functor, on morphisms. If we view the maps as +-- bipartite graphs, then the new map is the result of placing the +-- left and right maps next to one another. This is similar to +-- @(+++)@ from "Control.Arrow". +fplus :: (Add m n o, Add m' n' o') + => (Fin m -> Fin m') -- ^ The left morphism + -> (Fin n -> Fin n') -- ^ The right morphism + -> (Fin o -> Fin o') -- ^ +fplus = fplus_ + where + -- HACK: Hiding the use of -XScopedTypeVariables from Haddock + fplus_ :: forall m n o m' n' o'. (Add m n o, Add m' n' o') + => (Fin m -> Fin m') -> (Fin n -> Fin n') -> Fin o -> Fin o' + fplus_ f g (Fin i) + | i <= x = weakenPlus (f $! Fin i) + | otherwise = widenPlus (g $! Fin (i-x)) + where + x = maxBoundOf (__ :: Fin m) + {-# INLINE fplus_ #-} +{-# INLINE fplus #-} + +-- TODO: unfplus :: (Fin o -> Fin o') -> (Fin m -> Fin m', Fin n -> Fin n') + +-- TODO: (Fin m, Fin n) <-> Fin (Times m n) + +---------------------------------------------------------------- +{- -- Agda's version: +thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n) +thin zero j = suc j +thin (suc i) zero = zero +thin (suc i) (suc j) = suc (thin i j) +-} +-- | The \"face maps\" for @Fin@ viewed as the standard simplices +-- (aka: the thinning view). Traditionally spelled with delta or +-- epsilon. For each @i@, it is the unique injective monotonic map +-- that skips @i@. That is, +-- +-- > thin i = (\j -> if j < i then j else succ j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thin i j /= i +-- +thin :: Succ m n => Fin n -> Fin m -> Fin n +thin i j + | weaken j < i = weaken j + | otherwise = succ (weaken j) +{-# INLINE thin #-} + + +-- | The \"degeneracy maps\" for @Fin@ viewed as the standard +-- simplices. Traditionally spelled with sigma or eta. For each +-- @i@, it is the unique surjective monotonic map that covers @i@ +-- twice. That is, +-- +-- > thick i = (\j -> if j <= i then j else pred j) -- morally speaking... +-- +-- Which has the important universal property that: +-- +-- > thick i (i+1) == i +-- +thick :: Succ m n => Fin m -> Fin n -> Fin m +thick i j = + case maxView (if j <= weaken i then j else pred j) of + Just j' -> j' + Nothing -> _thick_impossible +{-# INLINE thick #-} + + + +{- +-- ueh? this is just another way to test for n==0; why bother with this? The only possible use I could see is to say, hey I have an actual value of Fin n, therefore n can't be zero... but then if you had a purported value of Fin n and that wasn't the case, then you'd have a contradiction to work with, ne? +-- The non zero view, which is used for defining compare... +data NonEmptyView : {n : Nat} -> Fin n -> Set where + ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i + +nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i +nonEmpty zero = ne +nonEmpty (suc _) = ne + + +data EqView : {n : Nat} -> Fin n -> Fin n -> Set where + equal : {n : Nat}{i : Fin n} -> EqView i i + notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j) + +compare : {n : Nat}(i j : Fin n) -> EqView i j +compare zero zero = equal +compare zero (suc j) = notequal j +compare (suc i) zero with nonEmpty i +... | ne = notequal zero +compare (suc i) (suc j) with compare i j +compare (suc i) (suc .i) | equal = equal +compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j) +-} + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- Error messages + +__ :: a +__ = error "Data.Number.Fin: attempted to evaluate type token" +{-# NOINLINE __ #-} +-- TODO: use extensible-exceptions instead of 'error' +-- TODO: use Proxy instead of these undefined values... + +_thick_impossible :: a +_thick_impossible = error "Data.Number.Fin.thick: the impossible happened" +{-# NOINLINE _thick_impossible #-} +-- TODO: use extensible-exceptions instead of 'error' + +_succ_maxBound :: String -> a +_succ_maxBound ty = + error $ "Enum.succ{"++ty++"}: tried to take `succ' of maxBound" +{-# NOINLINE _succ_maxBound #-} +-- TODO: is there an extensible-exception for this? + +_pred_minBound :: String -> a +_pred_minBound ty = + error $ "Enum.pred{"++ty++"}: tried to take `pred' of minBound" +{-# NOINLINE _pred_minBound #-} +-- TODO: is there an extensible-exception for this? + +_toEnum_OOR :: String -> a +_toEnum_OOR ty = + error $ "Enum.toEnum{"++ty++"}: argument out of range" +{-# NOINLINE _toEnum_OOR #-} +-- TODO: is there an extensible-exception for this? + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Data/Number/Fin/TyDecimal.hs b/src/Data/Number/Fin/TyDecimal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Number/Fin/TyDecimal.hs @@ -0,0 +1,941 @@ +-- TODO: see also +{-# 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. +-- +-- +-- [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. +-- +-- +-- [3] +---------------------------------------------------------------- +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 + +succ :: Succ x y => Proxy x -> Proxy y +succ _ = Proxy +{-# INLINE succ #-} + +pred :: Succ x y => Proxy y -> Proxy x +pred _ = Proxy +{-# INLINE pred #-} + + +-- | Assert @10*x + d == y@ where @d@ is a decimal digit and both @x@ +-- and @y@ are decimal numbers. @x@ may be zero. Essentially, this +-- is the general, non-structural, constructor\/deconstructor of a +-- decimal number. This is like the assertion @x:.d ~ y@ except that +-- we trim leading zeros of @y@ in order to ensure that it is +-- well-formed. +class (Digit_ d, Nat_ x, Nat_ y) => Snoc x d y | x d -> y, y -> x d +instance Snoc D0 D0 D0 +instance Snoc D0 D1 D1 +instance Snoc D0 D2 D2 +instance Snoc D0 D3 D3 +instance Snoc D0 D4 D4 +instance Snoc D0 D5 D5 +instance Snoc D0 D6 D6 +instance Snoc D0 D7 D7 +instance Snoc D0 D8 D8 +instance Snoc D0 D9 D9 +instance (Digit_ d, Nat_ (D1:.d)) => Snoc D1 d (D1:.d) +instance (Digit_ d, Nat_ (D2:.d)) => Snoc D2 d (D2:.d) +instance (Digit_ d, Nat_ (D3:.d)) => Snoc D3 d (D3:.d) +instance (Digit_ d, Nat_ (D4:.d)) => Snoc D4 d (D4:.d) +instance (Digit_ d, Nat_ (D5:.d)) => Snoc D5 d (D5:.d) +instance (Digit_ d, Nat_ (D6:.d)) => Snoc D6 d (D6:.d) +instance (Digit_ d, Nat_ (D7:.d)) => Snoc D7 d (D7:.d) +instance (Digit_ d, Nat_ (D8:.d)) => Snoc D8 d (D8:.d) +instance (Digit_ d, Nat_ (D9:.d)) => Snoc D9 d (D9:.d) +instance (Digit_ d', Nat_ (x:.d), Nat_ (x:.d:.d')) => Snoc (x:.d) d' (x:.d:.d') + + +-- | The primitive addition relation; by structural induction on +-- the first argument. Modes: +-- +-- > Add_ x y (x+y) +-- > Add_ x (z-x) z -- when it's defined. +-- +class (Nat_ x, Nat_ y, Nat_ z) => Add_ x y z | x y -> z, z x -> y +instance (Nat_ y) => Add_ D0 y y +instance (Succ y y1) => Add_ D1 y y1 +instance (Succ y y1, Succ y1 y2) => Add_ D2 y y2 +instance (Succ y y1, Succ y1 y2, Succ y2 y3) => Add_ D3 y y3 +instance + ( Succ y y1, Succ y1 y2, Succ y2 y3 + , Succ y3 y4 + ) => Add_ D4 y y4 +instance + ( Succ y y1, Succ y1 y2, Succ y2 y3 + , Succ y3 y4, Succ y4 y5 + ) => Add_ D5 y y5 +instance + ( Succ y y1, Succ y1 y2, Succ y2 y3 + , Succ y3 y4, Succ y4 y5, Succ y5 y6 + ) => Add_ D6 y y6 +instance + ( Succ y y1, Succ y1 y2, Succ y2 y3 + , Succ y3 y4, Succ y4 y5, Succ y5 y6 + , Succ y6 y7 + ) => Add_ D7 y y7 +instance + ( Succ y y1, Succ y1 y2, Succ y2 y3 + , Succ y3 y4, Succ y4 y5, Succ y5 y6 + , Succ y6 y7, Succ y7 y8 + ) => Add_ D8 y y8 +instance + ( Succ y y1, Succ y1 y2, Succ y2 y3 + , Succ y3 y4, Succ y4 y5, Succ y5 y6 + , Succ y6 y7, Succ y7 y8, Succ y8 y9 + ) => Add_ D9 y y9 +instance (NatNE0_ x, NatNE0_ (z:.dz), Add_ x y' z, Snoc y' dz y) + => Add_ (x:.D0) y (z:.dz) +instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D1 (zh:.dy) z) + => Add_ (x:.D1) y z +instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D2 (zh:.dy) z) + => Add_ (x:.D2) y z +instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D3 (zh:.dy) z) + => Add_ (x:.D3) y z +instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D4 (zh:.dy) z) + => Add_ (x:.D4) y z +instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D5 (zh:.dy) z) + => Add_ (x:.D5) y z +instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D6 (zh:.dy) z) + => Add_ (x:.D6) y z +instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D7 (zh:.dy) z) + => Add_ (x:.D7) y z +instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D8 (zh:.dy) z) + => Add_ (x:.D8) y z +instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D9 (zh:.dy) z) + => Add_ (x:.D9) y z + + +-- | The addition relation with full dependencies. Modes: +-- +-- > Add x y (x+y) +-- > Add x (z-x) z -- when it's defined. +-- > Add (z-y) y z -- when it's defined. +-- +class (Add_ x y z, Add_ y x z) => Add x y z | x y -> z, z x -> y, z y -> x +instance (Add_ x y z, Add_ y x z) => Add x y z + +add :: Add x y z => Proxy x -> Proxy y -> Proxy z +add _ _ = Proxy +{-# INLINE add #-} + +-- | N.B., this will be ill-typed if @x@ is greater than @z@. +minus :: Add x y z => Proxy z -> Proxy x -> Proxy y +minus _ _ = Proxy +{-# INLINE minus #-} + +-- | N.B., this will be ill-typed if @x@ is greater than @z@. +subtract :: Add x y z => Proxy x -> Proxy z -> Proxy y +subtract _ _ = Proxy +{-# INLINE subtract #-} + +---------------------------------------------------------------- +-- Equality and order: the comparison relation + +-- | Assert that the comparison relation @r@ (@LT_@, @EQ_@, or +-- @GT_@) holds between @x@ and @y@; by structural induction on the +-- first, and then the second argument. +class (Nat_ x, Nat_ y) => Compare x y r | x y -> r +instance Compare D0 D0 EQ_ +instance Compare D0 D1 LT_ +instance Compare D0 D2 LT_ +instance Compare D0 D3 LT_ +instance Compare D0 D4 LT_ +instance Compare D0 D5 LT_ +instance Compare D0 D6 LT_ +instance Compare D0 D7 LT_ +instance Compare D0 D8 LT_ +instance Compare D0 D9 LT_ +instance NatNE0_ (y:.dy) => Compare D0 (y:.dy) LT_ +instance Compare D1 D0 GT_ +instance Compare D1 D1 EQ_ +instance Compare D1 D2 LT_ +instance Compare D1 D3 LT_ +instance Compare D1 D4 LT_ +instance Compare D1 D5 LT_ +instance Compare D1 D6 LT_ +instance Compare D1 D7 LT_ +instance Compare D1 D8 LT_ +instance Compare D1 D9 LT_ +instance NatNE0_ (y:.dy) => Compare D1 (y:.dy) LT_ +instance Compare D2 D0 GT_ +instance Compare D2 D1 GT_ +instance Compare D2 D2 EQ_ +instance Compare D2 D3 LT_ +instance Compare D2 D4 LT_ +instance Compare D2 D5 LT_ +instance Compare D2 D6 LT_ +instance Compare D2 D7 LT_ +instance Compare D2 D8 LT_ +instance Compare D2 D9 LT_ +instance NatNE0_ (y:.dy) => Compare D2 (y:.dy) LT_ +instance Compare D3 D0 GT_ +instance Compare D3 D1 GT_ +instance Compare D3 D2 GT_ +instance Compare D3 D3 EQ_ +instance Compare D3 D4 LT_ +instance Compare D3 D5 LT_ +instance Compare D3 D6 LT_ +instance Compare D3 D7 LT_ +instance Compare D3 D8 LT_ +instance Compare D3 D9 LT_ +instance NatNE0_ (y:.dy) => Compare D3 (y:.dy) LT_ +instance Compare D4 D0 GT_ +instance Compare D4 D1 GT_ +instance Compare D4 D2 GT_ +instance Compare D4 D3 GT_ +instance Compare D4 D4 EQ_ +instance Compare D4 D5 LT_ +instance Compare D4 D6 LT_ +instance Compare D4 D7 LT_ +instance Compare D4 D8 LT_ +instance Compare D4 D9 LT_ +instance NatNE0_ (y:.dy) => Compare D4 (y:.dy) LT_ +instance Compare D5 D0 GT_ +instance Compare D5 D1 GT_ +instance Compare D5 D2 GT_ +instance Compare D5 D3 GT_ +instance Compare D5 D4 GT_ +instance Compare D5 D5 EQ_ +instance Compare D5 D6 LT_ +instance Compare D5 D7 LT_ +instance Compare D5 D8 LT_ +instance Compare D5 D9 LT_ +instance NatNE0_ (y:.dy) => Compare D5 (y:.dy) LT_ +instance Compare D6 D0 GT_ +instance Compare D6 D1 GT_ +instance Compare D6 D2 GT_ +instance Compare D6 D3 GT_ +instance Compare D6 D4 GT_ +instance Compare D6 D5 GT_ +instance Compare D6 D6 EQ_ +instance Compare D6 D7 LT_ +instance Compare D6 D8 LT_ +instance Compare D6 D9 LT_ +instance NatNE0_ (y:.dy) => Compare D6 (y:.dy) LT_ +instance Compare D7 D0 GT_ +instance Compare D7 D1 GT_ +instance Compare D7 D2 GT_ +instance Compare D7 D3 GT_ +instance Compare D7 D4 GT_ +instance Compare D7 D5 GT_ +instance Compare D7 D6 GT_ +instance Compare D7 D7 EQ_ +instance Compare D7 D8 LT_ +instance Compare D7 D9 LT_ +instance NatNE0_ (y:.dy) => Compare D7 (y:.dy) LT_ +instance Compare D8 D0 GT_ +instance Compare D8 D1 GT_ +instance Compare D8 D2 GT_ +instance Compare D8 D3 GT_ +instance Compare D8 D4 GT_ +instance Compare D8 D5 GT_ +instance Compare D8 D6 GT_ +instance Compare D8 D7 GT_ +instance Compare D8 D8 EQ_ +instance Compare D8 D9 LT_ +instance NatNE0_ (y:.dy) => Compare D8 (y:.dy) LT_ +instance Compare D9 D0 GT_ +instance Compare D9 D1 GT_ +instance Compare D9 D2 GT_ +instance Compare D9 D3 GT_ +instance Compare D9 D4 GT_ +instance Compare D9 D5 GT_ +instance Compare D9 D6 GT_ +instance Compare D9 D7 GT_ +instance Compare D9 D8 GT_ +instance Compare D9 D9 EQ_ +instance NatNE0_ (y:.dy) => Compare D9 (y:.dy) LT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D0 GT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D1 GT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D2 GT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D3 GT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D4 GT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D5 GT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D6 GT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D7 GT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D8 GT_ +instance NatNE0_ (x:.dx) => Compare (x:.dx) D9 GT_ +instance + ( NatNE0_ (x:.dx), NatNE0_ (y:.dy) + , Compare dx dy dr, Compare x y r', NCS r' dr r + ) => Compare (x:.dx) (y:.dy) r + +compare :: Compare x y r => Proxy x -> Proxy y -> Proxy r +compare _ _ = Proxy +{-# INLINE compare #-} + + +-- BUG: is this still an optimization now that there's a combinatorial explosion? +-- | Assert that @x <= y@. This is a popular constraint, so we +-- implement it specially. We could have said that @Add n x y => +-- NatLE x y@, but the following inductive definition is a bit +-- more optimal. +class (Nat_ x, Nat_ y) => NatLE x y +instance NatLE D0 D0 +instance NatLE D0 D1 +instance NatLE D0 D2 +instance NatLE D0 D3 +instance NatLE D0 D4 +instance NatLE D0 D5 +instance NatLE D0 D6 +instance NatLE D0 D7 +instance NatLE D0 D8 +instance NatLE D0 D9 +instance NatNE0_ (y:.dy) => NatLE D0 (y:.dy) +instance NatLE D1 D1 +instance NatLE D1 D2 +instance NatLE D1 D3 +instance NatLE D1 D4 +instance NatLE D1 D5 +instance NatLE D1 D6 +instance NatLE D1 D7 +instance NatLE D1 D8 +instance NatLE D1 D9 +instance NatNE0_ (y:.dy) => NatLE D1 (y:.dy) +instance NatLE D2 D2 +instance NatLE D2 D3 +instance NatLE D2 D4 +instance NatLE D2 D5 +instance NatLE D2 D6 +instance NatLE D2 D7 +instance NatLE D2 D8 +instance NatLE D2 D9 +instance NatNE0_ (y:.dy) => NatLE D2 (y:.dy) +instance NatLE D3 D3 +instance NatLE D3 D4 +instance NatLE D3 D5 +instance NatLE D3 D6 +instance NatLE D3 D7 +instance NatLE D3 D8 +instance NatLE D3 D9 +instance NatNE0_ (y:.dy) => NatLE D3 (y:.dy) +instance NatLE D4 D4 +instance NatLE D4 D5 +instance NatLE D4 D6 +instance NatLE D4 D7 +instance NatLE D4 D8 +instance NatLE D4 D9 +instance NatNE0_ (y:.dy) => NatLE D4 (y:.dy) +instance NatLE D5 D5 +instance NatLE D5 D6 +instance NatLE D5 D7 +instance NatLE D5 D8 +instance NatLE D5 D9 +instance NatNE0_ (y:.dy) => NatLE D5 (y:.dy) +instance NatLE D6 D6 +instance NatLE D6 D7 +instance NatLE D6 D8 +instance NatLE D6 D9 +instance NatNE0_ (y:.dy) => NatLE D6 (y:.dy) +instance NatLE D7 D7 +instance NatLE D7 D8 +instance NatLE D7 D9 +instance NatNE0_ (y:.dy) => NatLE D7 (y:.dy) +instance NatLE D8 D8 +instance NatLE D8 D9 +instance NatNE0_ (y:.dy) => NatLE D8 (y:.dy) +instance NatLE D9 D9 +instance NatNE0_ (y:.dy) => NatLE D9 (y:.dy) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D9) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D1) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D9) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D2) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D2) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D9) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D9) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D9) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D9) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D9) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D9) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D8) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D8) (y:.D9) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D0) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D1) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D2) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D3) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D4) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D5) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D6) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D7) +instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D8) +instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D9) (y:.D9) + + +-- | N.B., this will be ill-typed if @x@ is greater than @y@. +assert_NatLE :: NatLE x y => Proxy x -> Proxy y -> () +assert_NatLE Proxy Proxy = () + + +-- | Assert that @x < y@. This is just a shorthand for @x <= pred y@. +class (Nat_ x, NatNE0_ y) => NatLT x y +instance (Succ y' y, NatLE x y') => NatLT x y + + +-- | Choose the larger of @x@ and @y@ according to the order @r@. +class Max_ x y r z | x y r -> z +instance Max_ x y LT_ y +instance Max_ x y EQ_ y -- doesn't matter which we pick +instance Max_ x y GT_ x + +-- | Choose the larger of @x@ and @y@. +max :: (Compare x y r, Max_ x y r z) => Proxy x -> Proxy y -> Proxy z +max _ _ = Proxy +{-# INLINE max #-} + + +-- | Choose the smaller of @x@ and @y@ according to the order @r@. +class Min_ x y r z | x y r -> z +instance Min_ x y LT_ x +instance Min_ x y EQ_ x -- doesn't matter which we pick +instance Min_ x y GT_ y + +-- | Choose the smaller of @x@ and @y@. +min :: (Compare x y r, Min_ x y r z) => Proxy x -> Proxy y -> Proxy z +min _ _ = Proxy +{-# INLINE min #-} + + +{- +---------------------------------------------------------------- +-- TODO: should we offer @((floor.). div)@, @((ceiling.). div)@, @divMod@ ? + + +-- | Assert that @x * y == z@ where @x > 0@; by structural induction +-- on the first argument. +class (NatNE0_ x, Nat_ y, Nat_ z) => Mul_ x y z | x y -> z, x z -> y +instance Nat_ y => Mul_ B1 y y +instance (Mul_ x y zh, Snoc zh B0 z) => Mul_ (x:.B0) y z +instance (Mul_F x y z, Mul_B x y z) => Mul_ (x:.B1) y z + + +-- | Assert that @(2x+1) * y == z@ where @x > 0@. +class (NatNE0_ x, Nat_ y, Nat_ z) => Mul_F x y z | x y -> z +instance NatNE0_ x => Mul_F x B0 B0 +instance NatNE0_ x => Mul_F x B1 (x:.B1) +-- (2x+1) * 2y +instance (Mul_F x y z, NatNE0_ x, NatNE0_ y, NatNE0_ z) + => Mul_F x (y:.B0) (z:.B0) +-- (2x+1) * (2y+1) = 2*( (2x+1)*y + x ) + 1, y > 0 +instance (Mul_F x y z', Add x z' z, NatNE0_ x, NatNE0_ y, NatNE0_ z) + => Mul_F x (y:.B1) (z:.B1) + + +-- | Assert that @(2x+1) * y == z@ where @x > 0@. The functional +-- dependencies go the other way though. +class (NatNE0_ x, Nat_ y, Nat_ z) => Mul_B x y z | z x -> y +instance NatNE0_ x => Mul_B x B0 B0 +-- instance NatNE0_ x => Mul_B x y B1 -- cannot happen +-- (2x+1) * 2y +instance (Mul_B x y z, NatNE0_ x, NatNE0_ y, NatNE0_ z) + => Mul_B x (y:.B0) (z:.B0) +-- (2x+1) * (2y+1) = 2*( (2x+1)*y + x ) + 1, y >= 0 +instance (Snoc y B1 yt, Mul_B x y z', Add x z' z, NatNE0_ x, NatNE0_ z) + => Mul_B x yt (z:.B1) + + +-- | The multiplication relation with full dependencies. Modes: +-- +-- > Mul x y (x*y) +-- > Mul x (z/x) z -- when it's defined. +-- > Mul (z/y) y z -- when it's defined. +-- +class (Mul_ x y z, Mul_ y x z) => Mul x y z | x y -> z, x z -> y, y z -> x +instance (Mul_ x y z, Mul_ y x z) => Mul x y z + +mul :: Mul x y z => Proxy x -> Proxy y -> Proxy z +mul _ _ = Proxy +{-# INLINE mul #-} + +-- | N.B., this will be ill-typed if @z@ is not a multiple of @x@. +div :: Mul x y z => Proxy z -> Proxy x -> Proxy y +div _ _ = Proxy +{-# INLINE div #-} + +-- tm1 = mul nat2 nat8 +-- tm2 = reflect $ mul nat8 nat2 +-- tm3 = reflect $ mul (succ nat2) nat2 +-- tm4 = reflect $ mul nat2 (succ nat2) +-- tm5 = reflect $ mul (succ nat4) (succ nat2) +-- tm6 = reflect $ mul (succ nat2) (succ nat4) +-- tm7 = reflect $ div (mul (succ nat8) nat2) (succ nat2) -- 18/3 + + +---------------------------------------------------------------- +-- TODO: should we offer @(floor . logBase 2)@ and @(ceiling . logBase 2)@ ? +-- TODO: general exponentiation/logarithm + + +-- | Power-of-two exponentiation\/logarithm relation. Modes: +-- +-- > Exp2 x (2^x) +-- > Exp2 (logBase 2 y) y -- when it's defined. +-- +class (Nat_ x, NatNE0_ y) => Exp2 x y | x -> y, y -> x +instance Exp2 B0 B1 +instance Exp2 B1 (B1:.B0) +instance (Succ x1 (x:.d), Exp2 x1 (y:.B0)) => Exp2 (x:.d) (y:.B0:.B0) + +exp2 :: Exp2 x y => Proxy x -> Proxy y +exp2 _ = Proxy +{-# INLINE exp2 #-} + +-- | N.B., this will be ill-typed if @y@ is not a power of 2. +log2 :: Exp2 x y => Proxy y -> Proxy x +log2 _ = Proxy +{-# INLINE log2 #-} + +-- te1 = exp2 (succ (succ nat8)) +-- te1' = reflect $ exp2 (succ (succ nat8)) +-- te2 = reflect $ log2 nat8 + + +---------------------------------------------------------------- +-- Do we need the full dependency? If we know x and we know z, +-- we can't tell what y exactly (except being the multiple of z) + +-- | Get the gcd by Euclid's algorithm. Modes: +-- +-- > GCD x y (gcd x y) +-- +class (Nat_ x, Nat_ y, Nat_ z) => GCD x y z | x y -> z +instance Nat_ y => GCD B0 y y +instance Nat_ y => GCD B1 y B1 +instance (Compare (x:.dx) y r, GCD_ r (x:.dx) y z) => GCD (x:.dx) y z + +class (NatNE0_ x, Nat_ y, Nat_ z) => GCD_ r x y z | r x y -> z +instance NatNE0_ x => GCD_ EQ_ x x x +instance (GCD y x z, NatNE0_ x) => GCD_ GT_ x y z +instance (Add x y1 y, GCD y1 x z, NatNE0_ x) => GCD_ LT_ x y z + +gcd :: GCD x y z => Proxy x -> Proxy y -> Proxy z +gcd _ _ = Proxy +{-# INLINE gcd #-} + +-- tg1 = reflect $ gcd nat8 nat8 +-- tg2 = reflect $ gcd nat8 (pred nat8) +-- tg3 = reflect $ gcd nat8 (pred (pred nat8)) +-- tg4 = reflect $ gcd (pred (pred nat8)) nat8 +-- tg5 = reflect $ gcd nat4 nat8 +-- tg6 = reflect $ gcd (pred nat4) (succ nat8) +-- tg7 = reflect $ gcd (succ nat8) (pred nat4) +-} + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Data/Number/Fin/TyOrdering.hs b/src/Data/Number/Fin/TyOrdering.hs new file mode 100644 --- /dev/null +++ b/src/Data/Number/Fin/TyOrdering.hs @@ -0,0 +1,79 @@ +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +{-# LANGUAGE EmptyDataDecls + , DeriveDataTypeable + , MultiParamTypeClasses + , FlexibleInstances + , FunctionalDependencies + #-} + +{-# LANGUAGE CPP #-} +#if __GLASGOW_HASKELL__ >= 701 +{-# LANGUAGE Safe #-} +#endif +---------------------------------------------------------------- +-- 2013.05.29 +-- | +-- Module : Data.Number.Fin.TyOrdering +-- Copyright : 2012--2013 wren ng thornton, +-- 2004--2007 Oleg Kiselyov and Chung-chieh Shan +-- License : BSD3 +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : non-portable +-- +-- Type-level 'Ordering'. This is based on [1], and is intended to +-- work with [2] (though we use the @reflection@ package for the +-- actual reification part). +-- +-- A lot of this also duplicates the functionality in +-- @HList:Data.HList.FakePrelude@[3], which is (or should be) +-- obviated by the new data kinds extension. However, we don't want +-- to restrict this module to the newer versions of GHC which support +-- data kinds. +-- +-- [1] Oleg Kiselyov and Chung-chieh Shan. (2007) /Lightweight/ +-- /static resources: Sexy types for embedded and systems/ +-- /programming/. Proc. Trends in Functional Programming. +-- New York, 2--4 April 2007. +-- +-- +-- [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. +-- +-- +-- [3] +---------------------------------------------------------------- +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.