Repository : ssh://darcs.haskell.org//srv/darcs/packages/base On branch : type-nats
http://hackage.haskell.org/trac/ghc/changeset/b56b66baf9b83aa53a4e0a0b96ce4ab489c1d5ef >--------------------------------------------------------------- commit b56b66baf9b83aa53a4e0a0b96ce4ab489c1d5ef Author: Iavor S. Diatchki <[email protected]> Date: Thu Dec 29 17:57:29 2011 -0800 Remove all but the basics from the GHC module. In this way we can work on the programmer library without having to recompile all libraries. >--------------------------------------------------------------- GHC/TypeNats.hs | 176 ++++++++---------------------------------------------- 1 files changed, 26 insertions(+), 150 deletions(-) diff --git a/GHC/TypeNats.hs b/GHC/TypeNats.hs index 4aefa55..e86c4b6 100644 --- a/GHC/TypeNats.hs +++ b/GHC/TypeNats.hs @@ -1,57 +1,49 @@ -{-# LANGUAGE TypeNaturals #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE CPP #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE EmptyDataDecls #-} {-# OPTIONS_GHC -XNoImplicitPrelude #-} +{-| This module is an internal GHC module. It declares the constants used +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 - , NatI() - , nat - , natToInteger - , checkNat - - -- * Type-Level Operations - , type (<=) (+) (*) (^) - - -- * Natural Numbers - , Natural(..) - , NaturalInteger(..) - , toNaturalInteger - , subNatural + , NatS(..) + , NatI(..) + , (:<=), (:+), (:*), (:^) ) where -#ifdef __GLASGOW_HASKELL__ -import GHC.Base -import Data.Maybe (Maybe(..), fromMaybe) -import GHC.Num (Integer, Num(..)) -import GHC.Real (Integral(..), Real(..)) -import GHC.Enum (Enum(..)) -import GHC.Show (Show(..)) -import GHC.Read (Read(..)) -#endif +import GHC.Integer(Integer) +-- | This is the *kind* of type-level natural numbers. +data Nat -- | Comparsion of type-level naturals. -class (m :: Nat) <= (n :: Nat) +class (m :: Nat) :<= (n :: Nat) -- | Addition of type-level naturals. -type family (m :: Nat) + (n :: Nat) :: Nat +type family (m :: Nat) :+ (n :: Nat) :: Nat -- | Multiplication of type-level naturals. -type family (m :: Nat) * (n :: Nat) :: Nat +type family (m :: Nat) :* (n :: Nat) :: Nat -- | Exponentiation of type-level naturals. -type family (m :: Nat) ^ (n :: Nat) :: Nat +type family (m :: Nat) :^ (n :: Nat) :: Nat --- | The type @Nat n@ is m \"singleton\" type containing only the value @n@. --- (Technically, there is also m bottom element). +-- | The type @NatS 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. -newtype Nat (n :: Nat) = Nat Integer +newtype NatS (n :: Nat) = NatS Integer --- NOTE: The instances for "NatI" are provided directly by GHC. +-- | The class 'NatI' provides a \"smart\" constructor for values +-- of type @Nat n@. There are built-in instances for all natural numbers. +-- +-- NOTE: The instances for 'NatI' are provided directly by GHC. -- The built-in instances use the integer corresponding to the instance -- as evidence. This works because of the following two details about GHC: -- * The "dictionary" for classes with a single method is the method itself, @@ -60,126 +52,10 @@ newtype Nat (n :: Nat) = Nat Integer -- (This is a bit of a hack but it seems to work pretty well. -- It is also possible to implement the same API in a different way.) --- | The class 'NatI' provides a \"smart\" constructor for values --- of type @Nat n@. There are built-in instances for all natural numbers. class NatI (n :: Nat) where -- | The only defined element of type @Nat n@. - nat :: Nat n - --- | The integer value corresponding to a type-level natural. -natToInteger :: Nat n -> Integer -natToInteger (Nat x) = x - - --- Natural numbers ------------------------------------------------------------- - --- | The type of natural numbers. -data Natural = forall n. Natural !(Nat n) - - -instance Show Natural where - showsPrec p n = showsPrec p (n2i n) - -instance Read Natural where - readsPrec p s = do (x,xs) <- readsPrec p s - case toNaturalInteger x of - NonNegative n -> [(n,xs)] - Negative _ -> [] - -instance Eq Natural where - x == y = n2i x == n2i y - -instance Ord Natural where - compare x y = compare (n2i x) (n2i y) - -instance Num Natural where - x + y = _i2n (n2i x + n2i y) - x * y = _i2n (n2i x * n2i y) - x - y = _ni2n (subNatural x y) - abs = id - signum x = _i2n (signum (n2i x)) - fromInteger x = _ni2n (toNaturalInteger x) - -instance Enum Natural where - succ x = _i2n (1 + n2i x) - pred x = _ni2n (toNaturalInteger (n2i x - 1)) - toEnum x = if x < 0 then error msg else _i2n (toEnum x) - where msg = "toEnum @ Natural: -ve number" - fromEnum x = fromEnum (n2i x) - - enumFrom x = map _i2n (enumFrom (n2i x)) - enumFromTo x y = map _i2n (enumFromTo (n2i x) (n2i y)) - enumFromThen x y - | x <= y = map _i2n (enumFromThen (n2i x) (n2i y)) - | otherwise = map _i2n (enumFromThenTo (n2i x) (n2i y) 0) - enumFromThenTo x y z = map _i2n (enumFromThenTo (n2i x) (n2i y) (n2i z)) - -instance Real Natural where - toRational x = toRational (n2i x) - -instance Integral Natural where - toInteger x = n2i x - -- Perhaps this could be made more efficient because we only - -- deal with non -ve values? Also, quot/div should be the same. - quotRem x y = case quotRem (n2i x) (n2i y) of - (a,b) -> (_i2n a, _i2n b) - divMod x y = case divMod (n2i x) (n2i y) of - (a,b) -> (_i2n a, _i2n b) - - - --- | Integers defined in terms of natural numbers. --- This is a convenience type used to convert 'Integer' to 'Natural' values. -data NaturalInteger = Negative Natural | NonNegative Natural deriving Show - --- | Convert an integer into a natural number. -toNaturalInteger :: Integer -> NaturalInteger -toNaturalInteger x - | x >= 0 = NonNegative (_i2n x) - | otherwise = Negative (_i2n (negate x)) - --- | Subtract two natural numbers. -subNatural :: Natural -> Natural -> NaturalInteger -subNatural x y = toNaturalInteger (n2i x - n2i y) - - - - --- The functions bellow are derived -------------------------------------------- - - - -instance Show (Nat n) where - showsPrec p n = showsPrec p (natToInteger n) - -instance NatI n => Read (Nat n) where - readsPrec p x = do (x,xs) <- readsPrec p x - case checkNat (x ==) of - Just n -> [(n,xs)] - Nothing -> [] - --- | Returns @Just n@ if, and only if, @natToInteger n@ satisfies the --- given predicate. -checkNat :: NatI n => (Integer -> Bool) -> Maybe (Nat n) -checkNat p = check nat - where check y = if p (natToInteger y) then Just y else Nothing - - --- PRIVATE --------------------------------------------------------------------- - --- Private. Used just for the short name. --- Exported as 'toInteger' in class 'Integral'. -n2i :: Natural -> Integer -n2i (Natural x) = natToInteger x - --- Private. Used only when we know that the integer is positive. -_i2n :: Integer -> Natural -_i2n x = Natural (Nat x) + natS :: NatS n --- Priavte. Turns -ve numbers into undefined elements. -_ni2n :: NaturalInteger -> Natural -_ni2n (NonNegative x) = x -_ni2n (Negative x) = error ("Negative natural number: -" ++ show x) _______________________________________________ Cvs-libraries mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-libraries
