git.iko.soy/tix
on master help sign in
Seems to typecheck almost fine
4f4657eiko
src/Data/Range.hsnew file+41
compare with master
unifiedsplit
@@ -0,0 +1,41 @@
1+module Data.Range
2+ ( Range (Range, InfiniteRange, EmptyRange),
3+ member,
4+ notMember,
5+ )
6+where
7+
8+-- | Includes both ends included
9+data Range a
10+ = Range' !a !a
11+ | InfiniteRange
12+ | EmptyRange
13+
14+member :: Ord a => a -> Range a -> Bool
15+member _ InfiniteRange = True
16+member _ EmptyRange = False
17+member a (Range' l r) = a >= l && a <= r
18+{-# INLINE member #-}
19+
20+notMember :: Ord a => a -> Range a -> Bool
21+notMember a r = not $ member a r
22+{-# INLINE notMember #-}
23+
24+pattern Range :: Ord a => a -> a -> Range a
25+pattern Range x y <- Range' x y where Range x y = Range' (min x y) (max x y)
26+
27+-- pattern EmptyRange :: Range a
28+-- pattern EmptyRange = Range' []
29+
30+-- pattern Range :: Ord a => a -> a -> Range a -> Range a
31+-- pattern Range l r rest <-
32+-- ( ( \x -> case x of
33+-- Range' ((a, b) : rest) -> Just (a, b, Range' rest)
34+-- _ -> Nothing
35+-- ) ->
36+-- Just (l, r, rest)
37+-- )
38+
39+-- addToRange :: Ord a => a -> a -> Range a -> Range a
40+-- addToRange _ _ InfiniteRange = InfiniteRange
41+-- addToRange l r (Range' rs) =
src/Tix/Typechecker.hs+125−46
@@ -24,6 +24,8 @@ import qualified Data.List.NonEmpty as NE
24import Data.Map.Strict (Map)
24import Data.Map.Strict (Map)
25import qualified Data.Map.Strict as M
25import qualified Data.Map.Strict as M
26import Data.MonoTraversable
26import Data.MonoTraversable
27+import Data.Range (Range (..))
28+import qualified Data.Range as R
27import Data.Sequence (Seq (..))
29import Data.Sequence (Seq (..))
28import Data.Sequences
30import Data.Sequences
29import Data.Set (Set)
31import Data.Set (Set)
@@ -61,11 +63,11 @@ getType' ::
61 NExprLoc ->
63 NExprLoc ->
62 Eff r NType
64 Eff r NType
63getType' r = do
65getType' r = do
64− (t, constraints) <-
66+ ((t, s'), constraints) <-
65− runSeqWriter @(Seq Constraint) $
67+ runSeqWriter @(Seq Constraint) . runWriter @Substitution $
66− infer r
68+ inferGeneral r
67− s <- solve (traceShowId constraints)
69+ s <- solve (traceShowId . fmap (subCon s') $ constraints)
68− return . close $ sub s (traceShowId t)
70+ return . close InfiniteRange $ sub (s <> s') (traceShowId t)
69
71
70newtype TypeVariable = TypeVariable Int
72newtype TypeVariable = TypeVariable Int
71 deriving newtype (Show, Eq, Ord)
73 deriving newtype (Show, Eq, Ord)
@@ -85,23 +87,34 @@ variableNames =
85 <> (fmap (\(n, g) -> g <> T.fromString (show n)) $ zip [1 :: Int ..] greek)
87 <> (fmap (\(n, g) -> g <> T.fromString (show n)) $ zip [1 :: Int ..] greek)
86
88
87showNType :: NType -> Text
89showNType :: NType -> Text
88−showNType t = TL.toStrict . T.toLazyText $ showNType' t
90+showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
89 where
91 where
90− greekVars = M.fromList $ zip (S.toList $ getDeBurjins t) variableNames
92+ greekVars = M.fromList . traceShowId $ zip (S.toList $ getAllDeBurjins t) variableNames
91− showNType' :: NType -> T.Builder
93+ showNType' :: Int -> NType -> T.Builder
94+ showNType' depth u =
95+ foralls <> case u of
92− showNType' (NAtomic a) = showAtomicType a
96+ (NAtomic a) -> showAtomicType a
93− showNType' (NBrujin b) = greekVars M.! b
97+ (NBrujin (DeBrujin i j)) -> greekVars M.! (DeBrujin (i - depth) j)
94− showNType' (NTypeVariable _) = error "should not have free type variables at this point"
98+ (NTypeVariable _) -> error "should not have free type variables at this point"
95− showNType' (x :-> y) = showNType' x <> " -> " <> showNType' y
99+ (x :-> y) -> showNType' (depth + 1) x <> " -> " <> showNType' (depth + 1) y
96− showNType' (List x) = "[" <> showNType' x <> "]"
100+ (List x) -> "[" <> showNType' (depth + 1) x <> "]"
97− showNType' (NAttrSet x) =
101+ (NAttrSet x) ->
98− "AttrSet {"
102+ "{ "
99− <> ( mconcat
103+ <> ( mconcat
100− . intersperse "; "
104+ . intersperse "; "
101− . fmap (\(k, v) -> T.fromText k <> " :: " <> showNType' v)
105+ . fmap (\(k, v) -> T.fromText k <> " = " <> showNType' (depth + 1) v)
102− $ M.toList x
106+ $ M.toList x
103− )
107+ )
104− <> "}"
108+ <> " }"
109+ where
110+ currBurjins = traceShowId . S.mapMonotonic (DeBrujin (- depth)) $ getDeBurjins 0 (traceShowId u)
111+ foralls =
112+ if S.null currBurjins
113+ then ""
114+ else
115+ "∀ "
116+ <> (mconcat . intersperse " " . M.elems $ M.restrictKeys greekVars currBurjins)
117+ <> ". "
105
118
106showAtomicType :: AtomicType -> T.Builder
119showAtomicType :: AtomicType -> T.Builder
107showAtomicType Integer = "Integer"
120showAtomicType Integer = "Integer"
@@ -116,9 +129,9 @@ data NType
116 = NTypeVariable !TypeVariable
129 = NTypeVariable !TypeVariable
117 | NBrujin !DeBrujin
130 | NBrujin !DeBrujin
118 | NAtomic !AtomicType
131 | NAtomic !AtomicType
119− | !NType :-> !NType
120 | -- These two introduce a new De Brujin binding context
132 | -- These two introduce a new De Brujin binding context
133+ !NType :-> !NType
121− List !NType
134+ | List !NType
122 | NAttrSet !(Map Text NType)
135 | NAttrSet !(Map Text NType)
123 deriving stock (Eq, Ord, Show)
136 deriving stock (Eq, Ord, Show)
124
137
@@ -132,13 +145,26 @@ data AtomicType
132 | URI
145 | URI
133 deriving stock (Eq, Ord, Show)
146 deriving stock (Eq, Ord, Show)
134
147
135−getDeBurjins :: NType -> Set DeBrujin
148+getDeBurjins :: Int -> NType -> Set Int
136−getDeBurjins (NTypeVariable _) = S.empty
149+getDeBurjins _ (NTypeVariable _) = S.empty
150+getDeBurjins _ (NAtomic _) = S.empty
137−getDeBurjins (NBrujin x) = S.singleton x
151+getDeBurjins n (NBrujin (DeBrujin m j)) | m == n = S.singleton j
138−getDeBurjins (NAtomic _) = S.empty
152+getDeBurjins _ (NBrujin _) = S.empty
139−getDeBurjins (x :-> y) = getDeBurjins x <> getDeBurjins y
153+getDeBurjins n (x :-> y) = getDeBurjins (n + 1) x <> getDeBurjins (n + 1) y
140−getDeBurjins (List x) = getDeBurjins x
154+getDeBurjins n (List x) = getDeBurjins (n + 1) x
141−getDeBurjins (NAttrSet xs) = foldMap getDeBurjins . M.elems $ xs
155+getDeBurjins n (NAttrSet xs) = foldMap (getDeBurjins (n + 1)) . M.elems $ xs
156+
157+getAllDeBurjins :: NType -> Set DeBrujin
158+getAllDeBurjins =
159+ traceShowId . \case
160+ (NTypeVariable _) -> S.empty
161+ (NAtomic _) -> S.empty
162+ (NBrujin x) -> S.singleton x
163+ (x :-> y) -> bncCtx $ getAllDeBurjins x <> getAllDeBurjins y
164+ (List x) -> bncCtx $ getAllDeBurjins x
165+ (NAttrSet xs) -> bncCtx . foldMap getAllDeBurjins . M.elems $ xs
166+ where
167+ bncCtx = S.mapMonotonic (\(DeBrujin i j) -> DeBrujin (i - 1) j)
142
168
143isClosed :: NType -> Bool
169isClosed :: NType -> Bool
144isClosed (NTypeVariable _) = False
170isClosed (NTypeVariable _) = False
@@ -148,8 +174,8 @@ isClosed (x :-> y) = isClosed x && isClosed y
148isClosed (List x) = isClosed x
174isClosed (List x) = isClosed x
149isClosed (NAttrSet xs) = all isClosed . M.elems $ xs
175isClosed (NAttrSet xs) = all isClosed . M.elems $ xs
150
176
151−close :: NType -> NType
177+close :: Range TypeVariable -> NType -> NType
152−close =
178+close range =
153 run
179 run
154 . evalState @(Map TypeVariable DeBrujin) M.empty
180 . evalState @(Map TypeVariable DeBrujin) M.empty
155 . runReader @Int 0
181 . runReader @Int 0
@@ -160,12 +186,16 @@ close =
160 close' :: NType -> Eff '[State Int, Reader Int, State (Map TypeVariable DeBrujin)] NType
186 close' :: NType -> Eff '[State Int, Reader Int, State (Map TypeVariable DeBrujin)] NType
161 close' x@(NAtomic _) = return x
187 close' x@(NAtomic _) = return x
162 close' x@(NBrujin _) = return x
188 close' x@(NBrujin _) = return x
163− close' (x :-> y) = (:->) <$> close' x <*> close' y
164− close' (NTypeVariable tv) = NBrujin <$> newbrujin tv
189+ close' (NTypeVariable tv) | tv `R.member` range = NBrujin <$> newbrujin tv
190+ close' (x :-> y) = bndCtx $ (:->) <$> close' x <*> close' y
165 close' (List x) = bndCtx $ List <$> close' x
191 close' (List x) = bndCtx $ List <$> close' x
166 close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x
192 close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x
167
193
194+ bndCtx m = do
195+ modify @(Map TypeVariable DeBrujin) (fmap (\(DeBrujin i j) -> DeBrujin (i + 1) j))
168− bndCtx = local @Int (+ 1)
196+ x <- local @Int (+ 1) m
197+ modify @(Map TypeVariable DeBrujin) (fmap (\(DeBrujin i j) -> DeBrujin (i - 1) j))
198+ return x
169 newbrujin t = do
199 newbrujin t = do
170 get @(Map TypeVariable DeBrujin) <&> M.lookup t >>= \case
200 get @(Map TypeVariable DeBrujin) <&> M.lookup t >>= \case
171 Nothing -> do
201 Nothing -> do
@@ -188,6 +218,7 @@ instance Free NType where
188 free (x :-> y) = free x <> free y
218 free (x :-> y) = free x <> free y
189
219
190newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
220newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
221+ deriving newtype (Eq, Ord, Show)
191
222
192instance Semigroup Substitution where
223instance Semigroup Substitution where
193 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)
224 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)
@@ -218,9 +249,21 @@ v <<- x | v `occursIn` x = tell (InfinityType x) >> return mempty
218v <<- x = return $ Substitution $ M.singleton v x
249v <<- x = return $ Substitution $ M.singleton v x
219
250
220unify :: Constraint -> UnifyM Substitution
251unify :: Constraint -> UnifyM Substitution
221−unify (lhs :~ rhs) =
252+unify = unifyWithPriority EmptyRange
253+
254+unifyWithPriority ::
255+ -- | The range of type variables to interpret as being lower
256+ -- priority (try to replace them if possible)
257+ Range TypeVariable ->
258+ Constraint ->
259+ UnifyM Substitution
260+unifyWithPriority range (lhs :~ rhs) =
222 case (lhs, rhs) of
261 case (lhs, rhs) of
223 (NAtomic x, NAtomic y) | x == y -> return mempty
262 (NAtomic x, NAtomic y) | x == y -> return mempty
263+ (NTypeVariable x, NTypeVariable y) ->
264+ if y `R.member` range
265+ then x <<- NTypeVariable y
266+ else y <<- NTypeVariable x
224 (NTypeVariable t, x) -> t <<- x
267 (NTypeVariable t, x) -> t <<- x
225 (x, NTypeVariable t) -> t <<- x
268 (x, NTypeVariable t) -> t <<- x
226 (List x, List y) -> unify $ x :~ y
269 (List x, List y) -> unify $ x :~ y
@@ -235,10 +278,18 @@ unify (lhs :~ rhs) =
235 (x, y) -> tell (CanNotUnify x y) >> return mempty
278 (x, y) -> tell (CanNotUnify x y) >> return mempty
236
279
237solve :: Seq Constraint -> UnifyM Substitution
280solve :: Seq Constraint -> UnifyM Substitution
281+solve = solveWithPriority EmptyRange
282+
283+solveWithPriority ::
284+ -- | The range of type variables to interpret as being lower
285+ -- priority (try to replace them if possible)
286+ Range TypeVariable ->
287+ Seq Constraint ->
288+ UnifyM Substitution
238−solve Empty = return mempty
289+solveWithPriority _ Empty = return mempty
239−solve (rest :|> c) = do
290+solveWithPriority range (rest :|> c) = do
240− s <- unify c
291+ s <- unifyWithPriority range c
241− (<> s) <$> solve (fmap (subCon (traceShowId s)) rest)
292+ (<> s) <$> solveWithPriority range (fmap (subCon (traceShowId s)) rest)
242
293
243pattern Sempty <- (S.null -> True) where Sempty = S.empty
294pattern Sempty <- (S.null -> True) where Sempty = S.empty
244
295
@@ -265,6 +316,10 @@ data Errors
265
316
266data Fresh x where
317data Fresh x where
267 Fresh :: Fresh TypeVariable
318 Fresh :: Fresh TypeVariable
319+ -- | Inclusive
320+ MinFreshFromNow :: Fresh TypeVariable
321+ -- | Inclusive
322+ MaxFreshUntilNow :: Fresh TypeVariable
268
323
269data ResumableExceptions x
324data ResumableExceptions x
270
325
@@ -274,12 +329,24 @@ runFresh :: Runner Fresh
274runFresh =
329runFresh =
275 evalState (TypeVariable 0)
330 evalState (TypeVariable 0)
276 . reinterpret
331 . reinterpret
332+ ( \case
277− ( \Fresh -> do
333+ Fresh -> do
278− (TypeVariable old) <- get
334+ (TypeVariable x) <- get
279− put (TypeVariable $ old + 1)
335+ put (TypeVariable $ x + 1)
336+ return (TypeVariable x)
337+ MinFreshFromNow -> get
338+ MaxFreshUntilNow -> do
339+ (TypeVariable new) <- get
280− return (TypeVariable old)
340+ return $ TypeVariable (new - 1)
281 )
341 )
282
342
343+registerTypeVariables :: Member Fresh r => Eff r a -> Eff r (a, Range TypeVariable)
344+registerTypeVariables m = do
345+ l <- send MinFreshFromNow
346+ a <- m
347+ r <- send MaxFreshUntilNow
348+ return (a, Range l r)
349+
283freshSrc ::
350freshSrc ::
284 Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan)] r =>
351 Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan)] r =>
285 Eff r TypeVariable
352 Eff r TypeVariable
@@ -302,7 +369,8 @@ type InferEffs =
302 Writer Constraint,
369 Writer Constraint,
303 Writer (SrcSpan, Errors),
370 Writer (SrcSpan, Errors),
304 Reader VariableMap,
371 Reader VariableMap,
305− Writer UnifyingError
372+ Writer UnifyingError,
373+ Writer Substitution
306 ]
374 ]
307
375
308type InferM x = forall r. Members InferEffs r => Eff r x
376type InferM x = forall r. Members InferEffs r => Eff r x
@@ -475,7 +543,7 @@ inferBinding bindings = do
475 getPath path >>= \case
543 getPath path >>= \case
476 Nothing -> return []
544 Nothing -> return []
477 Just name -> do
545 Just name -> do
478− t <- infer r
546+ t <- inferGeneral r
479 return $ [stack ((,) <$> name) (NAttrSet . uncurry M.singleton) t]
547 return $ [stack ((,) <$> name) (NAttrSet . uncurry M.singleton) t]
480 Inherit attrSet keys src -> do
548 Inherit attrSet keys src -> do
481 vars <- case attrSet of
549 vars <- case attrSet of
@@ -491,6 +559,17 @@ inferBinding bindings = do
491 Just r -> Just (name, r)
559 Just r -> Just (name, r)
492 return $ M.fromListWith mergeSetTypes bindings'
560 return $ M.fromListWith mergeSetTypes bindings'
493
561
562+inferGeneral :: NExprLoc -> InferM NType
563+inferGeneral x = do
564+ ((t, cs), range) <- registerTypeVariables . runSeqWriter @(Seq Constraint) $ infer x
565+ s <- solveWithPriority range cs
566+ -- Filter for optimization purposes
567+ tell . Substitution . M.filterWithKey (\k _ -> k `R.notMember` range) . unSubstitution $ s
568+ return . close range $ sub s t
569+
570+-- appAll :: (a -> b -> b) -> [a] -> b -> b
571+-- appAll f xs = appEndo (mconcat $ Endo . f <$> xs)
572+
494expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NType -> Eff r VariableMap
573expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NType -> Eff r VariableMap
495expectAttrSet (NAttrSet x) = return x
574expectAttrSet (NAttrSet x) = return x
496expectAttrSet g = do
575expectAttrSet g = do