diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs --- a/Data/Type/Natural.hs +++ b/Data/Type/Natural.hs @@ -31,7 +31,7 @@ -- * Conversion functions natToInt, intToNat, sNatToInt, -- * Quasi quotes for natural numbers - nat, snat, + snat, -- * Properties of natural numbers IsPeano(..), plusCong, plusCongR, plusCongL, @@ -279,23 +279,9 @@ -- * Quasi Quoter -------------------------------------------------- --- | Quotesi-quoter for 'Nat'. This can be used for an expression, pattern and type. --- --- for example: @sing :: SNat ([nat| 2 |] :+ [nat| 5 |])@ -nat :: QuasiQuoter -nat = QuasiQuoter { quoteExp = foldr appE (conE 'Z) . flip replicate (conE 'S) . read - , quotePat = foldr (\a b -> conP a [b]) (conP 'Z []) . flip replicate 'S . read - , quoteType = foldr appT (conT 'Z) . flip replicate (conT 'S) . read - , quoteDec = error "not implemented" - } - --- | Quotesi-quoter for 'SNat'. This can be used for an expression, pattern and type. +-- | Quotesi-quoter for 'SNat'. This can be used for an expression. -- --- For example: @[snat|12|] '%+' [snat| 5 |]@, @'sing' :: [snat| 12 |]@, @f [snat| 12 |] = \"hey\"@ +-- For example: @[snat|12|] '%:+' [snat| 5 |]@. snat :: QuasiQuoter -snat = QuasiQuoter { quoteExp = foldr appE (conE 'SZ) . flip replicate (conE 'SS) . read - , quotePat = foldr (\a b -> conP a [b]) (conP 'SZ []) . flip replicate 'SS . read - , quoteType = appT (conT ''SNat) . foldr appT (conT 'Z) . flip replicate (conT 'S) . read - , quoteDec = error "not implemented" - } +snat = mkSNatQQ [t| Nat |] diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs --- a/Data/Type/Natural/Builtin.hs +++ b/Data/Type/Natural/Builtin.hs @@ -24,6 +24,8 @@ -- * Peano and commutative ring axioms for built-in @'GHC.TypeLits.Nat'@ IsPeano(..), inductionNat, + -- * QuasiQuotes + snat ) where import Data.Type.Natural.Class @@ -46,6 +48,7 @@ import Data.Void (Void) import GHC.TypeLits (type (+), type (<=), type (<=?)) import qualified GHC.TypeLits as TL +import Language.Haskell.TH.Quote (QuasiQuoter) import Proof.Equational (coerce, withRefl) import Proof.Equational (start, sym, (===), (=~=)) import Proof.Equational (because) @@ -276,8 +279,8 @@ -- | Induction scheme for built-in @'TL.Nat'@. inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n -inductionNat base step snat = - case viewNat snat of +inductionNat base step sn = + case viewNat sn of IsZero -> base IsSucc sl -> step (inductionNat base step sl) @@ -303,8 +306,8 @@ multAssoc _ _ _ = Refl plusMultDistrib _ _ _ = Refl multPlusDistrib _ _ _ = Refl - induction base step snat = - case viewNat snat of + induction base step sn = + case viewNat sn of IsZero -> base IsSucc sl -> withKnownNat sl $ step sing (induction base step sl) @@ -414,3 +417,8 @@ promote n = case toSing n of SomeSing k -> Monomorphic k {-# INLINE promote #-} +-- | Quotesi-quoter for singleton types for @'GHC.TypeLits.Nat'@. This can be used for an expression. +-- +-- For example: @[snat|12|] '%:+' [snat| 5 |]@. +snat :: QuasiQuoter +snat = mkSNatQQ [t| TL.Nat |] diff --git a/Data/Type/Natural/Class.hs b/Data/Type/Natural/Class.hs --- a/Data/Type/Natural/Class.hs +++ b/Data/Type/Natural/Class.hs @@ -1,7 +1,33 @@ +{-# LANGUAGE TemplateHaskell #-} -- | Re-exports arithmetic and order structure for peano arithmetic. -module Data.Type.Natural.Class ( module Data.Type.Natural.Class.Arithmetic - , module Data.Type.Natural.Class.Order - ) where +module Data.Type.Natural.Class + ( module Data.Type.Natural.Class.Arithmetic + , module Data.Type.Natural.Class.Order + , -- * Quasi quoters generator for naturals + mkSNatQQ) where import Data.Type.Natural.Class.Arithmetic import Data.Type.Natural.Class.Order +import Data.Singletons.Prelude (FromInteger, Sing, sing) +import Language.Haskell.TH +import Language.Haskell.TH.Quote + +-- | Quasiquoter generateor for specific peano-types. +-- +-- Since 0.7.0.0 +mkSNatQQ :: TypeQ -> QuasiQuoter +mkSNatQQ t = QuasiQuoter + { quoteExp = mkExpQuote + , quotePat = error "no pattern quoter for snats" + -- foldr (\a b -> conP a [b]) (conP 'SZ []) . flip replicate 'SS . read + , quoteType = mkTypeQuote + , quoteDec = error "not implemented" + } + where + mkExpQuote :: String -> ExpQ + mkExpQuote s = [| sing :: $(mkTypeQuote s) |] + + mkTypeQuote :: String -> TypeQ + mkTypeQuote s = + let n = read s + in [t| Sing $(sigT [t| FromInteger $(litT $ numTyLit n)|] =<< t) |] diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs --- a/Data/Type/Ordinal.hs +++ b/Data/Type/Ordinal.hs @@ -8,21 +8,21 @@ module Data.Type.Ordinal ( -- * Data-types Ordinal (..), pattern OZ, pattern OS, HasOrdinal, + -- * Quasi Quoter + -- $quasiquotes + mkOrdinalQQ, odPN, odLit, -- * Conversion from cardinals to ordinals. sNatToOrd', sNatToOrd, ordToInt, ordToSing, - ordToSing', CastedOrdinal(..), unsafeFromInt, inclusion, inclusion', -- * Ordinal arithmetics (@+), enumOrdinal, -- * Elimination rules for @'Ordinal' 'Z'@. - absurdOrd, vacuousOrd, vacuousOrdM, - -- * Quasi Quoter - od + absurdOrd, vacuousOrd ) where -import Control.Monad (liftM) import Data.Kind import Data.List (genericDrop, genericTake) import Data.Ord (comparing) +import Data.Singletons.Decide import Data.Singletons.Prelude import Data.Singletons.Prelude.Enum import Data.Type.Equality @@ -46,7 +46,7 @@ -- -- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. -- --- Since 0.5.0.0 +-- Since 0.6.0.0 data Ordinal (n :: nat) where OLt :: (IsPeano nat, (n :< m) ~ 'True) => Sing (n :: nat) -> Ordinal m @@ -57,12 +57,16 @@ OLt n -- | Pattern synonym representing the 0-th ordinal. +-- +-- Since 0.6.0.0 pattern OZ :: forall nat (n :: nat). IsPeano nat => (Zero nat :< n) ~ 'True => Ordinal n pattern OZ <- OLt Zero where OZ = OLt sZero -- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal. +-- +-- Since 0.6.0.0 pattern OS :: forall nat (t :: nat). (PeanoOrder nat, SingI t) => (IsPeano nat) => Ordinal t -> Ordinal (Succ t) @@ -133,7 +137,8 @@ => Ordinal n -> [Ordinal n] enumFromOrd ord = genericDrop (ordToInt ord) $ enumOrdinal (sing :: Sing n) -enumOrdinal :: (PeanoOrder nat, SingI n) => Sing (n :: nat) -> [Ordinal n] +-- | Enumerate all @'Ordinal'@s less than @n@. +enumOrdinal :: (PeanoOrder nat) => Sing (n :: nat) -> [Ordinal n] enumOrdinal (Succ n) = withSingI n $ withWitness (lneqZero n) $ OLt sZero : map succOrd (enumOrdinal n) @@ -162,7 +167,6 @@ sNatToOrd (sing :: Sing m) {-# INLINE maxBound #-} - unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => MonomorphicRep (Sing :: nat -> *) -> Ordinal n unsafeFromInt n = @@ -192,14 +196,6 @@ sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n sNatToOrd = sNatToOrd' sing -data CastedOrdinal n where - CastedOrdinal :: (m :< n) ~ 'True => Sing m -> CastedOrdinal n - --- | Convert @Ordinal n@ into @Sing m@ with the proof of @'S m :<= n@. -ordToSing' :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> CastedOrdinal n -ordToSing' (OLt s) = CastedOrdinal s -{-# INLINE ordToSing' #-} - -- | Convert @Ordinal n@ into monomorphic @Sing@ -- -- Since 0.5.0.0 @@ -216,11 +212,15 @@ {-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Integer #-} -- | Inclusion function for ordinals. -inclusion' :: (n :< m) ~ 'True => Sing m -> Ordinal n -> Ordinal m +-- +-- Since 0.7.0.0 (constraint was weakened since last released) +inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m inclusion' _ = unsafeCoerce {-# INLINE inclusion' #-} -- | Inclusion function for ordinals with codomain inferred. +-- +-- Since 0.7.0.0 (constraint was weakened since last released) inclusion :: ((n :<= m) ~ 'True) => Ordinal n -> Ordinal m inclusion on = unsafeCoerce on {-# INLINE inclusion #-} @@ -239,24 +239,36 @@ absurdOrd :: PeanoOrder nat => Ordinal (Zero nat) -> a absurdOrd (OLt n) = absurd $ lneqZeroAbsurd n Witness --- | 'absurdOrd' for the value in 'Functor'. +-- | @'absurdOrd'@ for value in 'Functor'. -- -- Since 0.2.3.0 vacuousOrd :: (PeanoOrder nat, Functor f) => f (Ordinal (Zero nat)) -> 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 :: (PeanoOrder nat, Monad m) => m (Ordinal (Zero nat)) -> m a -vacuousOrdM = liftM absurdOrd +{-$quasiquotes #quasiquoters# --- | Quasiquoter for ordinals -od :: QuasiQuoter -od = QuasiQuoter { quoteExp = foldr appE (conE 'OZ) . flip replicate (conE 'OS) . read - , quoteType = error "No type quoter for Ordinals" - , quotePat = foldr (\a b -> conP a [b]) (conP 'OZ []) . flip replicate 'OS . read - , quoteDec = error "No declaration quoter for Ordinals" - } + This section provides QuasiQuoter and general generator for ordinals. + Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT + checks boundary; with @'od'@, we can use literal with + boundary check. + For example, with @-XQuasiQuotes@ language extension enabled, + @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error, + whilst @12 :: Ordinal 1@ compiles but raises run-time error. + So, to enforce correctness, we recommend to use these quoters + instead of bare @'Num'@ numerals. +-} + +-- | Quasiquoter generator for ordinals +mkOrdinalQQ :: TypeQ -> QuasiQuoter +mkOrdinalQQ t = + QuasiQuoter { quoteExp = \s -> [| OLt $(quoteExp (mkSNatQQ t) s) |] + , quoteType = error "No type quoter for Ordinals" + , quotePat = \s -> [p| OLt ((%~ $(quoteExp (mkSNatQQ t) s)) -> Proved Refl) |] + , quoteDec = error "No declaration quoter for Ordinals" + } + +odPN, odLit :: QuasiQuoter +-- | Quasiquoter for ordinal indexed by Peano numeral @'Data.Type.Natural.Nat'@. +odPN = mkOrdinalQQ [t| PN.Nat |] +-- | Quasiquoter for ordinal indexed by built-in numeral @'GHC.TypeLits.Nat'@. +odLit = mkOrdinalQQ [t| TL.Nat |] diff --git a/Data/Type/Ordinal/Builtin.hs b/Data/Type/Ordinal/Builtin.hs new file mode 100644 --- /dev/null +++ b/Data/Type/Ordinal/Builtin.hs @@ -0,0 +1,149 @@ +{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs #-} +{-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-} +-- | Module providing the same API as 'Data.Type.Ordinal' but specialised to +-- GHC's builtin @'Nat'@. +-- +-- Since 0.7.0.0 +module Data.Type.Ordinal.Builtin + ( -- * Data-types and pattern synonyms + Ordinal, pattern OLt, pattern OZ, pattern OS, + -- * Quasi Quoter + -- $quasiquotes + od, + -- * Conversion from cardinals to ordinals. + sNatToOrd', sNatToOrd, ordToInt, + unsafeFromInt, inclusion, inclusion', + -- * Ordinal arithmetics + (@+), enumOrdinal, + -- * Elimination rules for @'Ordinal' 'Z'@. + absurdOrd, vacuousOrd + ) where +import Data.Kind +import Data.Singletons.Prelude (POrd (..), SingI, Sing (..)) +import Data.Singletons.Prelude.Enum (PEnum (..)) +import qualified Data.Type.Ordinal as O +import Data.Type.Natural +import Language.Haskell.TH.Quote (QuasiQuoter) +import Data.Type.Monomorphic + +-- | Set-theoretic (finite) ordinals: +-- +-- > n = {0, 1, ..., n-1} +-- +-- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. +-- This module exports a variant of polymorphic @'Data.Type.Ordinal.Ordinal'@ +-- specialised to GHC's builtin numeral @'Nat'@. +-- +-- Since 0.7.0.0 +type Ordinal (n :: Nat) = O.Ordinal n + +-- | We provide specialised version of constructor @'O.OLt'@ as type synonym @'OLt'@. +-- In some case, GHC warns about incomplete pattern using pattern @'OLt'@, +-- but it is due to the limitation of GHC's current exhaustiveness checker. +-- +-- Since 0.7.0.0 +pattern OLt :: () => forall (n1 :: Nat). ((n1 :< t) ~ 'True) + => Sing n1 -> O.Ordinal t +pattern OLt n = O.OLt n + +-- | Pattern synonym representing the 0-th ordinal. +-- +-- Since 0.7.0.0 +pattern OZ :: forall (n :: Nat). () + => ('Z :< n) ~ 'True => O.Ordinal n +pattern OZ = O.OZ + +-- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal. +-- +-- Since 0.7.0.0 +pattern OS :: forall (t :: Nat). (SingI t) + => () => O.Ordinal t -> O.Ordinal (Succ t) +pattern OS n = O.OS n + +{-$quasiquotes #quasiquoters# + + This section provides QuasiQuoter for ordinals. + Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT + checks boundary; with @'od'@, we can use literal with + boundary check. + For example, with @-XQuasiQuotes@ language extension enabled, + @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error, + whilst @12 :: Ordinal 1@ compiles but raises run-time error. + So, to enforce correctness, we recommend to use these quoters + instead of bare @'Num'@ numerals. +-} + +-- | Quasiquoter for ordinal indexed by GHC's built-n @'Data.Type.Natural.Nat'@. +-- +-- Since 0.7.0.0 +od :: QuasiQuoter +od = O.odLit +{-# INLINE od #-} + +-- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. +-- +-- Since 0.7.0.0 +sNatToOrd' :: (m :< n) ~ 'True => Sing n -> Sing m -> Ordinal n +sNatToOrd' = O.sNatToOrd' +{-# INLINE sNatToOrd' #-} + +-- | 'sNatToOrd'' with @n@ inferred. +-- +-- Since 0.7.0.0 +sNatToOrd :: (SingI n, (m :< n) ~ 'True) => Sing m -> Ordinal n +sNatToOrd = O.sNatToOrd +{-# INLINE sNatToOrd #-} + +-- | Convert ordinal into @Int@. +-- +-- Since 0.7.0.0 +ordToInt :: Ordinal n -> Integer +ordToInt = O.ordToInt +{-# INLINE ordToInt #-} + +unsafeFromInt :: SingI n + => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n +unsafeFromInt = O.unsafeFromInt +{-# INLINE unsafeFromInt #-} + +-- | Inclusion function for ordinals. +-- +-- Since 0.7.0.0 +inclusion :: (n :<= m) ~ 'True => Ordinal n -> Ordinal m +inclusion = O.inclusion +{-# INLINE inclusion #-} + +-- | Inclusion function for ordinals with codomain inferred. +-- +-- Since 0.7.0.0 +inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m +inclusion' = O.inclusion' +{-# INLINE inclusion' #-} + +-- | Ordinal addition. +-- +-- Since 0.7.0.0 +(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m) +(@+) = (O.@+) +{-# INLINE (@+) #-} + +-- | Enumerate all @'Ordinal'@s less than @n@. +-- +-- Since 0.7.0.0 +enumOrdinal :: Sing n -> [Ordinal n] +enumOrdinal = O.enumOrdinal +{-# INLINE enumOrdinal #-} + +-- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. +-- +-- Since 0.7.0.0 +absurdOrd :: Ordinal 'Z -> a +absurdOrd = O.absurdOrd +{-# INLINE absurdOrd #-} + +-- | @'absurdOrd'@ for values in 'Functor'. +-- +-- Since 0.7.0.0 +vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a +vacuousOrd = O.vacuousOrd +{-# INLINE vacuousOrd #-} diff --git a/Data/Type/Ordinal/Peano.hs b/Data/Type/Ordinal/Peano.hs new file mode 100644 --- /dev/null +++ b/Data/Type/Ordinal/Peano.hs @@ -0,0 +1,149 @@ +{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs #-} +{-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-} +-- | Module providing the same API as 'Data.Type.Ordinal' but specialised to +-- peano numeral @'Nat'@. +-- +-- Since 0.7.0.0 +module Data.Type.Ordinal.Peano + ( -- * Data-types and pattern synonyms + Ordinal, pattern OLt, pattern OZ, pattern OS, + -- * Quasi Quoter + -- $quasiquotes + od, + -- * Conversion from cardinals to ordinals. + sNatToOrd', sNatToOrd, ordToInt, + unsafeFromInt, inclusion, inclusion', + -- * Ordinal arithmetics + (@+), enumOrdinal, + -- * Elimination rules for @'Ordinal' 'Z'@. + absurdOrd, vacuousOrd + ) where +import Data.Kind +import Data.Singletons.Prelude (POrd (..), SingI, Sing (..)) +import Data.Singletons.Prelude.Enum (PEnum (..)) +import qualified Data.Type.Ordinal as O +import Data.Type.Natural +import Language.Haskell.TH.Quote (QuasiQuoter) +import Data.Type.Monomorphic + +-- | Set-theoretic (finite) ordinals: +-- +-- > n = {0, 1, ..., n-1} +-- +-- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. +-- This module exports a variant of polymorphic @'Data.Type.Ordinal.Ordinal'@ +-- specialised to Peano numeral @'Nat'@. +-- +-- Since 0.7.0.0 +type Ordinal (n :: Nat) = O.Ordinal n + +-- | We provide specialised version of constructor @'O.OLt'@ as type synonym @'OLt'@. +-- In some case, GHC warns about incomplete pattern using pattern @'OLt'@, +-- but it is due to the limitation of GHC's current exhaustiveness checker. +-- +-- Since 0.7.0.0 +pattern OLt :: () => forall (n1 :: Nat). ((n1 :< t) ~ 'True) + => Sing n1 -> O.Ordinal t +pattern OLt n = O.OLt n + +-- | Pattern synonym representing the 0-th ordinal. +-- +-- Since 0.7.0.0 +pattern OZ :: forall (n :: Nat). () + => ('Z :< n) ~ 'True => O.Ordinal n +pattern OZ = O.OZ + +-- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal. +-- +-- Since 0.7.0.0 +pattern OS :: forall (t :: Nat). (SingI t) + => () => O.Ordinal t -> O.Ordinal (Succ t) +pattern OS n = O.OS n + +{-$quasiquotes #quasiquoters# + + This section provides QuasiQuoter for ordinals. + Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT + checks boundary; with @'od'@, we can use literal with + boundary check. + For example, with @-XQuasiQuotes@ language extension enabled, + @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error, + whilst @12 :: Ordinal 1@ compiles but raises run-time error. + So, to enforce correctness, we recommend to use these quoters + instead of bare @'Num'@ numerals. +-} + +-- | Quasiquoter for ordinal indexed by Peano numeral @'Data.Type.Natural.Nat'@. +-- +-- Since 0.7.0.0 +od :: QuasiQuoter +od = O.odLit +{-# INLINE od #-} + +-- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. +-- +-- Since 0.7.0.0 +sNatToOrd' :: (m :< n) ~ 'True => Sing n -> Sing m -> Ordinal n +sNatToOrd' = O.sNatToOrd' +{-# INLINE sNatToOrd' #-} + +-- | 'sNatToOrd'' with @n@ inferred. +-- +-- Since 0.7.0.0 +sNatToOrd :: (SingI n, (m :< n) ~ 'True) => Sing m -> Ordinal n +sNatToOrd = O.sNatToOrd +{-# INLINE sNatToOrd #-} + +-- | Convert ordinal into @Int@. +-- +-- Since 0.7.0.0 +ordToInt :: Ordinal n -> Integer +ordToInt = O.ordToInt +{-# INLINE ordToInt #-} + +unsafeFromInt :: SingI n + => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n +unsafeFromInt = O.unsafeFromInt +{-# INLINE unsafeFromInt #-} + +-- | Inclusion function for ordinals. +-- +-- Since 0.7.0.0 +inclusion :: (n :<= m) ~ 'True => Ordinal n -> Ordinal m +inclusion = O.inclusion +{-# INLINE inclusion #-} + +-- | Inclusion function for ordinals with codomain inferred. +-- +-- Since 0.7.0.0 +inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m +inclusion' = O.inclusion' +{-# INLINE inclusion' #-} + +-- | Ordinal addition. +-- +-- Since 0.7.0.0 +(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m) +(@+) = (O.@+) +{-# INLINE (@+) #-} + +-- | Enumerate all @'Ordinal'@s less than @n@. +-- +-- Since 0.7.0.0 +enumOrdinal :: Sing n -> [Ordinal n] +enumOrdinal = O.enumOrdinal +{-# INLINE enumOrdinal #-} + +-- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. +-- +-- Since 0.7.0.0 +absurdOrd :: Ordinal 'Z -> a +absurdOrd = O.absurdOrd +{-# INLINE absurdOrd #-} + +-- | @'absurdOrd'@ for values in 'Functor'. +-- +-- Since 0.7.0.0 +vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a +vacuousOrd = O.vacuousOrd +{-# INLINE vacuousOrd #-} diff --git a/type-natural.cabal b/type-natural.cabal --- a/type-natural.cabal +++ b/type-natural.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural -version: 0.6.1.1 +version: 0.7.0.0 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties. . @@ -31,6 +31,8 @@ ghc-options: -Wno-redundant-constraints exposed-modules: Data.Type.Natural , Data.Type.Ordinal + , Data.Type.Ordinal.Builtin + , Data.Type.Ordinal.Peano , Data.Type.Natural.Builtin , Data.Type.Natural.Class , Data.Type.Natural.Class.Arithmetic