git.iko.soy/rowtype-yoga/purescript-native
on 4b08ade help sign in
rowtype-yoga/purescript-native/src/Language/PureScript/Types.hs
289 lines 9.9 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.Kinds
30import Language.PureScript.Traversals
32-- |
33-- An identifier for the scope of a skolem variable
34--
35newtype SkolemScope = SkolemScope { runSkolemScope :: Int } deriving (Show, Eq, Ord, Data, Typeable)
37-- |
38-- The type of types
39--
40data Type
41 -- |
42 -- A unification variable of type Type
43 --
44 = TUnknown Unknown
45 -- |
46 -- A named type variable
47 --
48 | TypeVar String
49 -- |
50 -- A type constructor
51 --
52 | TypeConstructor (Qualified ProperName)
53 -- |
54 -- A type application
55 --
56 | TypeApp Type Type
57 -- |
58 -- A type synonym which is \"saturated\", i.e. fully applied
59 --
60 | SaturatedTypeSynonym (Qualified ProperName) [Type]
61 -- |
62 -- Forall quantifier
63 --
64 | ForAll String Type (Maybe SkolemScope)
65 -- |
66 -- A type with a set of type class constraints
67 --
68 | ConstrainedType [(Qualified ProperName, [Type])] Type
69 -- |
70 -- A skolem constant
71 --
72 | Skolem String Int SkolemScope
73 -- |
74 -- An empty row
75 --
76 | REmpty
77 -- |
78 -- A non-empty row
79 --
80 | RCons String Type Type
81 -- |
82 -- A type with a kind annotation
83 --
84 | KindedType Type Kind
85 --
86 -- |
87 -- A placeholder used in pretty printing
88 --
89 | PrettyPrintFunction Type Type
90 -- |
91 -- A placeholder used in pretty printing
92 --
93 | PrettyPrintArray Type
94 -- |
95 -- A placeholder used in pretty printing
96 --
97 | PrettyPrintObject Type
98 -- |
99 -- A placeholder used in pretty printing
100 --
101 | PrettyPrintForAll [String] Type deriving (Show, Eq, Data, Typeable)
103-- |
104-- Convert a row to a list of pairs of labels and types
105--
106rowToList :: Type -> ([(String, Type)], Type)
107rowToList (RCons name ty row) = let (tys, rest) = rowToList row
108 in ((name, ty):tys, rest)
109rowToList r = ([], r)
111-- |
112-- Convert a list of labels and types to a row
113--
114rowFromList :: ([(String, Type)], Type) -> Type
115rowFromList ([], r) = r
116rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
118-- |
119-- Check whether a type is a monotype
120--
121isMonoType :: Type -> Bool
122isMonoType ForAll{} = False
123isMonoType _ = True
125-- |
126-- Universally quantify a type
127--
128mkForAll :: [String] -> Type -> Type
129mkForAll args ty = foldl (\t arg -> ForAll arg t Nothing) ty args
131-- |
132-- Replace a type variable, taking into account variable shadowing
133--
134replaceTypeVars :: String -> Type -> Type -> Type
135replaceTypeVars = replaceTypeVars' []
136 where
137 replaceTypeVars' bound name replacement = go bound
138 where
139 go :: [String] -> Type -> Type
140 go _ (TypeVar v) | v == name = replacement
141 go bs (TypeApp t1 t2) = TypeApp (go bs t1) (go bs t2)
142 go bs (SaturatedTypeSynonym name' ts) = SaturatedTypeSynonym name' $ map (go bs) ts
143 go bs f@(ForAll v t sco) | v == name = f
144 | v `elem` usedTypeVariables replacement =
145 let v' = genName v (name : bs ++ usedTypeVariables replacement)
146 t' = replaceTypeVars' bs v (TypeVar v') t
147 in ForAll v' (go (v' : bs) t') sco
148 | otherwise = ForAll v (go (v : bs) t) sco
149 go bs (ConstrainedType cs t) = ConstrainedType (map (second $ map (go bs)) cs) (go bs t)
150 go bs (RCons name' t r) = RCons name' (go bs t) (go bs r)
151 go bs (KindedType t k) = KindedType (go bs t) k
152 go _ ty = ty
153 genName orig inUse = try 0
154 where
155 try :: Integer -> String
156 try n | (orig ++ show n) `elem` inUse = try (n + 1)
157 | otherwise = orig ++ show n
159-- |
160-- Replace named type variables with types
161--
162replaceAllTypeVars :: [(String, Type)] -> Type -> Type
163replaceAllTypeVars = foldl (\f (name, ty) -> replaceTypeVars name ty . f) id
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 (SaturatedTypeSynonym _ ts) = concatMap (go bound) ts
184 go bound (ForAll v t _) = go (v : bound) t
185 go bound (ConstrainedType cs t) = concatMap (concatMap (go bound) . snd) cs ++ go bound t
186 go bound (RCons _ t r) = go bound t ++ go bound r
187 go bound (KindedType t _) = go bound t
188 go _ _ = []
190-- |
191-- Universally quantify over all type variables appearing free in a type
192--
193quantify :: Type -> Type
194quantify ty = foldr (\arg t -> ForAll arg t Nothing) ty $ freeTypeVariables ty
196-- |
197-- Move all universal quantifiers to the front of a type
198--
199moveQuantifiersToFront :: Type -> Type
200moveQuantifiersToFront = go [] []
201 where
202 go qs cs (ForAll q ty sco) = go ((q, sco) : qs) cs ty
203 go qs cs (ConstrainedType cs' ty) = go qs (cs ++ cs') ty
204 go qs cs ty =
205 let constrained = case cs of
206 [] -> ty
207 cs' -> ConstrainedType cs' ty
208 in case qs of
209 [] -> constrained
210 qs' -> foldl (\ty' (q, sco) -> ForAll q ty' sco) constrained qs'
212--
213-- Traversals
214--
216everywhereOnTypes :: (Type -> Type) -> Type -> Type
217everywhereOnTypes f = go
218 where
219 go (TypeApp t1 t2) = f (TypeApp (go t1) (go t2))
220 go (SaturatedTypeSynonym name tys) = f (SaturatedTypeSynonym name (map go tys))
221 go (ForAll arg ty sco) = f (ForAll arg (go ty) sco)
222 go (ConstrainedType cs ty) = f (ConstrainedType (map (fmap (map go)) cs) (go ty))
223 go (RCons name ty rest) = f (RCons name (go ty) (go rest))
224 go (KindedType ty k) = f (KindedType (go ty) k)
225 go (PrettyPrintFunction t1 t2) = f (PrettyPrintFunction (go t1) (go t2))
226 go (PrettyPrintArray t) = f (PrettyPrintArray (go t))
227 go (PrettyPrintObject t) = f (PrettyPrintObject (go t))
228 go (PrettyPrintForAll args t) = f (PrettyPrintForAll args (go t))
229 go other = f other
231everywhereOnTypesTopDown :: (Type -> Type) -> Type -> Type
232everywhereOnTypesTopDown f = go . f
233 where
234 go (TypeApp t1 t2) = TypeApp (go (f t1)) (go (f t2))
235 go (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name (map (go . f) tys)
236 go (ForAll arg ty sco) = ForAll arg (go (f ty)) sco
237 go (ConstrainedType cs ty) = ConstrainedType (map (fmap (map (go . f))) cs) (go (f ty))
238 go (RCons name ty rest) = RCons name (go (f ty)) (go (f rest))
239 go (KindedType ty k) = KindedType (go (f ty)) k
240 go (PrettyPrintFunction t1 t2) = PrettyPrintFunction (go (f t1)) (go (f t2))
241 go (PrettyPrintArray t) = PrettyPrintArray (go (f t))
242 go (PrettyPrintObject t) = PrettyPrintObject (go (f t))
243 go (PrettyPrintForAll args t) = PrettyPrintForAll args (go (f t))
244 go other = f other
246everywhereOnTypesM :: (Functor m, Applicative m, Monad m) => (Type -> m Type) -> Type -> m Type
247everywhereOnTypesM f = go
248 where
249 go (TypeApp t1 t2) = (TypeApp <$> go t1 <*> go t2) >>= f
250 go (SaturatedTypeSynonym name tys) = (SaturatedTypeSynonym name <$> mapM go tys) >>= f
251 go (ForAll arg ty sco) = (ForAll arg <$> go ty <*> pure sco) >>= f
252 go (ConstrainedType cs ty) = (ConstrainedType <$> mapM (sndM (mapM go)) cs <*> go ty) >>= f
253 go (RCons name ty rest) = (RCons name <$> go ty <*> go rest) >>= f
254 go (KindedType ty k) = (KindedType <$> go ty <*> pure k) >>= f
255 go (PrettyPrintFunction t1 t2) = (PrettyPrintFunction <$> go t1 <*> go t2) >>= f
256 go (PrettyPrintArray t) = (PrettyPrintArray <$> go t) >>= f
257 go (PrettyPrintObject t) = (PrettyPrintObject <$> go t) >>= f
258 go (PrettyPrintForAll args t) = (PrettyPrintForAll args <$> go t) >>= f
259 go other = f other
261everywhereOnTypesTopDownM :: (Functor m, Applicative m, Monad m) => (Type -> m Type) -> Type -> m Type
262everywhereOnTypesTopDownM f = go <=< f
263 where
264 go (TypeApp t1 t2) = TypeApp <$> (f t1 >>= go) <*> (f t2 >>= go)
265 go (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name <$> mapM (go <=< f) tys
266 go (ForAll arg ty sco) = ForAll arg <$> (f ty >>= go) <*> pure sco
267 go (ConstrainedType cs ty) = ConstrainedType <$> mapM (sndM (mapM (go <=< f))) cs <*> (f ty >>= go)
268 go (RCons name ty rest) = RCons name <$> (f ty >>= go) <*> (f rest >>= go)
269 go (KindedType ty k) = KindedType <$> (f ty >>= go) <*> pure k
270 go (PrettyPrintFunction t1 t2) = PrettyPrintFunction <$> (f t1 >>= go) <*> (f t2 >>= go)
271 go (PrettyPrintArray t) = PrettyPrintArray <$> (f t >>= go)
272 go (PrettyPrintObject t) = PrettyPrintObject <$> (f t >>= go)
273 go (PrettyPrintForAll args t) = PrettyPrintForAll args <$> (f t >>= go)
274 go other = f other
276everythingOnTypes :: (r -> r -> r) -> (Type -> r) -> Type -> r
277everythingOnTypes (<>) f = go
278 where
279 go t@(TypeApp t1 t2) = f t <> go t1 <> go t2
280 go t@(SaturatedTypeSynonym _ tys) = foldl (<>) (f t) (map go tys)
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@(PrettyPrintArray t1) = f t <> go t1
287 go t@(PrettyPrintObject t1) = f t <> go t1
288 go t@(PrettyPrintForAll _ t1) = f t <> go t1
289 go other = f other