git.iko.soy/rowtype-yoga/purescript-native
on a10616f help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Kinds.hs
150 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 let tyCon = 0
51 let nargs = [1..length args]
52 (cs, ns, _, m) <- kindConstraintsAll (length args + 1) (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 0
57starIfUnknown :: Kind -> Kind
58starIfUnknown (KUnknown _) = Star
59starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
60starIfUnknown k = k
62kindConstraintsAll :: Int -> M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], Int, M.Map String Int)
63kindConstraintsAll n m [] = return ([], [], n, m)
64kindConstraintsAll n m (t:ts) = do
65 (cs, n1, max1, m') <- kindConstraints n m t
66 (cs', ns, max2, m'') <- kindConstraintsAll (max1 + 1) m' ts
67 return ((KindConstraint n1 Star) : cs ++ cs', n1:ns, max2, m'')
69kindConstraints :: Int -> M.Map String Int -> Type -> Check ([KindConstraint], Int, Int, M.Map String Int)
70kindConstraints n m (Array t) = do
71 let me = n
72 (cs, n1, max1, m') <- kindConstraints (n + 1) m t
73 return ((KindConstraint n1 Star) : (KindConstraint me Star) : cs, me, max1, m')
74kindConstraints n m (Object row) = do
75 let me = n
76 (cs, row, max1, m') <- kindConstraintsForRow (n + 1) m row
77 return ((KindConstraint me Star) : (KindConstraint row Row) : cs, me, max1, m')
78kindConstraints n m (Function args ret) = do
79 let me = n
80 (cs, ns, max1, m') <- kindConstraintsAll (n + 1) m args
81 (cs', retN, max2, m'') <- kindConstraints (max1 + 1) m' ret
82 return ((KindConstraint retN Star) : (KindConstraint me Star) : (map (flip KindConstraint Star) ns) ++ cs, me, max2, m'')
83kindConstraints n m (TypeVar v) =
84 let n' = maybe n id (M.lookup v m)
85 in return ([], n', n, M.insert v n' m)
86kindConstraints n m (TypeConstructor v) = do
87 env <- get
88 kind <- case M.lookup v m of
89 Nothing -> case M.lookup v (types env) of
90 Nothing -> throwError $ "Unknown type constructor '" ++ v ++ "'"
91 Just k -> return k
92 Just u -> return (KUnknown u)
93 return ([KindConstraint n kind], n, n, m)
94kindConstraints n m (TypeApp t1 t2) = do
95 let me = n
96 (cs1, n1, max1, m1) <- kindConstraints (n + 1) m t1
97 (cs2, n2, max2, m2) <- kindConstraints (max1 + 1) m1 t2
98 return ((KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me))) : cs1 ++ cs2, me, max2, m2)
99kindConstraints n m _ = return ([KindConstraint n Star], n, n, m)
101kindConstraintsForRow :: Int -> M.Map String Int -> Row -> Check ([KindConstraint], Int, Int, M.Map String Int)
102kindConstraintsForRow n m (RowVar v) =
103 let n' = maybe n id (M.lookup v m)
104 in return ([KindConstraint n' Row], n', n, M.insert v n' m)
105kindConstraintsForRow n m REmpty = return ([KindConstraint n Row], n, n, m)
106kindConstraintsForRow n m (RCons _ ty row) = do
107 (cs1, n1, max1, m1) <- kindConstraints (n + 1) m ty
108 (cs2, n2, max2, m2) <- kindConstraintsForRow (max1 + 1) m1 row
109 return ((KindConstraint n Row) : (KindConstraint n1 Star) : (KindConstraint n2 Row) : cs1 ++ cs2, n, max2, m2)
111solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
112solveKindConstraints [] s = return s
113solveKindConstraints all@(KindConstraint n k:cs) s = do
114 guardWith "Occurs check failed" $ not $ kindOccursCheck n k
115 let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
116 cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
117 solveKindConstraints cs' s'
119substituteKindConstraint :: Int -> Kind -> KindConstraint -> Check [KindConstraint]
120substituteKindConstraint n k (KindConstraint m l)
121 | n == m = unifyKinds k l
122 | otherwise = return [KindConstraint m (replaceUnknownKind n k l)]
124replaceUnknownKind :: Int -> Kind -> Kind -> Kind
125replaceUnknownKind n k = f
126 where
127 f (KUnknown m) | m == n = k
128 f (FunKind k1 k2) = FunKind (f k2) (f k2)
129 f other = other
131unifyKinds :: Kind -> Kind -> Check [KindConstraint]
132unifyKinds (KUnknown u1) (KUnknown u2) | u1 == u2 = return []
133unifyKinds (KUnknown u) k = do
134 guardWith "Occurs check failed" $ not $ kindOccursCheck u k
135 return [KindConstraint u k]
136unifyKinds k (KUnknown u) = do
137 guardWith "Occurs check failed" $ not $ kindOccursCheck u k
138 return [KindConstraint u k]
139unifyKinds Star Star = return []
140unifyKinds Row Row = return []
141unifyKinds (FunKind k1 k2) (FunKind k3 k4) = do
142 cs1 <- unifyKinds k1 k3
143 cs2 <- unifyKinds k2 k4
144 return $ cs1 ++ cs2
145unifyKinds k1 k2 = throwError $ "Cannot unify " ++ show k1 ++ " with " ++ show k2 ++ "."
147kindOccursCheck :: Int -> Kind -> Bool
148kindOccursCheck u (KUnknown u') | u == u' = True
149kindOccursCheck u (FunKind k1 k2) = kindOccursCheck u k1 || kindOccursCheck u k2
150kindOccursCheck _ _ = False