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