type-natural 0.2.2.0 → 0.2.3.0

raw patch · 2 files changed

+42/−6 lines, 2 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Data/Type/Ordinal.hs +41/−5
• type-natural.cabal +1/−1

@@ -1,7 +1,11 @@+{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE CPP, DataKinds, EmptyDataDecls, FlexibleContexts         #-} {-# LANGUAGE FlexibleInstances, GADTs, KindSignatures, PolyKinds      #-} {-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-} {-# LANGUAGE TypeFamilies, TypeOperators                              #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707+{-# LANGUAGE EmptyCase, LambdaCase #-}+#endif -- | Set-theoretic ordinal arithmetic module Data.Type.Ordinal        ( -- * Data-types@@ -12,7 +16,9 @@          unsafeFromInt, inclusion, inclusion',          -- * Ordinal arithmetics          (@+), enumOrdinal,-         -- * Quasi Quote+         -- * Elimination rules for @'Ordinal' 'Z'@.+         absurdOrd, vacuousOrd, vacuousOrdM,+         -- * Quasi Quoter          od        ) where import Data.Constraint@@ -24,7 +30,9 @@ import Unsafe.Coerce #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 import Data.Singletons.Prelude+import Data.Typeable (Typeable) #endif+import Control.Monad (liftM)  -- | Set-theoretic (finite) ordinals: --@@ -35,6 +43,10 @@   OZ :: Ordinal (S n)   OS :: Ordinal n -> Ordinal (S n) +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707+-- | Since 0.2.3.0  +deriving instance Typeable Ordinal+#endif -- | Parsing always fails, because there are no inhabitant. instance Read (Ordinal Z) where   readsPrec _ _ = []@@ -85,7 +97,7 @@ unsafeFromInt n =     case (promote n :: Monomorphic (Sing :: Nat -> *)) of       Monomorphic sn ->-        case sS sn %:<<= (sing :: SNat n) of+        case SS sn %:<<= (sing :: SNat n) of           STrue -> sNatToOrd' (sing :: SNat n) sn           SFalse -> error "Bound over!" @@ -104,10 +116,10 @@  -- | Convert @Ordinal n@ into @SNat m@ with the proof of @S m :<<= n@. ordToSNat' :: Ordinal n -> CastedOrdinal n-ordToSNat' OZ = CastedOrdinal sZ+ordToSNat' OZ = CastedOrdinal SZ ordToSNat' (OS on) =   case ordToSNat' on of-    CastedOrdinal m -> CastedOrdinal (sS m)+    CastedOrdinal m -> CastedOrdinal (SS m)  -- | Convert @Ordinal n@ into monomorphic @SNat@ ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)@@ -132,7 +144,7 @@ inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m inclusion' (SS SZ) OZ = OZ inclusion' (SS (SS _)) OZ = OZ-inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (sS n) m+inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (SS n) m inclusion' _ _ = bugInGHC -} @@ -152,6 +164,30 @@   case sing :: SNat n of     SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m     _ -> bugInGHC++-- | Since @Ordinal Z@ is logically not inhabited, we can coerce it to any value.+--+-- Since 0.2.3.0+absurdOrd :: Ordinal Z -> a+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707+absurdOrd cs = case cs of {}+#else+absurdOrd _ = error "Impossible!"+#endif++-- | 'absurdOrd' for the value in 'Functor'.+-- +--   Since 0.2.3.0+vacuousOrd :: Functor f => f (Ordinal Z) -> f a+vacuousOrd = fmap absurdOrd++-- | 'absurdOrd' for the value in 'Monad'.+--   This function will become uneccesary once 'Applicative' (and hence 'Functor')+--   become the superclass of 'Monad'.+-- +--   Since 0.2.3.0+vacuousOrdM :: Monad m => m (Ordinal Z) -> m a+vacuousOrdM = liftM absurdOrd  -- | Quasiquoter for ordinals od :: QuasiQuoter

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.2.2.0+version:             0.2.3.0 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties. homepage:            https://github.com/konn/type-natural