[commit: base] master: Add unary natural numbers to experiment on matching with literals. (792f6df)

[Iavor Diatchki]

Repository : ssh://darcs.haskell.org//srv/darcs/packages/base

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/792f6df69e5e178da5a52f0db37f1453f11d8cb5

>---------------------------------------------------------------

commit 792f6df69e5e178da5a52f0db37f1453f11d8cb5
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sat Sep 29 14:52:35 2012 -0700

    Add unary natural numbers to experiment on matching with literals.
    
    The idea is that when we want to match on type level nats, we should
    use `Nat1`, and use the `FromNat1` function to switch between the
    structured and unstructured representation of numbers.
    
    A bit of custom machinery is needed for this to work properly,
    because to go back (i.e., to solve FromNat1 x ~ 3) GHC needs to know
    that FromNat1 is an injective function.

>---------------------------------------------------------------

 GHC/TypeLits.hs |   16 +++++++++++++++-
 1 files changed, 15 insertions(+), 1 deletions(-)

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index e5ab346..c0a3017 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -31,9 +31,12 @@ module GHC.TypeLits
     -- * Functions on type nats
   , type (<=), type (<=?), type (+), type (*), type (^)
 
-    -- * Destructing type-nats.
+    -- * Destructing type-nat singletons.
   , isZero, IsZero(..)
   , isEven, IsEven(..)
+
+    -- * Matching on type-nats
+  , Nat1(..), FromNat1
   ) where
 
 import GHC.Base(Eq((==)), Bool(..), ($), otherwise, (.))
@@ -186,3 +189,14 @@ instance Show (IsEven n) where
   show (IsOdd  x) = "(2 * " ++ show x ++ " + 1)"
 
 
+--------------------------------------------------------------------------------
+
+-- | Unary implemenation of natural numbers.
+-- 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
+
+