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