reflection 0.1.1 → 0.2.0
raw patch · 2 files changed
+140/−82 lines, 2 filesdep ~base
Dependency ranges changed: base
Files
- Data/Reflection.hs +134/−77
- reflection.cabal +6/−5
Data/Reflection.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE KindSignatures, RankNTypes, ScopedTypeVariables, EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-}+{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TypeOperators #-} ---------------------------------------------------------------------------- -- |@@ -10,33 +10,34 @@ -- Stability : experimental -- Portability : non-portable (scoped types, MPTCs, rank-n, FFI, kinds) ----- Implementation of the Functional Pearl: Implicit Configurations paper by+-- Based on the Functional Pearl: Implicit Configurations paper by -- Oleg Kiselyov and Chung-chieh Shan. -- -- <http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf> ----- Packaged and updated to work with the current implementation of scoped type --- variables by Edward Kmett.+-- Modified to work with an applicative phantom type parameter rather than +-- explicit scope type variables by Edward Kmett. -- ------------------------------------------------------------------------------- module Data.Reflection ( -- * Reflect Integrals- ReflectedNum+ ReifiesNum , reflectNum , reifyIntegral -- * Reflect Lists of Integrals- , ReflectedNums+ , ReifiesNums , reifyIntegrals -- * Reflect Storables- , ReflectedStorable+ , ReifiesStorable , reflectStorable , reifyStorable -- * Reflect Anything- , Reflects+ , Reifies , reflect , reify+ , Tagged(..) ) where import Foreign.C.Types@@ -47,101 +48,157 @@ import Foreign.StablePtr import Foreign.Storable import System.IO.Unsafe+import Control.Applicative +import Prelude hiding (succ, pred) -data Zero-data Twice s-data Succ s-data Pred s+class Unused t where unused :: t -> () -class ReflectedNum s where- reflectNum :: Num a => s -> a+newtype Tagged a b = Tagged { unTagged :: b } deriving (Eq,Ord,Show,Read)+type Retag f g = forall b. Tagged g b -> Tagged f b -instance ReflectedNum Zero where- reflectNum _ = 0+instance Functor (Tagged a) where + fmap f (Tagged x) = Tagged (f x)+ {-# INLINE fmap #-} -instance ReflectedNum s => ReflectedNum (Twice s) where- reflectNum _ = reflectNum (undefined :: s) * 2+instance Applicative (Tagged a) where+ pure = Tagged+ {-# INLINE pure #-}+ Tagged f <*> Tagged x = Tagged (f x)+ {-# INLINE (<*>) #-} -instance ReflectedNum s => ReflectedNum (Succ s) where- reflectNum _ = reflectNum (undefined :: s) + 1+instance Monad (Tagged a) where+ return = Tagged+ {-# INLINE return #-}+ Tagged m >>= k = k m + {-# INLINE (>>=) #-}+ _ >> n = n+ {-# INLINE (>>) #-} -instance ReflectedNum s => ReflectedNum (Pred s) where- reflectNum _ = reflectNum (undefined :: s) - 1+newtype Zero = Zero Zero deriving (Show)+newtype Twice s = Twice (Twice s) deriving (Show)+newtype Succ s = Succ (Succ s) deriving (Show)+newtype Pred s = Pred (Pred s) deriving (Show)+instance Unused Zero where unused Zero{} = ()+instance Unused (Twice s) where unused Twice{} = ()+instance Unused (Succ s) where unused Succ{} = ()+instance Unused (Pred s) where unused Pred{} = () -reifyIntegral :: Integral a => a -> (forall s. ReflectedNum s => s -> w) -> w-reifyIntegral i k = case quotRem i 2 of- (0, 0) -> k (undefined :: Zero)- (j, 0) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Twice s))- (j, 1) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Succ (Twice s)))- (j,-1) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Pred (Twice s)))- _ -> undefined+retag :: Retag f g+retag = Tagged . unTagged +{-# INLINE retag #-} -data Nil-data Cons s ss+pop :: Retag (f s) s+pop = retag+{-# INLINE pop #-} -class ReflectedNums ss where- reflectNums :: Num a => ss -> [a]+class ReifiesNum s where+ reflectNum :: Num a => Tagged s a -instance ReflectedNums Nil where- reflectNums _ = []+instance ReifiesNum Zero where+ reflectNum = pure 0 -instance (ReflectedNum s, ReflectedNums ss) => ReflectedNums (Cons s ss) where- reflectNums _ = reflectNum (undefined :: s) : reflectNums (undefined :: ss)+instance ReifiesNum s => ReifiesNum (Twice s) where+ reflectNum = (2*) <$> pop reflectNum -reifyIntegrals :: Integral a => [a] -> (forall ss. ReflectedNums ss => ss -> w) -> w-reifyIntegrals [] k = k (undefined :: Nil)-reifyIntegrals (i:ii) k = - reifyIntegral i (\(_ :: s) -> - reifyIntegrals ii (\(_ :: ss) -> - k (undefined :: Cons s ss)))+instance ReifiesNum s => ReifiesNum (Succ s) where+ reflectNum = (1+) <$> pop reflectNum -data Store s a +instance ReifiesNum s => ReifiesNum (Pred s) where+ reflectNum = subtract 1 <$> pop reflectNum -class ReflectedStorable s where- reflectStorable :: Storable a => s a -> a+reifyIntegral :: Integral a => a -> (forall s. ReifiesNum s => Tagged s w) -> w+reifyIntegral i k = case quotRem i 2 of+ (0, 0) -> zero k + (j, 0) -> reifyIntegral j (twice k)+ (j, 1) -> reifyIntegral j (twice (succ k))+ (j,-1) -> reifyIntegral j (twice (pred k))+ _ -> undefined + where+ twice :: Retag s (Twice s)+ twice = retag+ succ :: Retag s (Succ s)+ succ = retag+ pred :: Retag s (Pred s)+ pred = retag+ zero :: Tagged Zero a -> a+ zero = unTagged -instance ReflectedNums s => ReflectedStorable (Store s) where+newtype Nil = Nil Nil+newtype Cons s ss = Cons (Cons s ss)+instance Unused Nil where unused Nil{} = ()+instance Unused (Cons s ss) where unused Cons{} = ()++class ReifiesNums ss where+ reflectNums :: Num a => Tagged ss [a]++instance ReifiesNums Nil where+ reflectNums = pure []++instance (ReifiesNum s, ReifiesNums ss) => ReifiesNums (Cons s ss) where+ reflectNums = (:) <$> car reflectNum <*> cdr reflectNums where+ car :: Retag (Cons s ss) s+ car = retag+ cdr :: Retag (Cons s ss) ss+ cdr = retag++reifyIntegrals :: Integral a => [a] -> (forall ss. ReifiesNums ss => Tagged ss w) -> w+reifyIntegrals [] k = nil k where+ nil :: Tagged Nil a' -> a'+ nil = unTagged +reifyIntegrals (i:ii) k = reifyIntegral i (reifyIntegrals ii (cons k)) where+ cons :: Tagged (Cons s' ss') a' -> Tagged ss' (Tagged s' a')+ cons = pure . retag+ +newtype Store s a = Store (Store s a)+instance Unused (Store s a) where unused Store{} = ()++class ReifiesStorable s where+ reflectStorable :: Storable a => Tagged (s a) a++instance ReifiesNums s => ReifiesStorable (Store s) where+ reflectStorable = r where + r = unsafePerformIO $ alloca $ \p -> do + pokeArray (castPtr p) (bytes reflectNums r)+ pure <$> peek p + bytes :: Tagged s' [CChar] -> Tagged (Store s' b) b -> [CChar]+ bytes (Tagged a) _ = a {-# NOINLINE reflectStorable #-}- reflectStorable _ = unsafePerformIO . alloca $ \p -> do - pokeArray (castPtr p) bytes- peek p - where - bytes = reflectNums (undefined :: s) :: [CChar] -reifyStorable :: Storable a => a -> (forall s. ReflectedStorable s => s a -> w) -> w-reifyStorable a k = reifyIntegrals (bytes :: [CChar]) (\(_ :: s) -> k (undefined :: Store s a))+store :: Retag s' (Store s' c)+store = retag++reifyStorable :: Storable a => a -> (forall s. ReifiesStorable s => Tagged (s a) w) -> w+reifyStorable a k = reifyIntegrals bytes (store k) where+ bytes :: [CChar] bytes = unsafePerformIO $ with a (peekArray (sizeOf a) . castPtr) {-# NOINLINE reifyStorable #-} -class Reflects s a | s -> a where - reflect :: s -> a+class Reifies s a | s -> a where + reflect :: Tagged s a -data Stable (s :: * -> *) a+newtype Stable s a = Stable (s (Stable s a))+instance Unused (Stable s a) where unused Stable{} = () -{--instance ReflectedStorable s => Reflects (Stable s a) a where- reflect = unsafePerformIO . fmap const . deRefStablePtr $ reflectStorable (undefined :: s p) +instance ReifiesStorable s => Reifies (Stable s a) a where+ reflect = r where+ r = unsafePerformIO $ do+ pure <$> deRefStablePtr p <* freeStablePtr p -reify :: a -> (forall s. Reflects s a => s -> w) -> w-reify (a :: a) k = unsafePerformIO $ do- p <- newStablePtr a- reifyStorable p (\(_ :: s (StablePtr a)) -> return (k (undefined :: Stable s a)))--}+ p = pointer reflectStorable r -instance ReflectedStorable s => Reflects (Stable s a) a where- reflect = unsafePerformIO $ do- a <- deRefStablePtr p- freeStablePtr p- return (const a)- where - p = reflectStorable (undefined :: s p)+ pointer :: Tagged (s' p) p -> Tagged (Stable s' a') a' -> p+ pointer (Tagged a) _ = a {-# NOINLINE reflect #-} -reify :: a -> (forall s. (s `Reflects` a) => s -> w) -> w-reify (a :: a) k = unsafePerformIO $ do+reify :: a -> (forall s. Reifies s a => Tagged s w) -> w+reify a k = unsafePerformIO $ do p <- newStablePtr a- reifyStorable p (\(_ :: s (StablePtr a)) -> - let k' s = (reflect :: Stable s a -> a) `seq` return (k s) - in k' (undefined :: Stable s a))+ reifyStorable p (stable (reflect `before` (return <$> k)))+ where+ stable :: Retag (s' (StablePtr a')) (Stable s' a')+ stable = retag+ before :: Tagged (s' a') a' -> Tagged (s' a') r -> Tagged (s' a') r+ before = seq {-# NOINLINE reify #-}+
reflection.cabal view
@@ -1,21 +1,22 @@ name: reflection-version: 0.1.1+version: 0.2.0 license: BSD3 license-file: LICENSE-author: Oleg Kiselyov and Chung-chieh Shan+author: Edward A. Kmett, Oleg Kiselyov and Chung-chieh Shan maintainer: Edward A. Kmett <ekmett@gmail.com> stability: experimental homepage: http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf-category: Data+category: Data, Reflection, Dependent Types synopsis: Functional Pearl: Implicit Configurations copyright: 2009 Edward A. Kmett, 2004 Oleg Kiselyov and Chung-chieh Shan-description: Implementation of the code in "Functional Pearl: Implicit Configurations" by Oleg Kiselyov and Chung-chieh Shan+description: Implementation of the ideas presented in the paper "Functional Pearl: Implicit Configurations" by Oleg Kiselyov and Chung-chieh Shan.+ Modified to avoid the use of scoped type variables, and to use a phantom type wrapper rather than dummy arguments. build-type: Simple cabal-version: >=1.2 library build-depends: - base >= 4 && < 4.2+ base >= 4 && < 5 exposed-modules: Data.Reflection