reflection 0.7 → 0.8

raw patch · 4 files changed

+103/−56 lines, 4 files

Files

Data/Reflection.hs +19/−23
examples/Constraints.hs +51/−0
examples/Monoid.hs +16/−22
reflection.cabal +17/−11

Data/Reflection.hs view

@@ -1,4 +1,4 @@-{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Rank2Types, TypeFamilies #-} {-# OPTIONS_GHC -fno-cse -fno-full-laziness -fno-float-in -fno-warn-unused-binds #-} ---------------------------------------------------------------------------- -- |@@ -8,7 +8,7 @@ -- -- Maintainer  : Edward Kmett <ekmett@gmail.com> -- Stability   : experimental--- Portability : non-portable (rank-2 types)+-- Portability : non-portable (rank-2 types, type families) -- -- Based on the Functional Pearl: Implicit Configurations paper by -- Oleg Kiselyov and Chung-chieh Shan.@@ -24,7 +24,6 @@     -- * Reifying any term at the type level       Reified(..)     , reify-    , reflectT     -- * Reifying integral values at the type level     , ReifiedNum(..)     , reifyIntegral@@ -43,15 +42,11 @@ newtype PredTwice s = PredTwice (PredTwice s) deriving (Show)  class ReifiedNum s where-  reflectNum :: Num a => proxy s -> a+  reflectNum :: Num a => p s -> a  instance ReifiedNum Zero where   reflectNum = pure 0 -pop :: proxy (f s) -> Proxy s-pop _ = Proxy-{-# INLINE pop #-}- instance ReifiedNum s => ReifiedNum (Twice s) where   reflectNum p = 2 * reflectNum (pop p) @@ -69,13 +64,17 @@     (j,-1) -> reifyIntegral j (k . predTwice)     _      -> undefined -twice :: proxy s -> Proxy (Twice s)+pop :: p (f s) -> Proxy s+pop _ = Proxy+{-# INLINE pop #-}++twice :: p s -> Proxy (Twice s) twice _ = Proxy -succTwice :: proxy s -> Proxy (SuccTwice s)+succTwice :: p s -> Proxy (SuccTwice s) succTwice _ = Proxy -predTwice :: proxy s -> Proxy (PredTwice s)+predTwice :: p s -> Proxy (PredTwice s) predTwice _ = Proxy  zero :: (Proxy Zero -> a) -> a@@ -90,32 +89,29 @@ intPtrToStablePtr = castPtrToStablePtr . intPtrToPtr  class Reified s where-  reflect :: p (s a) -> a+  type Reflected s+  reflect :: p s -> Reflected s +stable :: p s -> Proxy (Stable s a)+stable _ = Proxy+ unstable :: (p (Stable s a) -> a) -> Proxy s unstable _ = Proxy -instance ReifiedNum s => Reified (Stable s) where+instance ReifiedNum s => Reified (Stable s a) where+  type Reflected (Stable s a) = a   reflect = r where       r = unsafePerformIO $ pure <$> deRefStablePtr p <* freeStablePtr p       p = intPtrToStablePtr $ reflectNum $ unstable r   {-# NOINLINE reflect #-} -reflectT :: Reified s => t s a -> a-reflectT p = reflect (t p) where-  t :: p x y -> Proxy (x y)-  t _ = Proxy- -- This had to be moved to the top level, due to an apparent bug in the ghc inliner introduced in ghc 7.0.x-reflectBefore :: Reified s => (Proxy (s a) -> b) -> proxy (s a) -> b+reflectBefore :: Reified s => (Proxy s -> b) -> proxy s -> b reflectBefore f = let b = f Proxy in b `seq` const b {-# NOINLINE reflectBefore #-} -reify :: a -> (forall s. Reified s => Proxy (s a) -> w) -> w+reify :: a -> (forall s. (Reified s, Reflected s ~ a) => Proxy s -> w) -> w reify a k = unsafePerformIO $ do     p <- newStablePtr a     reifyIntegral (stablePtrToIntPtr p) (reflectBefore (fmap return k) . stable)-  where-    stable :: p s -> Proxy (Stable s a)-    stable _ = Proxy {-# NOINLINE reify #-}

+ examples/Constraints.hs view

@@ -0,0 +1,51 @@+{-# LANGUAGE Rank2Types, TypeFamilies, TypeOperators, ConstraintKinds, PolyKinds, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables #-}+import Control.Newtype        -- from newtype+import Data.Constraint        -- from constraints+import Data.Constraint.Unsafe -- from constraints+import Data.Monoid            -- from base+import Data.Proxy             -- from tagged+import Data.Reflection        -- from reflection++-- | Values in our dynamically constructed monoid over 'a'+newtype Lift (p :: * -> Constraint) (a :: *) (s :: *) = Lift { lower :: a }++class ReifiableConstraint p where+  data Def (p :: * -> Constraint) (a :: *)+  reifiedIns :: (Reified s, Reflected s ~ Def p a) :- p (Lift p a s)++instance Newtype (Lift p a s) a where+  pack = Lift+  unpack = lower++-- > ghci> with (Monoid (+) 0) $ mempty <> Lift 2+-- > 0+with :: Def p a -> (forall s. (Reified s, Reflected s ~ Def p a) => Lift p a s) -> a+with d v = reify d $ lower . asProxyOf v++reifyInstance :: Def p a -> (forall s. (Reified s, Reflected s ~ Def p a) => Proxy s -> r) -> r+reifyInstance = reify++asProxyOf :: f s -> Proxy s -> f s+asProxyOf a _ = a++-- > using (Monoid (+) 0) $ mappend mempty 12+using :: forall p a. ReifiableConstraint p => Def p a -> (p a => a) -> a+using d m = reify d $ \(_ :: Proxy s) -> m \\ trans (unsafeCoerceConstraint :: (p (Lift p a s) :- p a)) reifiedIns++usingT :: forall p f a. ReifiableConstraint p => Def p a -> (p a => f a) -> f a+usingT d m = reify d $ \(_ :: Proxy s) -> m \\ trans (unsafeCoerceConstraint :: (p (Lift p a s) :- p a)) reifiedIns++instance ReifiableConstraint Monoid where+  data Def Monoid a = Monoid { mappend_ :: a -> a -> a, mempty_ :: a }+  reifiedIns = Sub Dict++instance (Reified s, Reflected s ~ Def Monoid a) => Monoid (Lift Monoid a s) where+  mappend a b        = Lift $ mappend_ (reflect a) (lower a) (lower b)+  mempty = a where a = Lift $ mempty_ (reflect a)++instance ReifiableConstraint Eq where+  data Def Eq a = Eq { eq :: a -> a -> Bool }+  reifiedIns = Sub Dict++instance (Reified s, Reflected s ~ Def Eq a) => Eq (Lift Eq a s) where+  a == b = eq (reflect a) (lower a) (lower b)

examples/Monoid.hs view

@@ -1,28 +1,22 @@-{-# LANGUAGE Rank2Types, KindSignatures #-}-import Data.Reflection-import Data.Monoid-import Data.Proxy+{-# LANGUAGE Rank2Types, TypeFamilies #-}+import Data.Reflection -- from reflection+import Data.Monoid     -- from base+import Data.Proxy      -- from tagged -newtype M (s :: * -> *) a = M { runM :: a }+-- | Values in our dynamically constructed monoid over 'a'+newtype M a s = M { runM :: a } deriving (Eq,Ord) +-- | A dictionary describing the contents of a monoid data Monoid_ a = Monoid_ { mappend_ :: a -> a -> a, mempty_ :: a } -instance Reified s => Monoid (M s a) where-  mappend a b = M $ mappend_ (reflectM a) (runM a) (runM b)-  mempty = r where r = M $ mempty_ $ reflectM r--monoidProxy :: M s a -> Proxy (s (Monoid_ a))-monoidProxy _ = Proxy--reflectM :: Reified s => M s a -> Monoid_ a-reflectM m = reflect (monoidProxy m)--reifyMonoid :: (a -> a -> a) -> a -> (forall s. Reified s => Proxy (s (Monoid_ a)) -> r) -> r-reifyMonoid f z = reify (Monoid_ f z)+instance (Reified s, Reflected s ~ Monoid_ a) => Monoid (M a s) where+  mappend a b        = M $ mappend_ (reflect a) (runM a) (runM b)+  mempty = a where a = M $ mempty_ (reflect a) --- > ghci> withMonoid (+) 0 (mempty `mappend` M 2)+-- > ghci> withMonoid (+) 0 $ mempty <> M 2 -- > 2-withMonoid :: (a -> a -> a) -> a -> (forall s. Reified s => M s a) -> a-withMonoid f z v = reifyMonoid f z (\p -> runM (v `asProxyOf` p)) where-  asProxyOf :: M s x -> Proxy (s (Monoid_ x)) -> M s x-  asProxyOf a _ = a+withMonoid :: (a -> a -> a) -> a -> (forall s. (Reified s, Reflected s ~ Monoid_ a) => M a s) -> a+withMonoid f z v = reify (Monoid_ f z) (runM . asProxyOf v)++asProxyOf :: f s -> Proxy s -> f s+asProxyOf a _ = a

reflection.cabal view

@@ -1,5 +1,5 @@ name:           reflection-version:        0.7+version:        0.8 license:        BSD3 license-file:   LICENSE author:         Edward A. Kmett, Oleg Kiselyov and Chung-chieh Shan@@ -14,25 +14,31 @@ description:   This package provides an implementation of the ideas presented in the paper   "Functional Pearl: Implicit Configurations" by Oleg Kiselyov and-  Chung-chieh Shan. However, the API has been modified to use only-  one extension: @Rank2Types@+  Chung-chieh Shan. However, the API has been modified to use @Rank2Types@ and+  @TypeFamilies@   .   Usage reduces to using two combinators.   .-  > reify :: a -> (forall s. Reified s => Proxy (s a) -> w) -> w-  > reflect :: Reified s => p (s a) -> a+  > reify :: a -> (forall s. (Reified s, Reflected s ~ a) => Proxy s -> w) -> w+  > reflect :: Reified s => p s -> Reflected s   .-  > ghci> reify 6 (\p -> reflect p + reflect p)+  > ghci> reify 6 (\p -> reflect p + reflect p) :: Int   > 12   .   The argument passed along by reify is just a @data Proxy t = Proxy@, so all of the   information needed to reconstruct your value has been moved to the type level.   This enables it to be used when constructing instances (See @examples/Monoid.hs@).-  An additional combinator that may be more useful when building instances is also-  supplied.   .-  > reflectT :: Reified s => p s a -> a+  /Changes in 0.8/:   .+  * Switched to using type families to avoid a problem where the user could cast+    @Proxy (s a) -> Proxy (s b)@ and get back a values with the wrong type under+    the API in effect from 0.6. This API yields a much nicer example as well.+  .+  * Removed @reflectT@ as it no longer makes sense.+  .+  * Added a more advanced example @example/Constraints.hs@ using constraint kinds.+  .   /Changes in 0.7/:   .   * Uses a much simpler construction where @reify@ now converts a @StablePtr@ to an@@ -66,14 +72,14 @@     reduces the need for helper functions and scoped type variables in user     code. -extra-source-files: examples/Monoid.hs+extra-source-files: examples/Monoid.hs examples/Constraints.hs  source-repository head   type: git   location: git://github.com/ekmett/reflection.git  library-  other-extensions: Rank2Types+  other-extensions: Rank2Types, TypeFamilies   build-depends:     base >= 4 && < 5,     tagged >= 0.2.3 && < 0.3