type-natural 0.0.3.0 → 0.0.4.0

raw patch · 2 files changed

+85/−2 lines, 2 files

Files

• Data/Type/Ordinal.hs +83/−0
• type-natural.cabal +2/−2

@@ -0,0 +1,83 @@+{-# LANGUAGE DataKinds, EmptyDataDecls, FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE GADTs, KindSignatures, PolyKinds, StandaloneDeriving           #-}+{-# LANGUAGE TypeFamilies, TypeOperators                                    #-}+-- | Set-theoretic ordinal arithmetic+module Data.Type.Ordinal+       ( -- * Data-types+         Ordinal (..),+         -- * Conversion from cardinals to ordinals.+         sNatToOrd', sNatToOrd, ordToInt, ordToSNat,+         -- * Ordinal arithmetics+         (@+)+       ) where+import Data.Type.Monomorphic+import Data.Type.Natural++-- | Set-theoretic (finite) ordinals:+--+-- > n = {0, 1, ..., n-1}+--+-- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal Z@ is isomorphic to @Void@.+data Ordinal n where+  OZ :: Ordinal (S n)+  OS :: Ordinal n -> Ordinal (S n)++-- | Parsing always fails, because there are no inhabitant.+instance Read (Ordinal Z) where+  readsPrec _ _ = []++deriving instance Read (Ordinal n) => Read (Ordinal (S n))+deriving instance Show (Ordinal n)+deriving instance Eq (Ordinal n)+deriving instance Ord (Ordinal n)++-- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.+sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal n+sNatToOrd' (SS _) SZ = OZ+sNatToOrd' (SS n) (SS m) = OS $ sNatToOrd' n m+sNatToOrd' _ _ = bugInGHC++-- | 'sNatToOrd'' with @n@ inferred.+sNatToOrd :: (SingRep n, (S m :<<= n) ~ True) => SNat m -> Ordinal n+sNatToOrd = sNatToOrd' sing++-- | Convert @Ordinal n@ into monomorphic @SNat@+ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)+ordToSNat OZ = Monomorphic SZ+ordToSNat (OS n) =+  case ordToSNat n of+    Monomorphic sn ->+      case singInstance sn of+        SingInstance -> Monomorphic (SS sn)++-- | Convert ordinal into @Int@.+ordToInt :: Ordinal n -> Int+ordToInt OZ = 0+ordToInt (OS n) = 1 + ordToInt n++-- | Inclusion function for ordinals.+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' _ _ = bugInGHC++-- | Inclusion function for ordinals with codomain inferred.+inclusion :: ((n :<<= m) ~ True, SingRep m) => Ordinal n -> Ordinal m+inclusion = inclusion' sing++-- | Ordinal addition.+(@+) :: forall n m. (SingRep n, SingRep m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)+OZ @+ n =+  let sn = sing :: SNat n+      sm = sing :: SNat m+  in case singInstance (sn %+ sm) of+       SingInstance ->+         case propToBoolLeq (plusLeqR sn sm) of+           LeqTrueInstance -> inclusion n+OS n @+ m =+  case sing :: SNat n of+    SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m+    _ -> bugInGHC+

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.0.3.0+version:             0.0.4.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@@ -20,7 +20,7 @@   library-  exposed-modules:     Data.Type.Natural+  exposed-modules:     Data.Type.Natural, Data.Type.Ordinal   -- other-modules:          build-depends:       base                     == 4.6.*                ,       singletons               == 0.8.*