rank1dynamic (empty) → 0.1.0.0
raw patch · 5 files changed
+542/−0 lines, 5 filesdep +basedep +binarydep +ghc-primsetup-changed
Dependencies added: base, binary, ghc-prim
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- rank1dynamic.cabal +28/−0
- src/Data/Rank1Dynamic.hs +120/−0
- src/Data/Rank1Typeable.hs +362/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2012, Edsko de Vries++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Edsko de Vries nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ rank1dynamic.cabal view
@@ -0,0 +1,28 @@+Name: rank1dynamic+Version: 0.1.0.0+Synopsis: Like Data.Dynamic/Data.Typeable but with support for rank-1 polymorphic types+Description: "Data.Typeable" and "Data.Dynamic" only support monomorphic types. + In this package we provide similar functionality but with+ support for rank-1 polymorphic types. +Homepage: http://github.com/haskell-distributed/distributed-process+License: BSD3+License-File: LICENSE+Author: Edsko de Vries+Maintainer: edsko@well-typed.com+Copyright: Well-Typed LLP+Category: Data+Build-Type: Simple+Cabal-Version: >=1.8++Library+ Exposed-Modules: Data.Rank1Dynamic,+ Data.Rank1Typeable+ Build-Depends: base ==4.5.*,+ ghc-prim >= 0.2 && < 0.3,+ binary >= 0.5 && < 0.6 + HS-Source-Dirs: src+ GHC-Options: -Wall+ Extensions: EmptyDataDecls,+ DeriveDataTypeable,+ ViewPatterns,+ CPP
+ src/Data/Rank1Dynamic.hs view
@@ -0,0 +1,120 @@+-- | Dynamic values with support for rank-1 polymorphic types.+--+-- [Examples of fromDynamic]+--+-- These examples correspond to the 'Data.Rank1Typeable.isInstanceOf' examples+-- in "Data.Rank1Typeable".+--+-- > > do f <- fromDynamic (toDynamic (even :: Int -> Bool)) ; return $ (f :: Int -> Int) 0 +-- > Left "Cannot unify Int and Bool"+-- > +-- > > do f <- fromDynamic (toDynamic (const 1 :: ANY -> Int)) ; return $ (f :: Int -> Int) 0+-- > Right 1+-- > +-- > > do f <- fromDynamic (toDynamic (unsafeCoerce :: ANY1 -> ANY2)) ; return $ (f :: Int -> Int) 0+-- > Right 0+-- > +-- > > do f <- fromDynamic (toDynamic (id :: ANY -> ANY)) ; return $ (f :: Int -> Bool) 0+-- > Left "Cannot unify Bool and Int"+-- > +-- > > do f <- fromDynamic (toDynamic (undefined :: ANY)) ; return $ (f :: Int -> Int) 0+-- > Right *** Exception: Prelude.undefined+-- > +-- > > do f <- fromDynamic (toDynamic (id :: ANY -> ANY)) ; return $ (f :: Int)+-- > Left "Cannot unify Int and ->"+--+-- [Examples of dynApply]+-- +-- These examples correspond to the 'Data.Rank1Typeable.funResultTy' examples+-- in "Data.Rank1Typeable".+--+-- > > do app <- toDynamic (id :: ANY -> ANY) `dynApply` toDynamic True ; f <- fromDynamic app ; return $ (f :: Bool)+-- > Right True+-- > +-- > > do app <- toDynamic (const :: ANY -> ANY1 -> ANY) `dynApply` toDynamic True ; f <- fromDynamic app ; return $ (f :: Int -> Bool) 0+-- > Right True+-- > +-- > > do app <- toDynamic (($ True) :: (Bool -> ANY) -> ANY) `dynApply` toDynamic (id :: ANY -> ANY) ; f <- fromDynamic app ; return (f :: Bool)+-- > Right True+-- > +-- > > app <- toDynamic (const :: ANY -> ANY1 -> ANY) `dynApply` toDynamic (id :: ANY -> ANY) ; f <- fromDynamic app ; return $ (f :: Int -> Bool -> Bool) 0 True+-- > Right True+-- > +-- > > do app <- toDynamic ((\f -> f . f) :: (ANY -> ANY) -> ANY -> ANY) `dynApply` toDynamic (even :: Int -> Bool) ; f <- fromDynamic app ; return (f :: ()) +-- > Left "Cannot unify Int and Bool"+--+-- [Using toDynamic]+--+-- When using polymorphic values you need to give an explicit type annotation:+--+-- > > toDynamic id+-- > +-- > <interactive>:46:1:+-- > Ambiguous type variable `a0' in the constraint:+-- > (Typeable a0) arising from a use of `toDynamic'+-- > Probable fix: add a type signature that fixes these type variable(s)+-- > In the expression: toDynamic id+-- > In an equation for `it': it = toDynamic id+-- +-- versus+--+-- > > toDynamic (id :: ANY -> ANY)+-- > <<ANY -> ANY>>+-- +-- Note that these type annotation are checked by ghc like any other:+--+-- > > toDynamic (id :: ANY -> ANY1)+-- > +-- > <interactive>:45:12:+-- > Couldn't match expected type `V1' with actual type `V0'+-- > Expected type: ANY -> ANY1+-- > Actual type: ANY -> ANY+-- > In the first argument of `toDynamic', namely `(id :: ANY -> ANY1)'+-- > In the expression: toDynamic (id :: ANY -> ANY1)+module Data.Rank1Dynamic + ( Dynamic+ , toDynamic+ , fromDynamic+ , TypeError+ , dynTypeRep+ , dynApply+ ) where++import qualified GHC.Prim as GHC (Any)+import Data.Rank1Typeable + ( Typeable+ , TypeRep+ , typeOf+ , isInstanceOf+ , TypeError+ , funResultTy+ )+import Unsafe.Coerce (unsafeCoerce)++-- | Encapsulate an object and its type+data Dynamic = Dynamic TypeRep GHC.Any++instance Show Dynamic where+ showsPrec _ (Dynamic t _) = showString "<<" . shows t . showString ">>" ++-- | Introduce a dynamic value +toDynamic :: Typeable a => a -> Dynamic+toDynamic x = Dynamic (typeOf x) (unsafeCoerce x)++-- | Eliminate a dynamic value+fromDynamic :: Typeable a => Dynamic -> Either TypeError a+fromDynamic (Dynamic t v) =+ case unsafeCoerce v of + r -> case typeOf r `isInstanceOf` t of+ Left err -> Left err+ Right () -> Right r++-- | Apply one dynamic value to another+dynApply :: Dynamic -> Dynamic -> Either TypeError Dynamic+dynApply (Dynamic t1 f) (Dynamic t2 x) = do+ t3 <- funResultTy t1 t2+ return $ Dynamic t3 (unsafeCoerce f x)++-- | The type representation of a dynamic value+dynTypeRep :: Dynamic -> TypeRep+dynTypeRep (Dynamic t _) = t
+ src/Data/Rank1Typeable.hs view
@@ -0,0 +1,362 @@+-- | Runtime type representation of terms with support for rank-1 polymorphic+-- types with type variables of kind *.+--+-- The essence of this module is that we use the standard 'Typeable' +-- representation of "Data.Typeable" but we introduce a special (empty) data+-- type 'TypVar' which represents type variables. 'TypVar' is indexed by an+-- arbitrary other data type, giving you an unbounded number of type variables;+-- for convenience, we define 'ANY', 'ANY1', .., 'ANY9'.+--+-- [Examples of isInstanceOf]+--+-- > -- We CANNOT use a term of type 'Int -> Bool' as 'Int -> Int'+-- > > typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: Int -> Bool)+-- > Left "Cannot unify Int and Bool"+-- > +-- > -- We CAN use a term of type 'forall a. a -> Int' as 'Int -> Int'+-- > > typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: ANY -> Int)+-- > Right ()+-- > +-- > -- We CAN use a term of type 'forall a b. a -> b' as 'forall a. a -> a'+-- > > typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY1)+-- > Right ()+-- > +-- > -- We CANNOT use a term of type 'forall a. a -> a' as 'forall a b. a -> b'+-- > > typeOf (undefined :: ANY -> ANY1) `isInstanceOf` typeOf (undefined :: ANY -> ANY)+-- > Left "Cannot unify Succ and Zero"+-- > +-- > -- We CAN use a term of type 'forall a. a' as 'forall a. a -> a'+-- > > typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY)+-- > Right ()+-- > +-- > -- We CANNOT use a term of type 'forall a. a -> a' as 'forall a. a'+-- > > typeOf (undefined :: ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY)+-- > Left "Cannot unify Skolem and ->"+--+-- (Admittedly, the quality of the type errors could be improved.)+--+-- [Examples of funResultTy]+--+-- > -- Apply fn of type (forall a. a -> a) to arg of type Bool gives Bool +-- > > funResultTy (typeOf (undefined :: ANY -> ANY)) (typeOf (undefined :: Bool))+-- > Right Bool+-- > +-- > -- Apply fn of type (forall a b. a -> b -> a) to arg of type Bool gives forall a. a -> Bool+-- > > funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: Bool))+-- > Right (ANY -> Bool) -- forall a. a -> Bool+-- > +-- > -- Apply fn of type (forall a. (Bool -> a) -> a) to argument of type (forall a. a -> a) gives Bool+-- > > funResultTy (typeOf (undefined :: (Bool -> ANY) -> ANY)) (typeOf (undefined :: ANY -> ANY))+-- > Right Bool+-- >+-- > -- Apply fn of type (forall a b. a -> b -> a) to arg of type (forall a. a -> a) gives (forall a b. a -> b -> b)+-- > > funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: ANY1 -> ANY1))+-- > Right (ANY -> ANY1 -> ANY1)+-- >+-- > -- Cannot apply function of type (forall a. (a -> a) -> a -> a) to arg of type (Int -> Bool)+-- > > funResultTy (typeOf (undefined :: (ANY -> ANY) -> (ANY -> ANY))) (typeOf (undefined :: Int -> Bool))+-- > Left "Cannot unify Int and Bool"+module Data.Rank1Typeable + ( -- * Basic types + TypeRep+ , typeOf+ , splitTyConApp+ , mkTyConApp+ , underlyingTypeRep+ -- * Operations on type representations + , isInstanceOf+ , funResultTy+ , TypeError+ -- * Type variables+ , TypVar+ , Zero+ , Succ+ , V0+ , V1+ , V2+ , V3+ , V4+ , V5+ , V6+ , V7+ , V8+ , V9+ , ANY+ , ANY1+ , ANY2+ , ANY3+ , ANY4+ , ANY5+ , ANY6+ , ANY7+ , ANY8+ , ANY9+ -- * Re-exports from Typeable+ , Typeable+ ) where++import Prelude hiding (succ)+import Control.Arrow ((***), second)+import Control.Monad (void)+import Control.Applicative ((<$>))+import Data.List (intersperse, isPrefixOf)+import Data.Maybe (fromMaybe)+import Data.Typeable (Typeable, tyConName, mkTyCon3)+import Data.Typeable.Internal (listTc, funTc, TyCon(TyCon))+import Data.Binary (Binary(get, put))+import GHC.Fingerprint.Type (Fingerprint(..))+import qualified Data.Typeable as Typeable + ( TypeRep+ , typeOf+ , splitTyConApp+ , mkTyConApp+ )++--------------------------------------------------------------------------------+-- The basic type --+--------------------------------------------------------------------------------++-- | Dynamic type representation with support for rank-1 types+newtype TypeRep = TypeRep { + -- | Return the underlying standard ("Data.Typeable") type representation+ underlyingTypeRep :: Typeable.TypeRep + }++-- | Compare two type representations+--+-- For base >= 4.6 this compares fingerprints, but older versions of base+-- have a bug in the fingerprint construction +-- (<http://hackage.haskell.org/trac/ghc/ticket/5962>)+instance Eq TypeRep where+#if ! MIN_VERSION_base(4,6,0)+ (splitTyConApp -> (c1, ts1)) == (splitTyConApp -> (c2, ts2)) =+ c1 == c2 && all (uncurry (==)) (zip ts1 ts2)+#else+ t1 == t2 = underlyingTypeRep t1 == underlyingTypeRep t2+#endif++-- Binary instance for 'TypeRep', avoiding orphan instances+instance Binary TypeRep where+ put (splitTyConApp -> (TyCon (Fingerprint hi lo) package modul name, ts)) = do+ put hi + put lo+ put package+ put modul+ put name+ put ts+ get = do+ hi <- get+ lo <- get+ package <- get+ modul <- get+ name <- get+ ts <- get+ return $ mkTyConApp (TyCon (Fingerprint hi lo) package modul name) ts++-- | The type representation of any 'Typeable' term+typeOf :: Typeable a => a -> TypeRep+typeOf = TypeRep . Typeable.typeOf++--------------------------------------------------------------------------------+-- Constructors/destructors (views) --+--------------------------------------------------------------------------------++-- | Split a type representation into the application of+-- a type constructor and its argument+splitTyConApp :: TypeRep -> (TyCon, [TypeRep])+splitTyConApp t = + let (c, ts) = Typeable.splitTyConApp (underlyingTypeRep t)+ in (c, map TypeRep ts)++-- | Inverse of 'splitTyConApp'+mkTyConApp :: TyCon -> [TypeRep] -> TypeRep+mkTyConApp c ts + = TypeRep (Typeable.mkTyConApp c (map underlyingTypeRep ts))++isTypVar :: TypeRep -> Maybe Var +isTypVar (splitTyConApp -> (c, [t])) | c == typVar = Just t+isTypVar _ = Nothing++mkTypVar :: Var -> TypeRep+mkTypVar x = mkTyConApp typVar [x]++typVar :: TyCon+typVar = let (c, _) = splitTyConApp (typeOf (undefined :: TypVar V0)) in c++skolem :: TyCon+skolem = let (c, _) = splitTyConApp (typeOf (undefined :: Skolem V0)) in c++--------------------------------------------------------------------------------+-- Type variables --+--------------------------------------------------------------------------------++data TypVar a deriving Typeable +data Skolem a deriving Typeable+data Zero deriving Typeable+data Succ a deriving Typeable++type V0 = Zero+type V1 = Succ V0+type V2 = Succ V1+type V3 = Succ V2+type V4 = Succ V3+type V5 = Succ V4+type V6 = Succ V5+type V7 = Succ V6+type V8 = Succ V7+type V9 = Succ V8++type ANY = TypVar V0 +type ANY1 = TypVar V1+type ANY2 = TypVar V2+type ANY3 = TypVar V3+type ANY4 = TypVar V4+type ANY5 = TypVar V5+type ANY6 = TypVar V6+type ANY7 = TypVar V7+type ANY8 = TypVar V8+type ANY9 = TypVar V9++--------------------------------------------------------------------------------+-- Operations on type reps --+--------------------------------------------------------------------------------++-- | If 'isInstanceOf' fails it returns a type error+type TypeError = String++-- | @t1 `isInstanceOf` t2@ checks if @t1@ is an instance of @t2@ +isInstanceOf :: TypeRep -> TypeRep -> Either TypeError () +isInstanceOf t1 t2 = void (unify (skolemize t1) t2)++-- | @funResultTy t1 t2@ is the type of the result when applying a function+-- of type @t1@ to an argument of type @t2@+funResultTy :: TypeRep -> TypeRep -> Either TypeError TypeRep +funResultTy (splitTyConApp -> (fc, [farg, fres])) x | fc == funTc = do + s <- unify (alphaRename "f" farg) (alphaRename "x" x)+ return (normalize (subst s (alphaRename "f" fres)))+funResultTy f _ = + Left $ show f ++ " is not a function"++--------------------------------------------------------------------------------+-- Alpha-renaming and normalization --+--------------------------------------------------------------------------------++alphaRename :: String -> TypeRep -> TypeRep+alphaRename prefix (isTypVar -> Just x) =+ mkTypVar (mkTyConApp (mkTyCon prefix) [x])+alphaRename prefix (splitTyConApp -> (c, ts)) =+ mkTyConApp c (map (alphaRename prefix) ts)++tvars :: TypeRep -> [Var]+tvars (isTypVar -> Just x) = [x]+tvars (splitTyConApp -> (_, ts)) = concatMap tvars ts++normalize :: TypeRep -> TypeRep +normalize t = subst (zip (tvars t) anys) t+ where+ anys :: [TypeRep]+ anys = map mkTypVar (iterate succ zero)++ succ :: TypeRep -> TypeRep+ succ = mkTyConApp succTyCon . (:[])++ zero :: TypeRep+ zero = mkTyConApp zeroTyCon [] ++mkTyCon :: String -> TyCon+mkTyCon = mkTyCon3 "rank1typeable" "Data.Rank1Typeable"++succTyCon :: TyCon+succTyCon = let (c, _) = splitTyConApp (typeOf (undefined :: Succ Zero)) in c++zeroTyCon :: TyCon+zeroTyCon = let (c, _) = splitTyConApp (typeOf (undefined :: Zero)) in c++--------------------------------------------------------------------------------+-- Unification --+--------------------------------------------------------------------------------++type Substitution = [(Var, TypeRep)]+type Equation = (TypeRep, TypeRep)+type Var = TypeRep++skolemize :: TypeRep -> TypeRep+skolemize (isTypVar -> Just x) = mkTyConApp skolem [x] +skolemize (splitTyConApp -> (c, ts)) = mkTyConApp c (map skolemize ts)++occurs :: Var -> TypeRep -> Bool+occurs x (isTypVar -> Just x') = x == x' +occurs x (splitTyConApp -> (_, ts)) = any (occurs x) ts++subst :: Substitution -> TypeRep -> TypeRep+subst s (isTypVar -> Just x) = fromMaybe (mkTypVar x) (lookup x s)+subst s (splitTyConApp -> (c, ts)) = mkTyConApp c (map (subst s) ts)++unify :: TypeRep + -> TypeRep + -> Either TypeError Substitution +unify = \t1 t2 -> go [] [(t1, t2)]+ where+ go :: Substitution + -> [Equation] + -> Either TypeError Substitution + go acc [] = + return acc+ go acc ((t1, t2) : eqs) | t1 == t2 = -- Note: equality check is fast+ go acc eqs+ go acc ((isTypVar -> Just x, t) : eqs) =+ if x `occurs` t + then Left "Occurs check"+ else go ((x, t) : map (second $ subst [(x, t)]) acc) + (map (subst [(x, t)] *** subst [(x, t)]) eqs)+ go acc ((t, isTypVar -> Just x) : eqs) =+ go acc ((mkTypVar x, t) : eqs)+ go acc ((splitTyConApp -> (c1, ts1), splitTyConApp -> (c2, ts2)) : eqs) = + if c1 /= c2 + then Left $ "Cannot unify " ++ show c1 ++ " and " ++ show c2+ else go acc (zip ts1 ts2 ++ eqs)++--------------------------------------------------------------------------------+-- Pretty-printing --+--------------------------------------------------------------------------------++instance Show TypeRep where+ showsPrec p (splitTyConApp -> (tycon, tys)) =+ case tys of+ [] -> showsPrec p tycon+ [anyIdx -> Just i] | tycon == typVar -> showString "ANY" . showIdx i + [x] | tycon == listTc -> + showChar '[' . shows x . showChar ']'+ [a,r] | tycon == funTc -> + showParen (p > 8) $ showsPrec 9 a + . showString " -> " + . showsPrec 8 r+ xs | isTupleTyCon tycon -> + showTuple xs+ _ ->+ showParen (p > 9) $ showsPrec p tycon+ . showChar ' '+ . showArgs tys+ where+ showIdx 0 = showString ""+ showIdx i = shows i++showArgs :: Show a => [a] -> ShowS+showArgs [] = id+showArgs [a] = showsPrec 10 a+showArgs (a:as) = showsPrec 10 a . showString " " . showArgs as ++anyIdx :: TypeRep -> Maybe Int +anyIdx (splitTyConApp -> (c, [])) | c == zeroTyCon = Just 0+anyIdx (splitTyConApp -> (c, [t])) | c == succTyCon = (+1) <$> anyIdx t+anyIdx _ = Nothing++showTuple :: [TypeRep] -> ShowS+showTuple args = showChar '('+ . foldr (.) id ( intersperse (showChar ',') + $ map (showsPrec 10) args+ )+ . showChar ')'++isTupleTyCon :: TyCon -> Bool+isTupleTyCon = isPrefixOf "(," . tyConName