git.iko.soy/rowtype-yoga/purescript-native
on 100d787 help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Kinds.hs
131 lines 4.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 deriving Show
40newtype KindSolution = KindSolution { runKindSolution :: Int -> Kind }
42emptyKindSolution :: KindSolution
43emptyKindSolution = KindSolution KUnknown
45kindsOf :: [String] -> [Type] -> Check [Kind]
46kindsOf args ts = do
47 (cs, _, m) <- kindConstraintsAll 0 M.empty ts
48 solution <- solveKindConstraints cs emptyKindSolution
49 return $ map (maybe Star starIfUnknown . fmap (runKindSolution solution) . flip M.lookup m) args
51starIfUnknown :: Kind -> Kind
52starIfUnknown (KUnknown _) = Star
53starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
54starIfUnknown k = k
56kindConstraintsAll :: Int -> M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], M.Map String Int)
57kindConstraintsAll _ m [] = return ([], [], m)
58kindConstraintsAll n m (t:ts) = do
59 (cs, n', m') <- kindConstraints n m t
60 (cs', ns, m'') <- kindConstraintsAll (n' + 1) m' ts
61 return ((KindConstraint n' Star) : cs ++ cs', n':ns, m'')
63kindConstraints :: Int -> M.Map String Int -> Type -> Check ([KindConstraint], Int, M.Map String Int)
64kindConstraints n m (Array t) = do
65 (cs, n', m') <- kindConstraints n m t
66 return ((KindConstraint n' Star) : (KindConstraint (n' + 1) Star) : cs, n' + 1, m')
67kindConstraints n m (Object row) = do
68 let me = n
69 (cs, row, m') <- kindConstraintsForRow (n + 2) m row
70 return ((KindConstraint me Star) : (KindConstraint row Row) : cs, me, m')
71kindConstraints n m (Function args ret) = do
72 (cs, ns, m') <- kindConstraintsAll n m args
73 let next = maximum ns + 1
74 (cs', retN, m'') <- kindConstraints next m' ret
75 let me = retN + 1
76 return ((KindConstraint retN Star) : (KindConstraint me Star) : (map (flip KindConstraint Star) ns) ++ cs, me, m'')
77kindConstraints n m (TypeVar v) =
78 let
79 n' = maybe n id (M.lookup v m)
80 in return ([], n', M.insert v n' m)
81kindConstraints n m (TypeConstructor v) = do
82 env <- get
83 kind <- maybe (throwError "Unknown type constructor") return (M.lookup v (types env))
84 return ([KindConstraint n kind], n, m)
85kindConstraints n m (TypeApp t1 t2) = do
86 (cs1, n1, m1) <- kindConstraints n m t1
87 (cs2, n2, m2) <- kindConstraints (n1 + 1) m1 t2
88 return ((KindConstraint n1 (FunKind (KUnknown n2) (KUnknown (n2 + 1)))) : cs1 ++ cs2, n2 + 1, m2)
89kindConstraints n m _ = return ([KindConstraint n Star], n, m)
91kindConstraintsForRow :: Int -> M.Map String Int -> Row -> Check ([KindConstraint], Int, M.Map String Int)
92kindConstraintsForRow = undefined
94solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
95solveKindConstraints [] s = return s
96solveKindConstraints (KindConstraint n k:cs) s = do
97 guardWith "Occurs check failed" $ not $ kindOccursCheck n k
98 let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
99 cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
100 solveKindConstraints cs' s'
102substituteKindConstraint :: Int -> Kind -> KindConstraint -> Check [KindConstraint]
103substituteKindConstraint n k (KindConstraint m l)
104 | n == m = unifyKinds k l
105 | otherwise = return [KindConstraint m (replaceUnknownKind n k l)]
107replaceUnknownKind :: Int -> Kind -> Kind -> Kind
108replaceUnknownKind n k = f
109 where
110 f (KUnknown m) | m == n = k
111 f (FunKind k1 k2) = FunKind (f k2) (f k2)
112 f other = other
114unifyKinds :: Kind -> Kind -> Check [KindConstraint]
115unifyKinds (KUnknown u) k = do
116 guardWith "Occurs check failed" $ not $ kindOccursCheck u k
117 return [KindConstraint u k]
118unifyKinds k (KUnknown u) = do
119 guardWith "Occurs check failed" $ not $ kindOccursCheck u k
120 return [KindConstraint u k]
121unifyKinds Star Star = return []
122unifyKinds (FunKind k1 k2) (FunKind k3 k4) = do
123 cs1 <- unifyKinds k1 k3
124 cs2 <- unifyKinds k2 k4
125 return $ cs1 ++ cs2
126unifyKinds k1 k2 = throwError $ "Cannot unify " ++ show k1 ++ " with " ++ show k2 ++ "."
128kindOccursCheck :: Int -> Kind -> Bool
129kindOccursCheck u (KUnknown u') | u == u' = True
130kindOccursCheck u (FunKind k1 k2) = kindOccursCheck u k1 || kindOccursCheck u k2
131kindOccursCheck _ _ = False