Add type functions (-) and ToNat1; Turn FromNat1 into a closed family.
authorIavor S. Diatchki <iavor.diatchki@gmail.com>
Tue, 24 Sep 2013 13:22:54 +0000 (06:22 -0700)
committerIavor S. Diatchki <iavor.diatchki@gmail.com>
Tue, 24 Sep 2013 13:22:54 +0000 (06:22 -0700)
libraries/base/GHC/TypeLits.hs

index 3f95646..d6eba25 100644 (file)
@@ -31,7 +31,7 @@ module GHC.TypeLits
   , withSing, singThat
 
     -- * Functions on type nats
-  , type (<=), type (<=?), type (+), type (*), type (^)
+  , type (<=), type (<=?), type (+), type (*), type (^), type (-)
 
     -- * Comparing for equality
   , type (:~:) (..), eqSingNat, eqSingSym, eqSingBool
@@ -44,7 +44,7 @@ module GHC.TypeLits
 
 
     -- * Matching on type-nats
-  , Nat1(..), FromNat1
+  , Nat1(..), FromNat1, ToNat1
 
     -- * Kind parameters
   , KindIs(..), Demote, DemoteRep
@@ -124,7 +124,8 @@ type family (m :: Nat) * (n :: Nat) :: Nat
 -- | Exponentiation of type-level naturals.
 type family (m :: Nat) ^ (n :: Nat) :: Nat
 
-
+-- | Subtraction of type-level naturals.
+type family (m :: Nat) - (n :: Nat) :: Nat
 
 
 --------------------------------------------------------------------------------
@@ -312,9 +313,13 @@ instance Show (IsEven n) where
 -- Used both at the type and at the value level.
 data Nat1 = Zero | Succ Nat1
 
-type family FromNat1 (n :: Nat1) :: Nat
-type instance FromNat1 Zero     = 0
-type instance FromNat1 (Succ n) = 1 + FromNat1 n
+type family ToNat1 (n :: Nat) where
+  ToNat1 0 = Zero
+  ToNat1 x = Succ (ToNat1 (x - 1))
+
+type family FromNat1 (n :: Nat1) :: Nat where
+  FromNat1 Zero     = 0
+  FromNat1 (Succ n) = 1 + FromNat1 n
 
 --------------------------------------------------------------------------------