git.iko.soy/rowtype-yoga/purescript-native
on 8758966 help sign in
rowtype-yoga/purescript-native/src/Language/PureScript/Types.hs
327 lines 11 kB history raw
1-----------------------------------------------------------------------------
2--
3-- Module : Language.PureScript.Types
4-- Copyright : (c) Phil Freeman 2013
5-- License : MIT
6--
7-- Maintainer : Phil Freeman <paf31@cantab.net>
8-- Stability : experimental
9-- Portability :
10--
11-- |
12-- Data types for types
13--
14-----------------------------------------------------------------------------
16{-# LANGUAGE DeriveDataTypeable #-}
17{-# LANGUAGE GeneralizedNewtypeDeriving #-}
18{-# LANGUAGE TemplateHaskell #-}
19{-# LANGUAGE CPP #-}
21module Language.PureScript.Types where
23import Data.Data
24import Data.List (nub)
25import Data.Maybe (fromMaybe)
26import qualified Data.Aeson as A
27import qualified Data.Aeson.TH as A
29import Control.Monad.Unify
30import Control.Arrow (second)
31#if __GLASGOW_HASKELL__ < 710
32import Control.Applicative
33#endif
34import Control.Monad ((<=<))
36import Language.PureScript.Names
37import Language.PureScript.Kinds
38import Language.PureScript.Traversals
40-- |
41-- An identifier for the scope of a skolem variable
42--
43newtype SkolemScope = SkolemScope { runSkolemScope :: Int } deriving (Show, Read, Eq, Ord, Data, Typeable, A.ToJSON, A.FromJSON)
45-- |
46-- The type of types
47--
48data Type
49 -- |
50 -- A unification variable of type Type
51 --
52 = TUnknown Unknown
53 -- |
54 -- A named type variable
55 --
56 | TypeVar String
57 -- |
58 -- A type wildcard, as would appear in a partial type synonym
59 --
60 | TypeWildcard
61 -- |
62 -- A type constructor
63 --
64 | TypeConstructor (Qualified ProperName)
65 -- |
66 -- A type application
67 --
68 | TypeApp Type Type
69 -- |
70 -- A type synonym which is \"saturated\", i.e. fully applied
71 --
72 | SaturatedTypeSynonym (Qualified ProperName) [Type]
73 -- |
74 -- Forall quantifier
75 --
76 | ForAll String Type (Maybe SkolemScope)
77 -- |
78 -- A type with a set of type class constraints
79 --
80 | ConstrainedType [Constraint] Type
81 -- |
82 -- A skolem constant
83 --
84 | Skolem String Int SkolemScope
85 -- |
86 -- An empty row
87 --
88 | REmpty
89 -- |
90 -- A non-empty row
91 --
92 | RCons String Type Type
93 -- |
94 -- A type with a kind annotation
95 --
96 | KindedType Type Kind
97 --
98 -- |
99 -- A placeholder used in pretty printing
100 --
101 | PrettyPrintFunction Type Type
102 -- |
103 -- A placeholder used in pretty printing
104 --
105 | PrettyPrintObject Type
106 -- |
107 -- A placeholder used in pretty printing
108 --
109 | PrettyPrintForAll [String] Type deriving (Show, Read,Eq, Ord, Data, Typeable)
111-- |
112-- A typeclass constraint
113--
114type Constraint = (Qualified ProperName, [Type])
116$(A.deriveJSON A.defaultOptions ''Type)
118-- |
119-- Convert a row to a list of pairs of labels and types
120--
121rowToList :: Type -> ([(String, Type)], Type)
122rowToList (RCons name ty row) = let (tys, rest) = rowToList row
123 in ((name, ty):tys, rest)
124rowToList r = ([], r)
126-- |
127-- Convert a list of labels and types to a row
128--
129rowFromList :: ([(String, Type)], Type) -> Type
130rowFromList ([], r) = r
131rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
133-- |
134-- Check whether a type is a monotype
135--
136isMonoType :: Type -> Bool
137isMonoType ForAll{} = False
138isMonoType _ = True
140-- |
141-- Universally quantify a type
142--
143mkForAll :: [String] -> Type -> Type
144mkForAll args ty = foldl (\t arg -> ForAll arg t Nothing) ty args
146-- |
147-- Replace a type variable, taking into account variable shadowing
148--
149replaceTypeVars :: String -> Type -> Type -> Type
150replaceTypeVars v r = replaceAllTypeVars [(v, r)]
152-- |
153-- Replace named type variables with types
154--
155replaceAllTypeVars :: [(String, Type)] -> Type -> Type
156replaceAllTypeVars = go []
157 where
159 go :: [String] -> [(String, Type)] -> Type -> Type
160 go _ m (TypeVar v) = fromMaybe (TypeVar v) (v `lookup` m)
161 go bs m (TypeApp t1 t2) = TypeApp (go bs m t1) (go bs m t2)
162 go bs m (SaturatedTypeSynonym name' ts) = SaturatedTypeSynonym name' $ map (go bs m) ts
163 go bs m f@(ForAll v t sco) | v `elem` keys = go bs (filter ((/= v) . fst) m) f
164 | v `elem` usedVars =
165 let v' = genName v (keys ++ bs ++ usedVars)
166 t' = go bs [(v, TypeVar v')] t
167 in ForAll v' (go (v' : bs) m t') sco
168 | otherwise = ForAll v (go (v : bs) m t) sco
169 where
170 keys = map fst m
171 usedVars = concatMap (usedTypeVariables . snd) m
172 go bs m (ConstrainedType cs t) = ConstrainedType (map (second $ map (go bs m)) cs) (go bs m t)
173 go bs m (RCons name' t r) = RCons name' (go bs m t) (go bs m r)
174 go bs m (KindedType t k) = KindedType (go bs m t) k
175 go _ _ ty = ty
177 genName orig inUse = try 0
178 where
179 try :: Integer -> String
180 try n | (orig ++ show n) `elem` inUse = try (n + 1)
181 | otherwise = orig ++ show n
183-- |
184-- Collect all type variables appearing in a type
185--
186usedTypeVariables :: Type -> [String]
187usedTypeVariables = nub . everythingOnTypes (++) go
188 where
189 go (TypeVar v) = [v]
190 go _ = []
192-- |
193-- Collect all free type variables appearing in a type
194--
195freeTypeVariables :: Type -> [String]
196freeTypeVariables = nub . go []
197 where
198 go :: [String] -> Type -> [String]
199 go bound (TypeVar v) | v `notElem` bound = [v]
200 go bound (TypeApp t1 t2) = go bound t1 ++ go bound t2
201 go bound (SaturatedTypeSynonym _ ts) = concatMap (go bound) ts
202 go bound (ForAll v t _) = go (v : bound) t
203 go bound (ConstrainedType cs t) = concatMap (concatMap (go bound) . snd) cs ++ go bound t
204 go bound (RCons _ t r) = go bound t ++ go bound r
205 go bound (KindedType t _) = go bound t
206 go _ _ = []
208-- |
209-- Universally quantify over all type variables appearing free in a type
210--
211quantify :: Type -> Type
212quantify ty = foldr (\arg t -> ForAll arg t Nothing) ty $ freeTypeVariables ty
214-- |
215-- Move all universal quantifiers to the front of a type
216--
217moveQuantifiersToFront :: Type -> Type
218moveQuantifiersToFront = go [] []
219 where
220 go qs cs (ForAll q ty sco) = go ((q, sco) : qs) cs ty
221 go qs cs (ConstrainedType cs' ty) = go qs (cs ++ cs') ty
222 go qs cs ty =
223 let constrained = case cs of
224 [] -> ty
225 cs' -> ConstrainedType cs' ty
226 in case qs of
227 [] -> constrained
228 qs' -> foldl (\ty' (q, sco) -> ForAll q ty' sco) constrained qs'
230-- |
231-- Check if a type contains wildcards
232--
233containsWildcards :: Type -> Bool
234containsWildcards = everythingOnTypes (||) go
235 where
236 go :: Type -> Bool
237 go TypeWildcard = True
238 go _ = False
240--
241-- Traversals
242--
244everywhereOnTypes :: (Type -> Type) -> Type -> Type
245everywhereOnTypes f = go
246 where
247 go (TypeApp t1 t2) = f (TypeApp (go t1) (go t2))
248 go (SaturatedTypeSynonym name tys) = f (SaturatedTypeSynonym name (map go tys))
249 go (ForAll arg ty sco) = f (ForAll arg (go ty) sco)
250 go (ConstrainedType cs ty) = f (ConstrainedType (map (fmap (map go)) cs) (go ty))
251 go (RCons name ty rest) = f (RCons name (go ty) (go rest))
252 go (KindedType ty k) = f (KindedType (go ty) k)
253 go (PrettyPrintFunction t1 t2) = f (PrettyPrintFunction (go t1) (go t2))
254 go (PrettyPrintObject t) = f (PrettyPrintObject (go t))
255 go (PrettyPrintForAll args t) = f (PrettyPrintForAll args (go t))
256 go other = f other
258everywhereOnTypesTopDown :: (Type -> Type) -> Type -> Type
259everywhereOnTypesTopDown f = go . f
260 where
261 go (TypeApp t1 t2) = TypeApp (go (f t1)) (go (f t2))
262 go (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name (map (go . f) tys)
263 go (ForAll arg ty sco) = ForAll arg (go (f ty)) sco
264 go (ConstrainedType cs ty) = ConstrainedType (map (fmap (map (go . f))) cs) (go (f ty))
265 go (RCons name ty rest) = RCons name (go (f ty)) (go (f rest))
266 go (KindedType ty k) = KindedType (go (f ty)) k
267 go (PrettyPrintFunction t1 t2) = PrettyPrintFunction (go (f t1)) (go (f t2))
268 go (PrettyPrintObject t) = PrettyPrintObject (go (f t))
269 go (PrettyPrintForAll args t) = PrettyPrintForAll args (go (f t))
270 go other = f other
272everywhereOnTypesM :: (Functor m, Applicative m, Monad m) => (Type -> m Type) -> Type -> m Type
273everywhereOnTypesM f = go
274 where
275 go (TypeApp t1 t2) = (TypeApp <$> go t1 <*> go t2) >>= f
276 go (SaturatedTypeSynonym name tys) = (SaturatedTypeSynonym name <$> mapM go tys) >>= f
277 go (ForAll arg ty sco) = (ForAll arg <$> go ty <*> pure sco) >>= f
278 go (ConstrainedType cs ty) = (ConstrainedType <$> mapM (sndM (mapM go)) cs <*> go ty) >>= f
279 go (RCons name ty rest) = (RCons name <$> go ty <*> go rest) >>= f
280 go (KindedType ty k) = (KindedType <$> go ty <*> pure k) >>= f
281 go (PrettyPrintFunction t1 t2) = (PrettyPrintFunction <$> go t1 <*> go t2) >>= f
282 go (PrettyPrintObject t) = (PrettyPrintObject <$> go t) >>= f
283 go (PrettyPrintForAll args t) = (PrettyPrintForAll args <$> go t) >>= f
284 go other = f other
286everywhereOnTypesTopDownM :: (Functor m, Applicative m, Monad m) => (Type -> m Type) -> Type -> m Type
287everywhereOnTypesTopDownM f = go <=< f
288 where
289 go (TypeApp t1 t2) = TypeApp <$> (f t1 >>= go) <*> (f t2 >>= go)
290 go (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name <$> mapM (go <=< f) tys
291 go (ForAll arg ty sco) = ForAll arg <$> (f ty >>= go) <*> pure sco
292 go (ConstrainedType cs ty) = ConstrainedType <$> mapM (sndM (mapM (go <=< f))) cs <*> (f ty >>= go)
293 go (RCons name ty rest) = RCons name <$> (f ty >>= go) <*> (f rest >>= go)
294 go (KindedType ty k) = KindedType <$> (f ty >>= go) <*> pure k
295 go (PrettyPrintFunction t1 t2) = PrettyPrintFunction <$> (f t1 >>= go) <*> (f t2 >>= go)
296 go (PrettyPrintObject t) = PrettyPrintObject <$> (f t >>= go)
297 go (PrettyPrintForAll args t) = PrettyPrintForAll args <$> (f t >>= go)
298 go other = f other
300everythingOnTypes :: (r -> r -> r) -> (Type -> r) -> Type -> r
301everythingOnTypes (<>) f = go
302 where
303 go t@(TypeApp t1 t2) = f t <> go t1 <> go t2
304 go t@(SaturatedTypeSynonym _ tys) = foldl (<>) (f t) (map go tys)
305 go t@(ForAll _ ty _) = f t <> go ty
306 go t@(ConstrainedType cs ty) = foldl (<>) (f t) (map go $ concatMap snd cs) <> go ty
307 go t@(RCons _ ty rest) = f t <> go ty <> go rest
308 go t@(KindedType ty _) = f t <> go ty
309 go t@(PrettyPrintFunction t1 t2) = f t <> go t1 <> go t2
310 go t@(PrettyPrintObject t1) = f t <> go t1
311 go t@(PrettyPrintForAll _ t1) = f t <> go t1
312 go other = f other
314everythingWithContextOnTypes :: s -> r -> (r -> r -> r) -> (s -> Type -> (s, r)) -> Type -> r
315everythingWithContextOnTypes s0 r0 (<>) f = go' s0
316 where
317 go' s t = let (s', r) = f s t in r <> go s' t
318 go s (TypeApp t1 t2) = go' s t1 <> go' s t2
319 go s (SaturatedTypeSynonym _ tys) = foldl (<>) r0 (map (go' s) tys)
320 go s (ForAll _ ty _) = go' s ty
321 go s (ConstrainedType cs ty) = foldl (<>) r0 (map (go' s) $ concatMap snd cs) <> go' s ty
322 go s (RCons _ ty rest) = go' s ty <> go' s rest
323 go s (KindedType ty _) = go' s ty
324 go s (PrettyPrintFunction t1 t2) = go' s t1 <> go' s t2
325 go s (PrettyPrintObject t1) = go' s t1
326 go s (PrettyPrintForAll _ t1) = go' s t1
327 go _ _ = r0