git.iko.soy/rowtype-yoga/purescript-native
on 2ffe085 help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Kinds.hs
168 lines 6.3 kB history raw
1-----------------------------------------------------------------------------
2--
3-- Module : PureScript.TypeChecker.Kinds
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--
13-----------------------------------------------------------------------------
15module PureScript.TypeChecker.Kinds (
16 KindConstraint(..),
17 KindSolution(..),
18 kindsOf,
19 kindOf
20) where
22import Data.List
23import Data.Maybe (fromMaybe)
24import Data.Function
26import PureScript.Types
27import PureScript.Kinds
28import PureScript.Declarations
29import PureScript.TypeChecker.Monad
31import Control.Monad.State
32import Control.Monad.Error
34import Control.Applicative
35import Control.Arrow (Kleisli(..), (***))
36import qualified Control.Category as C
38import qualified Data.Map as M
40data KindConstraint = KindConstraint Int Kind
42instance Show KindConstraint where
43 show (KindConstraint n k) = show n ++ " = " ++ show k
45newtype KindSolution = KindSolution { runKindSolution :: Int -> Kind }
47emptyKindSolution :: KindSolution
48emptyKindSolution = KindSolution KUnknown
50kindOf :: PolyType -> Check Kind
51kindOf (PolyType idents ty) = do
52 ns <- replicateM (length idents) fresh
53 (cs, n, m) <- kindConstraints (M.fromList (zip idents ns)) ty
54 solution <- solveKindConstraints cs emptyKindSolution
55 return $ starIfUnknown $ runKindSolution solution n
57kindsOf :: Maybe String -> [String] -> [Type] -> Check Kind
58kindsOf name args ts = do
59 tyCon <- fresh
60 nargs <- replicateM (length args) fresh
61 (cs, ns, m) <- kindConstraintsAll (maybe id (flip M.insert tyCon) name $ M.fromList (zipWith (,) args nargs)) ts
62 let extraConstraints = KindConstraint tyCon (foldr FunKind Star (map KUnknown nargs)) : map (flip KindConstraint Star) ns
63 solution <- solveKindConstraints (extraConstraints ++ cs) emptyKindSolution
64 return $ starIfUnknown $ runKindSolution solution tyCon
66starIfUnknown :: Kind -> Kind
67starIfUnknown (KUnknown _) = Star
68starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
69starIfUnknown k = k
71kindConstraintsAll :: M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], M.Map String Int)
72kindConstraintsAll m [] = return ([], [], m)
73kindConstraintsAll m (t:ts) = do
74 (cs, n1, m') <- kindConstraints m t
75 (cs', ns, m'') <- kindConstraintsAll m' ts
76 return ((KindConstraint n1 Star) : cs ++ cs', n1:ns, m'')
78kindConstraints :: M.Map String Int -> Type -> Check ([KindConstraint], Int, M.Map String Int)
79kindConstraints m (Array t) = do
80 me <- fresh
81 (cs, n1, m') <- kindConstraints m t
82 return ((KindConstraint n1 Star) : (KindConstraint me Star) : cs, me, m')
83kindConstraints m (Object row) = do
84 me <- fresh
85 (cs, row, m') <- kindConstraintsForRow m row
86 return ((KindConstraint me Star) : (KindConstraint row Row) : cs, me, m')
87kindConstraints m (Function args ret) = do
88 me <- fresh
89 (cs, ns, m') <- kindConstraintsAll m args
90 (cs', retN, m'') <- kindConstraints m' ret
91 return ((KindConstraint retN Star) : (KindConstraint me Star) : (map (flip KindConstraint Star) ns) ++ cs, me, m'')
92kindConstraints m (TypeVar v) = do
93 case M.lookup v m of
94 Just u -> return ([], u, m)
95 Nothing -> throwError $ "Unbound type variable " ++ v
96kindConstraints m (TypeConstructor v) = do
97 env <- getEnv
98 me <- fresh
99 case M.lookup v m of
100 Nothing -> case M.lookup v (types env) of
101 Nothing -> throwError $ "Unknown type constructor '" ++ v ++ "'"
102 Just (kind, _) -> return ([KindConstraint me kind], me, m)
103 Just u -> do
104 return ([KindConstraint me (KUnknown u)], me, m)
105kindConstraints m (TypeApp t1 t2) = do
106 me <- fresh
107 (cs1, n1, m1) <- kindConstraints m t1
108 (cs2, n2, m2) <- kindConstraints m1 t2
109 return ((KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me))) : cs1 ++ cs2, me, m2)
110kindConstraints m _ = do
111 me <- fresh
112 return ([KindConstraint me Star], me, m)
114kindConstraintsForRow :: M.Map String Int -> Row -> Check ([KindConstraint], Int, M.Map String Int)
115kindConstraintsForRow m (RowVar v) = do
116 me <- case M.lookup v m of
117 Just u -> return u
118 Nothing -> fresh
119 return ([KindConstraint me Row], me, M.insert v me m)
120kindConstraintsForRow m REmpty = do
121 me <- fresh
122 return ([KindConstraint me Row], me, m)
123kindConstraintsForRow m (RCons _ ty row) = do
124 me <- fresh
125 (cs1, n1, m1) <- kindConstraints m ty
126 (cs2, n2, m2) <- kindConstraintsForRow m1 row
127 return ((KindConstraint me Row) : (KindConstraint n1 Star) : (KindConstraint n2 Row) : cs1 ++ cs2, me, m2)
129solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
130solveKindConstraints [] s = return s
131solveKindConstraints all@(KindConstraint n k:cs) s = do
132 guardWith "Occurs check failed" $ not $ kindOccursCheck False n k
133 let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
134 cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
135 solveKindConstraints cs' s'
137substituteKindConstraint :: Int -> Kind -> KindConstraint -> Check [KindConstraint]
138substituteKindConstraint n k (KindConstraint m l)
139 | n == m = unifyKinds k l
140 | otherwise = return [KindConstraint m (replaceUnknownKind n k l)]
142replaceUnknownKind :: Int -> Kind -> Kind -> Kind
143replaceUnknownKind n k = f
144 where
145 f (KUnknown m) | m == n = k
146 f (FunKind k1 k2) = FunKind (f k2) (f k2)
147 f other = other
149unifyKinds :: Kind -> Kind -> Check [KindConstraint]
150unifyKinds (KUnknown u1) (KUnknown u2) | u1 == u2 = return []
151unifyKinds (KUnknown u) k = do
152 guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
153 return [KindConstraint u k]
154unifyKinds k (KUnknown u) = do
155 guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
156 return [KindConstraint u k]
157unifyKinds Star Star = return []
158unifyKinds Row Row = return []
159unifyKinds (FunKind k1 k2) (FunKind k3 k4) = do
160 cs1 <- unifyKinds k1 k3
161 cs2 <- unifyKinds k2 k4
162 return $ cs1 ++ cs2
163unifyKinds k1 k2 = throwError $ "Cannot unify " ++ show k1 ++ " with " ++ show k2 ++ "."
165kindOccursCheck :: Bool -> Int -> Kind -> Bool
166kindOccursCheck b u (KUnknown u') | u == u' = b
167kindOccursCheck _ u (FunKind k1 k2) = kindOccursCheck True u k1 || kindOccursCheck True u k2
168kindOccursCheck _ _ _ = False