tfp 1.0.0.2 → 1.0.1
raw patch · 8 files changed
+192/−76 lines, 8 files
Files
- CHANGES +0/−19
- Changes.md +19/−0
- src/Type/Base/Proxy.hs +12/−0
- src/Type/Data/Num.hs +19/−4
- src/Type/Data/Num/Decimal/Number.hs +13/−0
- src/Type/Data/Num/Unary.hs +18/−1
- src/Type/Data/Num/Unary/Proof.hs +107/−48
- tfp.cabal +4/−4
− CHANGES
@@ -1,19 +0,0 @@-1.0:--* Change representation of decimals to an inherently normalized form- that is symmetric with respect to positive and negative numbers.--* singularize module names--* separate Decimal and general representation--* use Proxys instead of plain types for data functions- This is also consistent with new Nat kind,- where types of kind Nat have no data values.--* Ord: make infix operators classes and prefix functions type functions- It seems to be more natural to me to write- x :<: y and GTT x y ~ True--* Num, Bool, Ord: remove T suffixes from functions- Use qualification instead.
+ Changes.md view
@@ -0,0 +1,19 @@+1.0:++* Change representation of decimals to an inherently normalized form+ that is symmetric with respect to positive and negative numbers.++* singularize module names++* separate Decimal and general representation++* use Proxys instead of plain types for data functions+ This is also consistent with new Nat kind,+ where types of kind Nat have no data values.++* Ord: make infix operators classes and prefix functions type functions+ It seems to be more natural to me to write+ x :<: y and GTT x y ~ True++* Num, Bool, Ord: remove T suffixes from functions+ Use qualification instead.
src/Type/Base/Proxy.hs view
@@ -2,7 +2,12 @@ import Control.Applicative (Applicative, pure, (<*>), ) +import qualified Prelude as P+import Prelude (String, Eq, Functor, fmap)++ data Proxy a = Proxy+ deriving (Eq) instance Functor Proxy where fmap _f Proxy = Proxy@@ -10,3 +15,10 @@ instance Applicative Proxy where pure _ = Proxy Proxy <*> Proxy = Proxy+++class Show a where+ showsPrec :: P.Int -> Proxy a -> P.ShowS++instance Show a => P.Show (Proxy a) where+ showsPrec = showsPrec
src/Type/Data/Num.hs view
@@ -55,6 +55,10 @@ , Natural , Positive , Negative+ , integerFromSingleton+ , integralFromSingleton+ , singletonFromProxy+ , integralFromProxy , fromInteger , reifyPositive , reifyNegative@@ -184,10 +188,21 @@ newtype Singleton d = Singleton P.Integer -fromInteger :: forall x y. (Integer x, Num y) => Proxy x -> y-fromInteger _ =- case singleton :: Singleton x of- Singleton n -> P.fromInteger n+integerFromSingleton :: (Integer x) => Singleton x -> P.Integer+integerFromSingleton (Singleton n) = n++integralFromSingleton :: (Integer x, Num y) => Singleton x -> y+integralFromSingleton = P.fromInteger . integerFromSingleton++singletonFromProxy :: (Integer x) => Proxy x -> Singleton x+singletonFromProxy Proxy = singleton++integralFromProxy :: (Integer x, Num y) => Proxy x -> y+integralFromProxy = integralFromSingleton . singletonFromProxy++-- | synonym for 'integralFromProxy', kept for backward compatibility+fromInteger :: (Integer x, Num y) => Proxy x -> y+fromInteger = integralFromProxy --- positive and negative assertions: unsafe, in a trusted kernel
src/Type/Data/Num/Decimal/Number.hs view
@@ -35,6 +35,7 @@ import qualified Type.Data.Num.Unary as Unary import qualified Type.Data.Num as Op import qualified Type.Data.Ord as Ord+import qualified Type.Base.Proxy as Proxy import Type.Data.Num.Decimal.Digit (Dec0, Dec1, Dec2, Dec3, Dec4, Dec5, Dec6, Dec7, Dec8, Dec9)@@ -46,6 +47,8 @@ import Data.Tuple.HT (swap) import qualified Data.List as List +import Text.Printf (printf)+ import qualified Prelude as P import Prelude hiding (Integer) @@ -97,6 +100,16 @@ decimal :: Proxy n -> Proxy (Dec n) decimal Proxy = Proxy++stripDec :: Proxy (Dec n) -> Proxy n+stripDec Proxy = Proxy+++instance Integer a => Proxy.Show (Dec a) where+ showsPrec prec =+ (\n -> showParen (prec>10) (showString (printf "decimal d%d" n)))+ . integerFromSingleton . singletonFromProxy . stripDec+ reifyIntegral :: P.Integer -> (forall s. Integer s => Proxy s -> w) -> w reifyIntegral n f =
src/Type/Data/Num/Unary.hs view
@@ -3,16 +3,21 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Type.Data.Num.Unary (- Unary, Un, Zero, Succ, zero, succ,+ Unary, unary, Un, Zero, Succ, zero, succ, Singleton(..), singleton, singletonFromProxy, integerFromSingleton, integralFromSingleton,+ integralFromProxy, Natural(..), Positive(..), (:+:), (:*:),+ reifyNatural, ) where import qualified Type.Data.Num as Num+import qualified Type.Base.Proxy as Proxy import Type.Base.Proxy (Proxy(Proxy)) +import Text.Printf (printf)+ import Prelude hiding (succ) @@ -96,13 +101,19 @@ singletonFromProxy :: (Natural n) => Proxy n -> Singleton n singletonFromProxy Proxy = singleton +integralFromProxy :: (Natural n, Num a) => Proxy n -> a+integralFromProxy = integralFromSingleton . singletonFromProxy + instance Num.Representation Unary where reifyIntegral _ i k = reifyIntegral i (k . unary) unary :: Proxy n -> Proxy (Un n) unary Proxy = Proxy +stripUn :: Proxy (Un n) -> Proxy n+stripUn Proxy = Proxy+ reifyIntegral :: Integer -> (forall s. Natural s => Proxy s -> w) -> w reifyIntegral n f = if n < 0@@ -118,3 +129,9 @@ type instance Un x Num.:+: Un y = Un (x :+: y) type instance Un x Num.:*: Un y = Un (x :*: y)+++instance Natural a => Proxy.Show (Un a) where+ showsPrec prec =+ (\n -> showParen (prec>10) (showString (printf "unary u%d" n)))+ . integerFromSingleton . singletonFromProxy . stripUn
src/Type/Data/Num/Unary/Proof.hs view
@@ -1,15 +1,19 @@ {-# LANGUAGE TypeOperators #-}-{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Rank2Types #-} {-# LANGUAGE FlexibleContexts #-} module Type.Data.Num.Unary.Proof ( Nat(..), Pos(..), natFromPos, addNat, addPosL, addPosR,+ AddZeroL(..), addZeroL,+ AddComm(..), addComm,+ AddAssoc(..), addAssoc, mulNat, mulPos, ) where import Type.Data.Num.Unary- (Natural, Positive, Succ, switchNat, switchPos, (:+:), (:*:))+ (Natural, Positive, Zero, Succ, switchNat, switchPos, (:+:), (:*:)) data Nat x = Natural x => Nat data Pos x = Positive x => Pos@@ -33,76 +37,131 @@ newtype- AddNatTheorem x y =- AddNatTheorem {- runAddNatTheorem :: Nat x -> Nat y -> Nat (x :+: y)- }+ QuantifiedAdd condx condy prop x y =+ QuantifiedAdd {runQuantifiedAdd :: condx x -> condy y -> prop (x :+: y)} addNat :: Nat x -> Nat y -> Nat (x :+: y) addNat x0 y0@Nat =- runAddNatTheorem+ runQuantifiedAdd (switchNat- (AddNatTheorem $ \Nat Nat -> Nat)- (AddNatTheorem $ \x -> succNat . addNat x . prevNat))+ (QuantifiedAdd const)+ (QuantifiedAdd $ \x -> succNat . addNat x . prevNat)) x0 y0 --newtype- AddPosRTheorem x y =- AddPosRTheorem {- runAddPosRTheorem :: Nat x -> Pos y -> Pos (x :+: y)- }- addPosR :: Nat x -> Pos y -> Pos (x :+: y) addPosR x0 y0@Pos =- runAddPosRTheorem- (switchPos- (AddPosRTheorem $ \x ->- posSucc . addNat x . prevPos))+ runQuantifiedAdd+ (switchPos (QuantifiedAdd $ \x -> posSucc . addNat x . prevPos)) x0 y0 --newtype- AddPosLTheorem x y =- AddPosLTheorem {- runAddPosLTheorem :: Pos x -> Nat y -> Pos (x :+: y)- }- addPosL :: Pos x -> Nat y -> Pos (x :+: y) addPosL x0 y0@Nat =- runAddPosLTheorem+ runQuantifiedAdd (switchNat- (AddPosLTheorem $ \x _y -> x)- (AddPosLTheorem $ \x ->- posSucc . addNat (natFromPos x) . prevNat))+ (QuantifiedAdd const)+ (QuantifiedAdd $ \x -> posSucc . addNat (natFromPos x) . prevNat)) x0 y0 +newtype Quantified prop x = Quantified {runQuantified :: Nat x -> prop x}++induction ::+ quant Zero -> (forall x. Nat x -> quant (Succ x)) ->+ Nat y -> quant y+induction base step y@Nat =+ runQuantified+ (switchNat+ (Quantified $ const base)+ (Quantified $ step . prevNat))+ y+++data AddZeroL x = (Zero:+:x) ~ x => AddZeroL++succZeroL :: AddZeroL x -> AddZeroL (Succ x)+succZeroL AddZeroL = AddZeroL++addZeroL :: Nat x -> AddZeroL x+addZeroL = induction AddZeroL (succZeroL . addZeroL)+++{-+induction step:++Succ x :+: Succ y+Succ (x :+: Succ y)+Succ (Succ (x:+:y))+Succ (Succ x :+: y)+-}+data AddSuccL x y = (Succ x :+: y) ~ Succ (x:+:y) => AddSuccL++succSuccL :: AddSuccL x y -> AddSuccL x (Succ y)+succSuccL AddSuccL = AddSuccL++addSuccL :: Nat x -> Nat y -> AddSuccL x y+addSuccL x =+ induction+ (case addZeroL x of AddZeroL -> AddSuccL)+ (succSuccL . addSuccL x)+++{-+induction step:++y :+: Succ x+Succ (y :+: x)+Succ (x :+: y)+Succ x :+: y+-}+data AddComm x y = (x:+:y) ~ (y:+:x) => AddComm++succComm :: Nat x -> Nat y -> AddComm x y -> AddComm x (Succ y)+succComm x y AddComm = case addSuccL y x of AddSuccL -> AddComm++{- |+The proof is pretty expensive.+For proving (x:+:y ~ y:+:x) we need about @x*y@ reduction steps.+-}+addComm :: Nat x -> Nat y -> AddComm x y+addComm x =+ induction+ (case addZeroL x of AddZeroL -> AddComm)+ (\y -> succComm x y $ addComm x y)+++{-+induction step:++x :+: (y :+: Succ z)+x :+: Succ (y :+: z)+Succ (x :+: (y :+: z))+Succ ((x :+: y) :+: z)+(x :+: y) :+: Succ z+-}+data AddAssoc x y z = (x:+:(y:+:z)) ~ ((x:+:y):+:z) => AddAssoc++succAssoc :: AddAssoc x y z -> AddAssoc x y (Succ z)+succAssoc AddAssoc = AddAssoc++addAssoc :: Nat x -> Nat y -> Nat z -> AddAssoc x y z+addAssoc x y = induction AddAssoc (succAssoc . addAssoc x y)++ newtype- MulNatTheorem x y =- MulNatTheorem {- runMulNatTheorem :: Nat x -> Nat y -> Nat (x :*: y)- }+ QuantifiedMul condx condy prop x y =+ QuantifiedMul {runQuantifiedMul :: condx x -> condy y -> prop (x :*: y)} mulNat :: Nat x -> Nat y -> Nat (x :*: y) mulNat x0 y0@Nat =- runMulNatTheorem+ runQuantifiedMul (switchNat- (MulNatTheorem $ \Nat Nat -> Nat)- (MulNatTheorem $ \x -> addNat x . mulNat x . prevNat))+ (QuantifiedMul $ \Nat Nat -> Nat)+ (QuantifiedMul $ \x -> addNat x . mulNat x . prevNat)) x0 y0 --newtype- MulPosTheorem x y =- MulPosTheorem {- runMulPosTheorem :: Pos x -> Pos y -> Pos (x :*: y)- }- mulPos :: Pos x -> Pos y -> Pos (x :*: y) mulPos x0 y0@Pos =- runMulPosTheorem+ runQuantifiedMul (switchPos- (MulPosTheorem $ \x ->- addPosL x . mulNat (natFromPos x) . prevPos))+ (QuantifiedMul $ \x -> addPosL x . mulNat (natFromPos x) . prevPos)) x0 y0
tfp.cabal view
@@ -1,5 +1,5 @@ name: tfp-version: 1.0.0.2+version: 1.0.1 build-type: Simple license: BSD3 license-file: LICENSE@@ -18,16 +18,16 @@ and functions on numerical values at compile time. category: Type System tested-with: GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.4, GHC == 8.0.1-cabal-version: >= 1.14+cabal-version: 1.14 extra-source-files:- CHANGES+ Changes.md source-repository head type: darcs location: http://hub.darcs.net/thielema/tfp/ source-repository this- tag: 1.0.0.2+ tag: 1.0.1 type: darcs location: http://hub.darcs.net/thielema/tfp/