Repository : ssh://darcs.haskell.org//srv/darcs/packages/base On branch : type-nats
http://hackage.haskell.org/trac/ghc/changeset/92768c08d06d837611c8354830e1875ddc2a57fc >--------------------------------------------------------------- commit 92768c08d06d837611c8354830e1875ddc2a57fc Author: Iavor S. Diatchki <[email protected]> Date: Tue Jan 24 22:12:34 2012 -0800 Rename GHC.TypeNats to GHC.TypeList, cleanup, add type-level strings. >--------------------------------------------------------------- GHC/{TypeNats.hs => TypeLits.hs} | 74 ++++++++++++++++++++++++++------------ base.cabal | 2 +- 2 files changed, 52 insertions(+), 24 deletions(-) diff --git a/GHC/TypeNats.hs b/GHC/TypeLits.hs similarity index 60% rename from GHC/TypeNats.hs rename to GHC/TypeLits.hs index 11932f6..707df69 100644 --- a/GHC/TypeNats.hs +++ b/GHC/TypeLits.hs @@ -9,38 +9,45 @@ in the implementation of type-level natural numbers. The programmer interface for workin with type-level naturals should be defined in a separate library. -} -module GHC.TypeNats - ( -- * Basic Types - Nat - , NatS(..) - , NatI(..) - , (:<=), (:+), (:*), (:^) +module GHC.TypeLits + ( -- * Kinds + Nat, Symbol + + -- * Singleton type + , TNat(..), TSymbol(..) + + -- * Linking type nad value level + , NatI(..), SymbolI(..) + + -- * Functions on type nats + , type (<=), type (+), type (*), type (^) ) where -import GHC.Word(Word) +import GHC.Num(Integer) +import GHC.Base(String) -- | This is the *kind* of type-level natural numbers. data Nat --- | Comparsion of type-level naturals. -class (m :: Nat) :<= (n :: Nat) - --- | Addition of type-level naturals. -type family (m :: Nat) :+ (n :: Nat) :: Nat - --- | Multiplication of type-level naturals. -type family (m :: Nat) :* (n :: Nat) :: Nat +-- | This is the *kind* of type-level symbols. +data Symbol --- | Exponentiation of type-level naturals. -type family (m :: Nat) :^ (n :: Nat) :: Nat +-------------------------------------------------------------------------------- --- | The type @NatS n@ is m \"singleton\" type containing only the value @n@. +-- | The type @TNat n@ is m \"singleton\" type containing only the value @n@. -- (Technically, there is also a bottom element). -- This type relates type-level naturals to run-time values. --- NOTE: For the moment we support only singleton types that can fit in --- a 'Word'. -newtype NatS (n :: Nat) = NatS Word +newtype TNat (n :: Nat) = TNat Integer + +-- | The type @TSymbol s@ is m \"singleton\" type containing only the value @s@. +-- (Technically, there is also a bottom element). +-- This type relates type-level symbols to run-time values. +newtype TSymbol (n :: Symbol) = TSymbol String + + + +-------------------------------------------------------------------------------- -- | The class 'NatI' provides a \"smart\" constructor for values -- of type @Nat n@. There are built-in instances for all natural numbers @@ -60,8 +67,29 @@ newtype NatS (n :: Nat) = NatS Word class NatI (n :: Nat) where - -- | The only defined element of type @Nat n@. - natS :: NatS n + -- | The only defined element of type @TNat n@. + tNat :: TNat n +class SymbolI (n :: Symbol) where + + -- | The only defined element of type @TSymbol n@. + tSymbol :: TSymbol n + + + + +-- | Comparsion of type-level naturals. +class (m :: Nat) <= (n :: Nat) + +-- | Addition of type-level naturals. +type family (m :: Nat) + (n :: Nat) :: Nat + +-- | Multiplication of type-level naturals. +type family (m :: Nat) * (n :: Nat) :: Nat + +-- | Exponentiation of type-level naturals. +type family (m :: Nat) ^ (n :: Nat) :: Nat + + diff --git a/base.cabal b/base.cabal index 6d15db3..bbe5a99 100644 --- a/base.cabal +++ b/base.cabal @@ -98,7 +98,7 @@ Library { GHC.Stable, GHC.Storable, GHC.STRef, - GHC.TypeNats, + GHC.TypeLits, GHC.TopHandler, GHC.Unicode, GHC.Weak, _______________________________________________ Cvs-libraries mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-libraries
