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