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 <[email protected]> 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 + + _______________________________________________ Cvs-libraries mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-libraries
