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