diff --git a/rank1dynamic.cabal b/rank1dynamic.cabal --- a/rank1dynamic.cabal +++ b/rank1dynamic.cabal @@ -1,5 +1,5 @@ Name: rank1dynamic -Version: 0.2.0.0 +Version: 0.2.0.1 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 @@ -28,7 +28,27 @@ binary >= 0.5 && < 0.8 HS-Source-Dirs: src GHC-Options: -Wall - Extensions: EmptyDataDecls, + Extensions: ConstraintKinds, + EmptyDataDecls, + ExistentialQuantification, DeriveDataTypeable, + KindSignatures, + PolyKinds, + RankNTypes, + StandaloneDeriving, ViewPatterns, CPP + +Test-Suite TestRank1Dynamic + Type: exitcode-stdio-1.0 + Main-Is: test.hs + Build-Depends: base >= 4.4 && < 5, + HUnit >= 1.2 && < 1.3, + rank1dynamic, + test-framework >= 0.6 && < 0.9, + test-framework-hunit >= 0.2.0 && < 0.4 + if impl(ghc >= 7.8) + Build-Depends: constraints >= 0.4 && < 0.5 + ghc-options: -Wall -Werror + Extensions: CPP + HS-Source-Dirs: tests diff --git a/src/Data/Rank1Dynamic.hs b/src/Data/Rank1Dynamic.hs --- a/src/Data/Rank1Dynamic.hs +++ b/src/Data/Rank1Dynamic.hs @@ -22,6 +22,13 @@ -- > -- > > do f <- fromDynamic (toDynamic (id :: ANY -> ANY)) ; return $ (f :: Int) -- > Left "Cannot unify Int and ->" +-- > +-- > > do f <- fromDynamic (toDynamic (reifyConstraints return :: Dict (Monad Maybe) -> Int -> Maybe Int)) +-- > return $ (abstractConstraints (f :: Dict (Monad Maybe) -> Int -> Maybe Int)) 0 +-- > Right (Just 0) +-- +-- Please, see @tests/test.hs@ for examples of how to write the higher-kinded +-- case in ghc versions earlier than 7.6.3. -- -- [Examples of dynApply] -- diff --git a/src/Data/Rank1Typeable.hs b/src/Data/Rank1Typeable.hs --- a/src/Data/Rank1Typeable.hs +++ b/src/Data/Rank1Typeable.hs @@ -32,9 +32,32 @@ -- > -- 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 ->" +-- > +-- > -- We CAN use a term of type 'forall a. a -> m a' as 'Int -> Maybe Int' +-- > > typeOf (undefined :: Int -> Maybe Int) +-- > `isInstanceOf` typeOf (undefined :: ANY1 -> ANY ANY1) +-- > Left "Cannot unify Skolem and ->" +-- > +-- > -- We CAN use a term of type 'forall a. Monad a => a -> m a' as 'Int -> Maybe Int' +-- > -- 'Dict' comes from "Data.Constraint" in the package "constraints". +-- > > typeOf ((\Dict -> return) :: Dict (Monad Maybe) -> Int -> Maybe Int) +-- > `isInstanceOf` typeOf ((\Dict -> return) :: Dict (Monad ANY) -> ANY1 -> ANY ANY1) +-- > Right () -- -- (Admittedly, the quality of the type errors could be improved.) -- +-- When using @-XPolyKinds@, the type signatures with higher-kinded variables +-- need to be given as +-- +-- > (\Dict -> return) `asTypeOf` (undefined :: Dict (Monad ANY) -> ANY1 -> ANY ANY1) +-- +-- or +-- +-- > (\Dict -> return) :: Dict (Monad ANY) -> ANY1 -> ANY (ANY1 :: *) +-- +-- Please, see @tests/test.hs@ for examples of how to write the higher-kinded +-- cases in ghc versions earlier than 7.8.3. +-- -- [Examples of funResultTy] -- -- > -- Apply fn of type (forall a. a -> a) to arg of type Bool gives Bool @@ -56,6 +79,7 @@ -- > -- 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" +{-# OPTIONS_GHC -fno-warn-orphans #-} module Data.Rank1Typeable ( -- * Basic types TypeRep @@ -102,9 +126,21 @@ import Data.List (intersperse, isPrefixOf) import Data.Maybe (fromMaybe) import Data.Typeable (Typeable, mkTyCon3) +#if !MIN_VERSION_base(4,7,0) +import Data.Typeable + ( Typeable1(..) + , Typeable2(..) + , Typeable3(..) + , Typeable4(..) + , Typeable5(..) + , Typeable6(..) + , Typeable7(..) + ) +#endif import Data.Typeable.Internal (listTc, funTc, TyCon(TyCon), tyConName) import Data.Binary (Binary(get, put)) import GHC.Fingerprint.Type (Fingerprint(..)) +import GHC.Exts(Any) import qualified Data.Typeable as Typeable ( TypeRep , typeOf @@ -173,16 +209,23 @@ mkTyConApp c ts = TypeRep (Typeable.mkTyConApp c (map underlyingTypeRep ts)) -isTypVar :: TypeRep -> Maybe Var -isTypVar (splitTyConApp -> (c, [t])) | c == typVar = Just t -isTypVar _ = Nothing +isTypVarApp :: TypeRep -> Maybe (Var, [TypeRep]) +isTypVarApp (splitTyConApp -> (c, (t0:t:ts))) + | c == typVar && t0 == typTag = Just (t,ts) +isTypVarApp _ = Nothing -mkTypVar :: Var -> TypeRep -mkTypVar x = mkTyConApp typVar [x] +mkTypVarApp :: Var -> [TypeRep] -> TypeRep +mkTypVarApp x = mkTyConApp typVar . (typTag :) . (x :) +mkTyApp :: TypeRep -> [TypeRep] -> TypeRep +mkTyApp (splitTyConApp -> (c, ts)) = mkTyConApp c . (ts++) + typVar :: TyCon typVar = let (c, _) = splitTyConApp (typeOf (undefined :: TypVar V0)) in c +typTag :: TypeRep +typTag = typeOf (undefined :: T) + skolem :: TyCon skolem = let (c, _) = splitTyConApp (typeOf (undefined :: Skolem V0)) in c @@ -190,11 +233,42 @@ -- Type variables -- -------------------------------------------------------------------------------- -data TypVar a deriving Typeable -data Skolem a deriving Typeable -data Zero deriving Typeable -data Succ a deriving Typeable +-- | Internal tag to distinguish our uses of Any from user's. +data T deriving Typeable +type TypVar = Any T +data Skolem (a :: *) deriving Typeable +data Zero deriving Typeable +data Succ (a :: *) deriving Typeable + +#if MIN_VERSION_base(4,7,0) +deriving instance Typeable Any +#else +instance Typeable Any where + typeOf _ = Typeable.mkTyConApp (mkTyCon3 "ghc-prim" "GHC.Prim" "Any") [] + +instance Typeable1 Any where + typeOf1 _ = Typeable.mkTyConApp (mkTyCon3 "ghc-prim" "GHC.Prim" "Any") [] + +instance Typeable2 Any where + typeOf2 _ = Typeable.mkTyConApp (mkTyCon3 "ghc-prim" "GHC.Prim" "Any") [] + +instance Typeable3 Any where + typeOf3 _ = Typeable.mkTyConApp (mkTyCon3 "ghc-prim" "GHC.Prim" "Any") [] + +instance Typeable4 Any where + typeOf4 _ = Typeable.mkTyConApp (mkTyCon3 "ghc-prim" "GHC.Prim" "Any") [] + +instance Typeable5 Any where + typeOf5 _ = Typeable.mkTyConApp (mkTyCon3 "ghc-prim" "GHC.Prim" "Any") [] + +instance Typeable6 Any where + typeOf6 _ = Typeable.mkTyConApp (mkTyCon3 "ghc-prim" "GHC.Prim" "Any") [] + +instance Typeable7 Any where + typeOf7 _ = Typeable.mkTyConApp (mkTyCon3 "ghc-prim" "GHC.Prim" "Any") [] +#endif + type V0 = Zero type V1 = Succ V0 type V2 = Succ V1 @@ -232,7 +306,7 @@ -- of type @t1@ to an argument of type @t2@ funResultTy :: TypeRep -> TypeRep -> Either TypeError TypeRep funResultTy t1 t2 = do - let anyTy = mkTypVar $ typeOf (undefined :: V0) + let anyTy = mkTypVarApp (typeOf (undefined :: V0)) [] s <- unify (alphaRename "f" t1) $ mkTyConApp funTc [alphaRename "x" t2, anyTy] return $ normalize $ subst s anyTy @@ -241,20 +315,20 @@ -------------------------------------------------------------------------------- alphaRename :: String -> TypeRep -> TypeRep -alphaRename prefix (isTypVar -> Just x) = - mkTypVar (mkTyConApp (mkTyCon prefix) [x]) +alphaRename prefix (isTypVarApp -> Just (x,ts)) = + mkTypVarApp (mkTyConApp (mkTyCon prefix) [x]) (map (alphaRename prefix) ts) alphaRename prefix (splitTyConApp -> (c, ts)) = mkTyConApp c (map (alphaRename prefix) ts) tvars :: TypeRep -> [Var] -tvars (isTypVar -> Just x) = [x] +tvars (isTypVarApp -> Just (x, ts)) = x : concatMap tvars ts 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) + anys = map (flip mkTypVarApp []) (iterate succ zero) succ :: TypeRep -> TypeRep succ = mkTyConApp succTyCon . (:[]) @@ -280,15 +354,16 @@ type Var = TypeRep skolemize :: TypeRep -> TypeRep -skolemize (isTypVar -> Just x) = mkTyConApp skolem [x] -skolemize (splitTyConApp -> (c, ts)) = mkTyConApp c (map skolemize ts) +skolemize (isTypVarApp -> Just (x, ts)) = mkTyConApp skolem $ x : map skolemize ts +skolemize (splitTyConApp -> (c, ts)) = mkTyConApp c (map skolemize ts) occurs :: Var -> TypeRep -> Bool -occurs x (isTypVar -> Just x') = x == x' +occurs x (isTypVarApp -> Just (x', ts)) = x == x' || any (occurs x) ts 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 (isTypVarApp -> Just (x, ts)) = + flip mkTyApp (map (subst s) ts) $ fromMaybe (mkTypVarApp x []) (lookup x s) subst s (splitTyConApp -> (c, ts)) = mkTyConApp c (map (subst s) ts) unify :: TypeRep @@ -303,13 +378,23 @@ return acc go acc ((t1, t2) : eqs) | t1 == t2 = -- Note: equality check is fast go acc eqs - go acc ((isTypVar -> Just x, t) : eqs) = + go acc ((isTypVarApp -> 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) + -- The left-hand side of the equation is a type variable application. + -- Decompose the right-hand side of the equation. + go acc ((t1@(isTypVarApp -> Just (x, ts)), t2) : eqs) = + let (t,ts') = case isTypVarApp t2 of + Just (x', ts'') -> (mkTypVarApp x' [], ts'') + Nothing -> let (c,ts'') = splitTyConApp t2 + in (mkTyConApp c [], ts'') + in if length ts == length ts' + then go acc ((mkTypVarApp x [], t) : zip ts ts' ++ eqs) + else Left $ "Cannot unify " ++ show t1 ++ " and " ++ show t2 + go acc ((t, isTypVarApp -> Just (x, ts)) : eqs) = + go acc ((mkTypVarApp x ts, t) : eqs) go acc ((splitTyConApp -> (c1, ts1), splitTyConApp -> (c2, ts2)) : eqs) = if c1 /= c2 then Left $ "Cannot unify " ++ show c1 ++ " and " ++ show c2 @@ -323,7 +408,11 @@ showsPrec p (splitTyConApp -> (tycon, tys)) = case tys of [] -> showsPrec p tycon - [anyIdx -> Just i] | tycon == typVar -> showString "ANY" . showIdx i + (t0 : (anyIdx -> Just i) : ts) | tycon == typVar && t0 == typTag -> + if null ts + then showString "ANY" . showIdx i + else showParen (p > 9) $ showString "ANY" . showIdx i . + showChar ' ' . showArgs ts [x] | tycon == listTc -> showChar '[' . shows x . showChar ']' [a,r] | tycon == funTc -> diff --git a/tests/test.hs b/tests/test.hs new file mode 100644 --- /dev/null +++ b/tests/test.hs @@ -0,0 +1,197 @@ +#if !MIN_VERSION_base(4,7,0) +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ExistentialQuantification #-} +#if !MIN_VERSION_base(4,6,0) +{-# LANGUAGE KindSignatures #-} +#endif +#endif +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +import Data.Rank1Typeable +import Data.Rank1Dynamic + +#if MIN_VERSION_base(4,7,0) +import Data.Constraint (Dict(..)) +#else +import qualified Data.Typeable as Typeable (Typeable(..),Typeable1(..), mkTyCon3, mkTyConApp) +#endif +import Test.HUnit hiding (Test) +import Test.Framework +import Test.Framework.Providers.HUnit +import Unsafe.Coerce + + +main :: IO () +main = defaultMain tests + +#if MIN_VERSION_base(4,7,0) +deriving instance Typeable Monad +#else +data MonadDict m = Monad m => MonadDict + +instance Typeable.Typeable1 m => Typeable (MonadDict m) where + typeOf _ = Typeable.mkTyConApp (Typeable.mkTyCon3 "main" "Main" "MonadDict") + [ Typeable.typeOf1 (undefined :: m a) ] + +returnD :: MonadDict m -> a -> m a +returnD MonadDict = return +#endif + +tests :: [Test] +tests = + [ testGroup "Examples of isInstanceOf" + [ testCase "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" + + , testCase "CAN use a term of type 'forall a. a -> Int' as 'Int -> Int'" $ + typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: ANY -> Int) + @?= Right () + + , testCase "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 () + + , testCase "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" + + , testCase "CAN use a term of type 'forall a. a' as 'forall a. a -> a'" $ + typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY) + @?= Right () + + , testCase "CANNOT use a term of type 'forall a. a -> a' as 'forall a. a'" $ + typeOf (undefined :: ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY) +#if MIN_VERSION_base(4,7,0) + @?= Left "Cannot unify Skolem and (->)" +#else + @?= Left "Cannot unify Skolem and ->" +#endif + + , testCase "CAN use a term of type 'forall a. a -> m a' as 'Int -> Maybe Int'" $ + typeOf (undefined :: Int -> Maybe Int) + `isInstanceOf` +#if MIN_VERSION_base(4,6,0) + typeOf (undefined :: ANY1 -> ANY ANY1) +#else + typeOf (undefined :: ANY1 -> ANY (ANY1 :: *)) +#endif + @?= Right () + + , testCase "CAN use a term of type 'forall a. Monad a => a -> m a' as 'Int -> Maybe Int'" $ +#if MIN_VERSION_base(4,7,0) + typeOf ((\Dict -> return) :: Dict (Monad Maybe) -> Int -> Maybe Int) + `isInstanceOf` + typeOf ((\Dict -> return) :: Dict (Monad ANY) -> ANY1 -> ANY ANY1) +#else + typeOf (returnD :: MonadDict Maybe -> Int -> Maybe Int) + `isInstanceOf` +#if MIN_VERSION_base(4,6,0) + typeOf (returnD :: MonadDict ANY -> ANY1 -> ANY ANY1) +#else + typeOf (returnD :: MonadDict ANY -> ANY1 -> ANY (ANY1 :: *)) +#endif +#endif + @?= Right () + ] + + , testGroup "Examples of funResultTy" + [ testCase "Apply fn of type (forall a. a -> a) to arg of type Bool gives Bool" $ + show (funResultTy (typeOf (undefined :: ANY -> ANY)) (typeOf (undefined :: Bool))) + @?= "Right Bool" + + , testCase "Apply fn of type (forall a b. a -> b -> a) to arg of type Bool gives forall a. a -> Bool" $ + show (funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: Bool))) + @?= "Right (ANY -> Bool)" -- forall a. a -> Bool + + , testCase "Apply fn of type (forall a. (Bool -> a) -> a) to argument of type (forall a. a -> a) gives Bool" $ + show (funResultTy (typeOf (undefined :: (Bool -> ANY) -> ANY)) (typeOf (undefined :: ANY -> ANY))) + @?= "Right Bool" + + , testCase "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)" $ + show (funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: ANY1 -> ANY1))) + @?= "Right (ANY -> ANY1 -> ANY1)" + + , testCase "Cannot apply function of type (forall a. (a -> a) -> a -> a) to arg of type (Int -> Bool)" $ + show (funResultTy (typeOf (undefined :: (ANY -> ANY) -> (ANY -> ANY))) (typeOf (undefined :: Int -> Bool))) + @?= "Left \"Cannot unify Int and Bool\"" + ] + + , testGroup "Examples of fromDynamic" + [ testCase "CANNOT use a term of type 'Int -> Bool' as 'Int -> Int'" $ + do f <- fromDynamic (toDynamic (even :: Int -> Bool)) + return $ (f :: Int -> Int) 0 + @?= Left "Cannot unify Int and Bool" + + , testCase "CAN use a term of type 'forall a. a -> Int' as 'Int -> Int'" $ + do f <- fromDynamic (toDynamic (const 1 :: ANY -> Int)) + return $ (f :: Int -> Int) 0 + @?= Right 1 + + , testCase "CAN use a term of type 'forall a b. a -> b' as 'forall a. a -> a'" $ + do f <- fromDynamic (toDynamic (unsafeCoerce :: ANY1 -> ANY2)) + return $ (f :: Int -> Int) 0 + @?= Right 0 + + , testCase "CANNOT use a term of type 'forall a. a -> a' as 'forall a b. a -> b'" $ + do f <- fromDynamic (toDynamic (id :: ANY -> ANY)) + return $ (f :: Int -> Bool) 0 + @?= Left "Cannot unify Bool and Int" + + , testCase "CAN use a term of type 'forall a. a' as 'forall a. a -> a'" $ + case do f <- fromDynamic (toDynamic (undefined :: ANY)) + return $ (f :: Int -> Int) 0 + of + Right _ -> return () + result -> assertFailure $ "Expected 'Right _' but got '" ++ show result ++ "'" + + , testCase "CANNOT use a term of type 'forall a. a -> a' as 'forall a. a'" $ + do f <- fromDynamic (toDynamic (id :: ANY -> ANY)) ; return $ (f :: Int) +#if MIN_VERSION_base(4,7,0) + @?= Left "Cannot unify Int and (->)" +#else + @?= Left "Cannot unify Int and ->" +#endif + + , testCase "CAN use a term of type 'forall a. Monad a => a -> m a' as 'Int -> Maybe Int'" $ +#if MIN_VERSION_base(4,7,0) + do f <- fromDynamic (toDynamic ((\Dict -> return) :: Dict (Monad Maybe) -> Int -> Maybe Int)) + return $ (f :: Dict (Monad Maybe) -> Int -> Maybe Int) Dict 0 +#else + do f <- fromDynamic (toDynamic (returnD :: MonadDict Maybe -> Int -> Maybe Int)) + return $ ((f :: MonadDict Maybe -> Int -> Maybe Int) MonadDict) 0 +#endif + @?= Right (Just 0) + ] + + , testGroup "Examples of dynApply" + [ testCase "Apply fn of type (forall a. a -> a) to arg of type Bool gives Bool" $ + do app <- toDynamic (id :: ANY -> ANY) `dynApply` toDynamic True + f <- fromDynamic app + return $ (f :: Bool) + @?= Right True + + , testCase "Apply fn of type (forall a b. a -> b -> a) to arg of type Bool gives forall a. a -> Bool" $ + do app <- toDynamic (const :: ANY -> ANY1 -> ANY) `dynApply` toDynamic True + f <- fromDynamic app + return $ (f :: Int -> Bool) 0 + @?= Right True + + , testCase "Apply fn of type (forall a. (Bool -> a) -> a) to argument of type (forall a. a -> a) gives Bool" $ + do app <- toDynamic (($ True) :: (Bool -> ANY) -> ANY) `dynApply` toDynamic (id :: ANY -> ANY) + f <- fromDynamic app + return (f :: Bool) + @?= Right True + + , testCase "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)" $ + do app <- toDynamic (const :: ANY -> ANY1 -> ANY) `dynApply` toDynamic (id :: ANY -> ANY) + f <- fromDynamic app ; return $ (f :: Int -> Bool -> Bool) 0 True + @?= Right True + + , testCase "Cannot apply function of type (forall a. (a -> a) -> a -> a) to arg of type (Int -> Bool)" $ + 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" + ] + ]