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