@@ -1,8 +1,86 @@
1+-- | Runtime type representation of terms with support for rank-1 polymorphic
2+-- types with type variables of kind *.
3+--
4+-- The essence of this module is that we use the standard 'Typeable'
5+-- representation of "Data.Typeable" but we introduce a special (empty) data
6+-- type 'TypVar' which represents type variables. 'TypVar' is indexed by an
7+-- arbitrary other data type, giving you an unbounded number of type variables;
8+-- for convenience, we define 'ANY', 'ANY1', .., 'ANY9'.
9+--
10+-- [Examples of isInstanceOf]
11+--
12+-- > -- We CANNOT use a term of type 'Int -> Bool' as 'Int -> Int'
13+-- > > typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: Int -> Bool)
14+-- > Left "Cannot unify Int and Bool"
15+-- >
16+-- > -- We CAN use a term of type 'forall a. a -> Int' as 'Int -> Int'
17+-- > > typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: ANY -> Int)
18+-- > Right ()
19+-- >
20+-- > -- We CAN use a term of type 'forall a b. a -> b' as 'forall a. a -> a'
21+-- > > typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY1)
22+-- > Right ()
23+-- >
24+-- > -- We CANNOT use a term of type 'forall a. a -> a' as 'forall a b. a -> b'
25+-- > > typeOf (undefined :: ANY -> ANY1) `isInstanceOf` typeOf (undefined :: ANY -> ANY)
26+-- > Left "Cannot unify Succ and Zero"
27+-- >
28+-- > -- We CAN use a term of type 'forall a. a' as 'forall a. a -> a'
29+-- > > typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY)
30+-- > Right ()
31+-- >
32+-- > -- We CANNOT use a term of type 'forall a. a -> a' as 'forall a. a'
33+-- > > typeOf (undefined :: ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY)
34+-- > Left "Cannot unify Skolem and ->"
35+--
36+-- (Admittedly, the quality of the type errors could be improved.)
37+--
38+-- [Examples of funResultTy]
39+--
40+-- > -- Apply fn of type (forall a. a -> a) to arg of type Bool gives Bool
41+-- > > funResultTy (typeOf (undefined :: ANY -> ANY)) (typeOf (undefined :: Bool))
42+-- > Right Bool
43+-- >
44+-- > -- Apply fn of type (forall a b. a -> b -> a) to arg of type Bool gives forall a. a -> Bool
45+-- > > funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: Bool))
46+-- > Right (ANY -> Bool) -- forall a. a -> Bool
47+-- >
48+-- > -- Apply fn of type (forall a. (Bool -> a) -> a) to argument of type (forall a. a -> a) gives Bool
49+-- > > funResultTy (typeOf (undefined :: (Bool -> ANY) -> ANY)) (typeOf (undefined :: ANY -> ANY))
50+-- > Right Bool
51+-- >
52+-- > -- 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)
53+-- > > funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: ANY1 -> ANY1))
54+-- > Right (ANY -> ANY1 -> ANY1)
55+-- >
56+-- > -- Cannot apply function of type (forall a. (a -> a) -> a -> a) to arg of type (Int -> Bool)
57+-- > > funResultTy (typeOf (undefined :: (ANY -> ANY) -> (ANY -> ANY))) (typeOf (undefined :: Int -> Bool))
58+-- > Left "Cannot unify Int and Bool"
159module Data.Rank1Typeable
2− ( Rank1TypeRep
3− , underlyingTypeRep
60+ ( -- * Basic types
61+ TypeRep
462 , typeOf
63+ , splitTyConApp
64+ , mkTyConApp
65+ , underlyingTypeRep
66+ -- * Operations on type representations
67+ , isInstanceOf
68+ , funResultTy
69+ , TypeError
570 -- * Type variables
71+ , TypVar
72+ , Zero
73+ , Succ
74+ , V0
75+ , V1
76+ , V2
77+ , V3
78+ , V4
79+ , V5
80+ , V6
81+ , V7
82+ , V8
83+ , V9
684 , ANY
785 , ANY1
886 , ANY2
@@ -13,95 +91,240 @@ module Data.Rank1Typeable
1391 , ANY7
1492 , ANY8
1593 , ANY9
16− -- * Internal functions
17− , occurs
18− , subst
19− , unify
94+ -- * Re-exports from Typeable
95+ , Typeable
2096 ) where
2197
22−import Data.Typeable (Typeable, TypeRep, TyCon)
23−import Control.Arrow ((***))
24−import qualified Data.Typeable as Typeable (typeOf, splitTyConApp, mkTyConApp)
98+import Prelude hiding (succ)
99+import Control.Arrow ((***), second)
100+import Control.Monad (void)
101+import Control.Applicative ((<$>))
102+import Data.List (intersperse, isPrefixOf)
103+import Data.Maybe (fromMaybe)
104+import Data.Typeable (Typeable, TyCon, tyConName, mkTyCon3)
105+import Data.Typeable.Internal (listTc, funTc)
106+import qualified Data.Typeable as Typeable
107+ ( TypeRep
108+ , typeOf
109+ , splitTyConApp
110+ , mkTyConApp
111+ )
25112
26−newtype Rank1TypeRep = Rank1TypeRep { underlyingTypeRep :: TypeRep }
113+--------------------------------------------------------------------------------
114+-- The basic type --
115+--------------------------------------------------------------------------------
116+
117+-- | Dynamic type representation with support for rank-1 types
118+newtype TypeRep = TypeRep {
119+ -- | Return the underlying standard ("Data.Typeable") type representation
120+ underlyingTypeRep :: Typeable.TypeRep
121+ }
27122 deriving Eq
28123
29−instance Show Rank1TypeRep where
30− show = show . underlyingTypeRep
31−
32−typeOf :: Typeable a => a -> Rank1TypeRep
33−typeOf = Rank1TypeRep . Typeable.typeOf
34−
35−data ANY deriving Typeable
36−data ANY1 deriving Typeable
37−data ANY2 deriving Typeable
38−data ANY3 deriving Typeable
39−data ANY4 deriving Typeable
40−data ANY5 deriving Typeable
41−data ANY6 deriving Typeable
42−data ANY7 deriving Typeable
43−data ANY8 deriving Typeable
44−data ANY9 deriving Typeable
45−
46−tvars :: [Rank1TypeRep]
47−tvars =
48− [ typeOf (undefined :: ANY)
49− , typeOf (undefined :: ANY1)
50− , typeOf (undefined :: ANY2)
51− , typeOf (undefined :: ANY3)
52− , typeOf (undefined :: ANY4)
53− , typeOf (undefined :: ANY5)
54− , typeOf (undefined :: ANY6)
55− , typeOf (undefined :: ANY7)
56− , typeOf (undefined :: ANY8)
57− , typeOf (undefined :: ANY9)
58− ]
59−
60−isTVar :: Rank1TypeRep -> Bool
61−isTVar = flip elem tvars
62−
63−splitTyConApp :: Rank1TypeRep -> (TyCon, [Rank1TypeRep])
124+-- | The type representation of any 'Typeable' term
125+typeOf :: Typeable a => a -> TypeRep
126+typeOf = TypeRep . Typeable.typeOf
127+
128+--------------------------------------------------------------------------------
129+-- Constructors/destructors (views) --
130+--------------------------------------------------------------------------------
131+
132+-- | Split a type representation into the application of
133+-- a type constructor and its argument
134+splitTyConApp :: TypeRep -> (TyCon, [TypeRep])
64135splitTyConApp t =
65136 let (c, ts) = Typeable.splitTyConApp (underlyingTypeRep t)
66− in (c, map Rank1TypeRep ts)
137+ in (c, map TypeRep ts)
67138
68−mkTyConApp :: TyCon -> [Rank1TypeRep] -> Rank1TypeRep
139+-- | Inverse of 'splitTyConApp'
140+mkTyConApp :: TyCon -> [TypeRep] -> TypeRep
69141mkTyConApp c ts
70− = Rank1TypeRep (Typeable.mkTyConApp c (map underlyingTypeRep ts))
71−
72−occurs :: Rank1TypeRep -> Rank1TypeRep -> Bool
73−occurs x t
74− | x == t = True
75− | otherwise = let (_, ts) = splitTyConApp t
76− in any (occurs x) ts
77−
78−subst :: Rank1TypeRep -> Rank1TypeRep -> Rank1TypeRep -> Rank1TypeRep
79−subst x t t'
80− | x == t' = t
81− | otherwise = let (c, ts) = splitTyConApp t'
82− in mkTyConApp c (map (subst x t) ts)
83−
84−unify :: Monad m => Rank1TypeRep -> Rank1TypeRep -> m [(Rank1TypeRep, Rank1TypeRep)]
85−unify t1 t2 = unify' [(t1, t2)]
86−
87−unify' :: Monad m
88− => [(Rank1TypeRep, Rank1TypeRep)]
89− -> m [(Rank1TypeRep, Rank1TypeRep)]
90−unify' [] =
91− return []
92−unify' ((x, t) : eqs) | isTVar x && not (isTVar t) =
93− if x `occurs` t
94− then fail "Occurs check"
95− else do
96− s <- unify' (map (subst x t *** subst x t) eqs)
97− return ((x, t) : s)
98−unify' ((t, x) : eqs) | isTVar x && not (isTVar t) =
99− unify' ((x, t) : eqs)
100−unify' ((x, x') : eqs) | isTVar x && isTVar x' && x == x' =
101− unify' eqs
102−unify' ((t1, t2) : eqs) = do
103− let (c1, ts1) = splitTyConApp t1
104− (c2, ts2) = splitTyConApp t2
105− if c1 /= c2
106− then fail $ "Cannot unify' " ++ show c1 ++ " and " ++ show c2
107− else unify' (zip ts1 ts2 ++ eqs)
142+ = TypeRep (Typeable.mkTyConApp c (map underlyingTypeRep ts))
143+
144+isTypVar :: TypeRep -> Maybe Var
145+isTypVar (splitTyConApp -> (c, [t])) | c == typVar = Just t
146+isTypVar _ = Nothing
147+
148+mkTypVar :: Var -> TypeRep
149+mkTypVar x = mkTyConApp typVar [x]
150+
151+typVar :: TyCon
152+typVar = let (c, _) = splitTyConApp (typeOf (undefined :: TypVar V0)) in c
153+
154+skolem :: TyCon
155+skolem = let (c, _) = splitTyConApp (typeOf (undefined :: Skolem V0)) in c
156+
157+--------------------------------------------------------------------------------
158+-- Type variables --
159+--------------------------------------------------------------------------------
160+
161+data TypVar a deriving Typeable
162+data Skolem a deriving Typeable
163+data Zero deriving Typeable
164+data Succ a deriving Typeable
165+
166+type V0 = Zero
167+type V1 = Succ V0
168+type V2 = Succ V1
169+type V3 = Succ V2
170+type V4 = Succ V3
171+type V5 = Succ V4
172+type V6 = Succ V5
173+type V7 = Succ V6
174+type V8 = Succ V7
175+type V9 = Succ V8
176+
177+type ANY = TypVar V0
178+type ANY1 = TypVar V1
179+type ANY2 = TypVar V2
180+type ANY3 = TypVar V3
181+type ANY4 = TypVar V4
182+type ANY5 = TypVar V5
183+type ANY6 = TypVar V6
184+type ANY7 = TypVar V7
185+type ANY8 = TypVar V8
186+type ANY9 = TypVar V9
187+
188+--------------------------------------------------------------------------------
189+-- Operations on type reps --
190+--------------------------------------------------------------------------------
191+
192+-- | If 'isInstanceOf' fails it returns a type error
193+type TypeError = String
194+
195+-- | @t1 `isInstanceOf` t2@ checks if @t1@ is an instance of @t2@
196+isInstanceOf :: TypeRep -> TypeRep -> Either TypeError ()
197+isInstanceOf t1 t2 = void (unify (skolemize t1) t2)
198+
199+-- | @funResultTy t1 t2@ is the type of the result when applying a function
200+-- of type @t1@ to an argument of type @t2@
201+funResultTy :: TypeRep -> TypeRep -> Either TypeError TypeRep
202+funResultTy (splitTyConApp -> (fc, [farg, fres])) x | fc == funTc = do
203+ s <- unify (alphaRename "f" farg) (alphaRename "x" x)
204+ return (normalize (subst s (alphaRename "f" fres)))
205+funResultTy f _ =
206+ Left $ show f ++ " is not a function"
207+
208+--------------------------------------------------------------------------------
209+-- Alpha-renaming and normalization --
210+--------------------------------------------------------------------------------
211+
212+alphaRename :: String -> TypeRep -> TypeRep
213+alphaRename prefix (isTypVar -> Just x) =
214+ mkTypVar (mkTyConApp (mkTyCon prefix) [x])
215+alphaRename prefix (splitTyConApp -> (c, ts)) =
216+ mkTyConApp c (map (alphaRename prefix) ts)
217+
218+tvars :: TypeRep -> [Var]
219+tvars (isTypVar -> Just x) = [x]
220+tvars (splitTyConApp -> (_, ts)) = concatMap tvars ts
221+
222+normalize :: TypeRep -> TypeRep
223+normalize t = subst (zip (tvars t) anys) t
224+ where
225+ anys :: [TypeRep]
226+ anys = map mkTypVar (iterate succ zero)
227+
228+ succ :: TypeRep -> TypeRep
229+ succ = mkTyConApp succTyCon . (:[])
230+
231+ zero :: TypeRep
232+ zero = mkTyConApp zeroTyCon []
233+
234+mkTyCon :: String -> TyCon
235+mkTyCon = mkTyCon3 "rank1typeable" "Data.Rank1Typeable"
236+
237+succTyCon :: TyCon
238+succTyCon = let (c, _) = splitTyConApp (typeOf (undefined :: Succ Zero)) in c
239+
240+zeroTyCon :: TyCon
241+zeroTyCon = let (c, _) = splitTyConApp (typeOf (undefined :: Zero)) in c
242+
243+--------------------------------------------------------------------------------
244+-- Unification --
245+--------------------------------------------------------------------------------
246+
247+type Substitution = [(Var, TypeRep)]
248+type Equation = (TypeRep, TypeRep)
249+type Var = TypeRep
250+
251+skolemize :: TypeRep -> TypeRep
252+skolemize (isTypVar -> Just x) = mkTyConApp skolem [x]
253+skolemize (splitTyConApp -> (c, ts)) = mkTyConApp c (map skolemize ts)
254+
255+occurs :: Var -> TypeRep -> Bool
256+occurs x (isTypVar -> Just x') = x == x'
257+occurs x (splitTyConApp -> (_, ts)) = any (occurs x) ts
258+
259+subst :: Substitution -> TypeRep -> TypeRep
260+subst s (isTypVar -> Just x) = fromMaybe (mkTypVar x) (lookup x s)
261+subst s (splitTyConApp -> (c, ts)) = mkTyConApp c (map (subst s) ts)
262+
263+unify :: TypeRep
264+ -> TypeRep
265+ -> Either TypeError Substitution
266+unify = \t1 t2 -> go [] [(t1, t2)]
267+ where
268+ go :: Substitution
269+ -> [Equation]
270+ -> Either TypeError Substitution
271+ go acc [] =
272+ return acc
273+ go acc ((t1, t2) : eqs) | t1 == t2 = -- Note: equality check is fast
274+ go acc eqs
275+ go acc ((isTypVar -> Just x, t) : eqs) =
276+ if x `occurs` t
277+ then Left "Occurs check"
278+ else go ((x, t) : map (second $ subst [(x, t)]) acc)
279+ (map (subst [(x, t)] *** subst [(x, t)]) eqs)
280+ go acc ((t, isTypVar -> Just x) : eqs) =
281+ go acc ((mkTypVar x, t) : eqs)
282+ go acc ((splitTyConApp -> (c1, ts1), splitTyConApp -> (c2, ts2)) : eqs) =
283+ if c1 /= c2
284+ then Left $ "Cannot unify " ++ show c1 ++ " and " ++ show c2
285+ else go acc (zip ts1 ts2 ++ eqs)
286+
287+--------------------------------------------------------------------------------
288+-- Pretty-printing --
289+--------------------------------------------------------------------------------
290+
291+instance Show TypeRep where
292+ showsPrec p (splitTyConApp -> (tycon, tys)) =
293+ case tys of
294+ [] -> showsPrec p tycon
295+ [anyIdx -> Just i] | tycon == typVar -> showString "ANY" . showIdx i
296+ [x] | tycon == listTc ->
297+ showChar '[' . shows x . showChar ']'
298+ [a,r] | tycon == funTc ->
299+ showParen (p > 8) $ showsPrec 9 a
300+ . showString " -> "
301+ . showsPrec 8 r
302+ xs | isTupleTyCon tycon ->
303+ showTuple xs
304+ _ ->
305+ showParen (p > 9) $ showsPrec p tycon
306+ . showChar ' '
307+ . showArgs tys
308+ where
309+ showIdx 0 = showString ""
310+ showIdx i = shows i
311+
312+showArgs :: Show a => [a] -> ShowS
313+showArgs [] = id
314+showArgs [a] = showsPrec 10 a
315+showArgs (a:as) = showsPrec 10 a . showString " " . showArgs as
316+
317+anyIdx :: TypeRep -> Maybe Int
318+anyIdx (splitTyConApp -> (c, [])) | c == zeroTyCon = Just 0
319+anyIdx (splitTyConApp -> (c, [t])) | c == succTyCon = (+1) <$> anyIdx t
320+anyIdx _ = Nothing
321+
322+showTuple :: [TypeRep] -> ShowS
323+showTuple args = showChar '('
324+ . foldr (.) id ( intersperse (showChar ',')
325+ $ map (showsPrec 10) args
326+ )
327+ . showChar ')'
328+
329+isTupleTyCon :: TyCon -> Bool
330+isTupleTyCon = isPrefixOf "(," . tyConName