git.iko.soy/rowtype-yoga/purescript-native
on 4dbd9f9 help sign in
rowtype-yoga/purescript-native/src/Language/PureScript/Types.hs
282 lines 9.4 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 #-}
18module Language.PureScript.Types where
20import Data.Data
21import Data.List (nub)
23import Control.Monad.Unify
24import Control.Arrow (second)
25import Control.Applicative
26import Control.Monad ((<=<))
28import Language.PureScript.Names
29import Language.PureScript.Traversals
31-- |
32-- An identifier for the scope of a skolem variable
33--
34newtype SkolemScope = SkolemScope { runSkolemScope :: Int } deriving (Show, Eq, Ord, Data, Typeable)
36-- |
37-- The type of types
38--
39data Type
40 -- |
41 -- A unification variable of type Type
42 --
43 = TUnknown Unknown
44 -- |
45 -- A named type variable
46 --
47 | TypeVar String
48 -- |
49 -- A type constructor
50 --
51 | TypeConstructor (Qualified ProperName)
52 -- |
53 -- A type application
54 --
55 | TypeApp Type Type
56 -- |
57 -- A type synonym which is \"saturated\", i.e. fully applied
58 --
59 | SaturatedTypeSynonym (Qualified ProperName) [Type]
60 -- |
61 -- Forall quantifier
62 --
63 | ForAll String Type (Maybe SkolemScope)
64 -- |
65 -- A type with a set of type class constraints
66 --
67 | ConstrainedType [(Qualified ProperName, [Type])] Type
68 -- |
69 -- A skolem constant
70 --
71 | Skolem String Int SkolemScope
72 -- |
73 -- An empty row
74 --
75 | REmpty
76 -- |
77 -- A non-empty row
78 --
79 | RCons String Type Type
80 -- |
81 -- A placeholder used in pretty printing
82 --
83 | PrettyPrintFunction Type Type
84 -- |
85 -- A placeholder used in pretty printing
86 --
87 | PrettyPrintArray Type
88 -- |
89 -- A placeholder used in pretty printing
90 --
91 | PrettyPrintObject Type
92 -- |
93 -- A placeholder used in pretty printing
94 --
95 | PrettyPrintForAll [String] Type deriving (Show, Eq, Data, Typeable)
97-- |
98-- Convert a row to a list of pairs of labels and types
99--
100rowToList :: Type -> ([(String, Type)], Type)
101rowToList (RCons name ty row) = let (tys, rest) = rowToList row
102 in ((name, ty):tys, rest)
103rowToList r = ([], r)
105-- |
106-- Convert a list of labels and types to a row
107--
108rowFromList :: ([(String, Type)], Type) -> Type
109rowFromList ([], r) = r
110rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
112-- |
113-- Check whether a type is a monotype
114--
115isMonoType :: Type -> Bool
116isMonoType ForAll{} = False
117isMonoType _ = True
119-- |
120-- Universally quantify a type
121--
122mkForAll :: [String] -> Type -> Type
123mkForAll args ty = foldl (\t arg -> ForAll arg t Nothing) ty args
125-- |
126-- Replace a type variable, taking into account variable shadowing
127--
128replaceTypeVars :: String -> Type -> Type -> Type
129replaceTypeVars v r = replaceAllTypeVars [(v, r)]
131-- |
132-- Replace named type variables with types
133--
134replaceAllTypeVars :: [(String, Type)] -> Type -> Type
135replaceAllTypeVars = go []
136 where
138 go :: [String] -> [(String, Type)] -> Type -> Type
139 go _ m (TypeVar v) =
140 case v `lookup` m of
141 Just r -> r
142 Nothing -> TypeVar v
143 go bs m (TypeApp t1 t2) = TypeApp (go bs m t1) (go bs m t2)
144 go bs m (SaturatedTypeSynonym name' ts) = SaturatedTypeSynonym name' $ map (go bs m) ts
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 _ _ ty = ty
158 genName orig inUse = try 0
159 where
160 try :: Integer -> String
161 try n | (orig ++ show n) `elem` inUse = try (n + 1)
162 | otherwise = orig ++ show n
164-- |
165-- Collect all type variables appearing in a type
166--
167usedTypeVariables :: Type -> [String]
168usedTypeVariables = nub . everythingOnTypes (++) go
169 where
170 go (TypeVar v) = [v]
171 go _ = []
173-- |
174-- Collect all free type variables appearing in a type
175--
176freeTypeVariables :: Type -> [String]
177freeTypeVariables = nub . go []
178 where
179 go :: [String] -> Type -> [String]
180 go bound (TypeVar v) | v `notElem` bound = [v]
181 go bound (TypeApp t1 t2) = go bound t1 ++ go bound t2
182 go bound (SaturatedTypeSynonym _ ts) = concatMap (go bound) ts
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 _ _ = []
188-- |
189-- Universally quantify over all type variables appearing free in a type
190--
191quantify :: Type -> Type
192quantify ty = foldr (\arg t -> ForAll arg t Nothing) ty $ freeTypeVariables ty
194-- |
195-- Move all universal quantifiers to the front of a type
196--
197moveQuantifiersToFront :: Type -> Type
198moveQuantifiersToFront = go [] []
199 where
200 go qs cs (ForAll q ty sco) = go ((q, sco) : qs) cs ty
201 go qs cs (ConstrainedType cs' ty) = go qs (cs ++ cs') ty
202 go qs cs ty =
203 let constrained = case cs of
204 [] -> ty
205 cs' -> ConstrainedType cs' ty
206 in case qs of
207 [] -> constrained
208 qs' -> foldl (\ty' (q, sco) -> ForAll q ty' sco) constrained qs'
210--
211-- Traversals
212--
214everywhereOnTypes :: (Type -> Type) -> Type -> Type
215everywhereOnTypes f = go
216 where
217 go (TypeApp t1 t2) = f (TypeApp (go t1) (go t2))
218 go (SaturatedTypeSynonym name tys) = f (SaturatedTypeSynonym name (map go tys))
219 go (ForAll arg ty sco) = f (ForAll arg (go ty) sco)
220 go (ConstrainedType cs ty) = f (ConstrainedType (map (fmap (map go)) cs) (go ty))
221 go (RCons name ty rest) = f (RCons name (go ty) (go rest))
222 go (PrettyPrintFunction t1 t2) = f (PrettyPrintFunction (go t1) (go t2))
223 go (PrettyPrintArray t) = f (PrettyPrintArray (go t))
224 go (PrettyPrintObject t) = f (PrettyPrintObject (go t))
225 go (PrettyPrintForAll args t) = f (PrettyPrintForAll args (go t))
226 go other = f other
228everywhereOnTypesTopDown :: (Type -> Type) -> Type -> Type
229everywhereOnTypesTopDown f = go . f
230 where
231 go (TypeApp t1 t2) = TypeApp (go (f t1)) (go (f t2))
232 go (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name (map (go . f) tys)
233 go (ForAll arg ty sco) = ForAll arg (go (f ty)) sco
234 go (ConstrainedType cs ty) = ConstrainedType (map (fmap (map (go . f))) cs) (go (f ty))
235 go (RCons name ty rest) = RCons name (go (f ty)) (go (f rest))
236 go (PrettyPrintFunction t1 t2) = PrettyPrintFunction (go (f t1)) (go (f t2))
237 go (PrettyPrintArray t) = PrettyPrintArray (go (f t))
238 go (PrettyPrintObject t) = PrettyPrintObject (go (f t))
239 go (PrettyPrintForAll args t) = PrettyPrintForAll args (go (f t))
240 go other = f other
242everywhereOnTypesM :: (Functor m, Applicative m, Monad m) => (Type -> m Type) -> Type -> m Type
243everywhereOnTypesM f = go
244 where
245 go (TypeApp t1 t2) = (TypeApp <$> go t1 <*> go t2) >>= f
246 go (SaturatedTypeSynonym name tys) = (SaturatedTypeSynonym name <$> mapM go tys) >>= f
247 go (ForAll arg ty sco) = (ForAll arg <$> go ty <*> pure sco) >>= f
248 go (ConstrainedType cs ty) = (ConstrainedType <$> mapM (sndM (mapM go)) cs <*> go ty) >>= f
249 go (RCons name ty rest) = (RCons name <$> go ty <*> go rest) >>= f
250 go (PrettyPrintFunction t1 t2) = (PrettyPrintFunction <$> go t1 <*> go t2) >>= f
251 go (PrettyPrintArray t) = (PrettyPrintArray <$> go t) >>= f
252 go (PrettyPrintObject t) = (PrettyPrintObject <$> go t) >>= f
253 go (PrettyPrintForAll args t) = (PrettyPrintForAll args <$> go t) >>= f
254 go other = f other
256everywhereOnTypesTopDownM :: (Functor m, Applicative m, Monad m) => (Type -> m Type) -> Type -> m Type
257everywhereOnTypesTopDownM f = go <=< f
258 where
259 go (TypeApp t1 t2) = TypeApp <$> (f t1 >>= go) <*> (f t2 >>= go)
260 go (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name <$> mapM (go <=< f) tys
261 go (ForAll arg ty sco) = ForAll arg <$> (f ty >>= go) <*> pure sco
262 go (ConstrainedType cs ty) = ConstrainedType <$> mapM (sndM (mapM (go <=< f))) cs <*> (f ty >>= go)
263 go (RCons name ty rest) = RCons name <$> (f ty >>= go) <*> (f rest >>= go)
264 go (PrettyPrintFunction t1 t2) = PrettyPrintFunction <$> (f t1 >>= go) <*> (f t2 >>= go)
265 go (PrettyPrintArray t) = PrettyPrintArray <$> (f t >>= go)
266 go (PrettyPrintObject t) = PrettyPrintObject <$> (f t >>= go)
267 go (PrettyPrintForAll args t) = PrettyPrintForAll args <$> (f t >>= go)
268 go other = f other
270everythingOnTypes :: (r -> r -> r) -> (Type -> r) -> Type -> r
271everythingOnTypes (<>) f = go
272 where
273 go t@(TypeApp t1 t2) = f t <> go t1 <> go t2
274 go t@(SaturatedTypeSynonym _ tys) = foldl (<>) (f t) (map go tys)
275 go t@(ForAll _ ty _) = f t <> go ty
276 go t@(ConstrainedType cs ty) = foldl (<>) (f t) (map go $ concatMap snd cs) <> go ty
277 go t@(RCons _ ty rest) = f t <> go ty <> go rest
278 go t@(PrettyPrintFunction t1 t2) = f t <> go t1 <> go t2
279 go t@(PrettyPrintArray t1) = f t <> go t1
280 go t@(PrettyPrintObject t1) = f t <> go t1
281 go t@(PrettyPrintForAll _ t1) = f t <> go t1
282 go other = f other