on master help sign in
Simplified fresh variables
commitd40c07302a3f2fe520628782e8aa48b5ecd7d976 authoriko <ilyakooo0@gmail.com> dateThu 15 Apr 2021, 16:55 (6 years ago) parent62abc7b
2 files changed+50−48
src/Control/Monad/Freer/Fresh.hs+4 src/Tix/Typechecker.hs+46−48
src/Control/Monad/Freer/Fresh.hs+4
@@ -1,5 +1,6 @@
11module Control.Monad.Freer.Fresh
22 ( Fresh (..),
3+ fresh,
34 runFresh,
45 registerTypeVariables,
56 )
@@ -15,6 +16,9 @@ data Fresh x where
1516 -- | Inclusive
1617 MinFreshFromNow :: Fresh TypeVariable
1718
19+fresh :: Member Fresh eff => Eff eff TypeVariable
20+fresh = send Fresh
21+
1822type Runner effect = forall effs a. Eff (effect ': effs) a -> Eff effs a
1923
2024runFresh :: Runner Fresh
src/Tix/Typechecker.hs+46−48
@@ -58,6 +58,7 @@ getType :: NExprLoc -> (Scheme, [(SrcSpan, Errors)], [InferError], [UnifyingErro
5858getType r =
5959 let ((((((((t, traceTree), inf), predicate), unifying), errs), _srcs), subs), _) =
6060 run
61+ . runReader nullSpan
6162 . evalState @(MKM.Map Pred) mempty
6263 . interpret @(Writer Pred) (\(Tell x) -> modify (<> MKM.singleton x))
6364 . evalState (M.empty :: VariableMap)
@@ -68,7 +69,7 @@ getType r =
6869 . runSeqWriter @[UnifyingError]
6970 . runSeqWriter @[PredicateError]
7071 . runSeqWriter @[InferError]
71− . runFresh
72+ . runFreshSrc
7273 . runTreeTracer
7374 $ inferGeneral r
7475 in (sub subs t, errs, inf, unifying, predicate, traceTree)
@@ -97,6 +98,21 @@ runConstraintEnv f = do
9798 $ f
9899 return ((x, subs), sub subs <$> cs)
99100
101+runFreshSrc ::
102+ Members '[Reader SrcSpan, Writer (TypeVariable, SrcSpan)] eff =>
103+ Eff (Fresh : eff) ~> Eff eff
104+runFreshSrc =
105+ runFresh
106+ . interpose @Fresh
107+ ( \case
108+ Fresh -> do
109+ v <- send Fresh
110+ src <- ask @SrcSpan
111+ tell (v, src)
112+ return v
113+ MinFreshFromNow -> send MinFreshFromNow
114+ )
115+
100116captureSubstitutions ::
101117 Members '[SubstituteEnv] effs =>
102118 Eff (Writer Substitution : effs) a ->
@@ -268,15 +284,6 @@ data Errors
268284 | UnexpectedType {expected :: Scheme, got :: Scheme}
269285 deriving stock (Eq, Ord, Show)
270286
271−freshSrc ::
272− Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan)] r =>
273− Eff r TypeVariable
274−freshSrc = do
275− v <- send Fresh
276− src <- ask @SrcSpan
277− tell (v, src)
278− return v
279−
280287data UnifyingError
281288 = InfinityType NType
282289 | CanNotUnify NType NType
@@ -297,7 +304,7 @@ type UnifyM x = forall r. Members '[Writer UnifyingError] r => Eff r x
297304
298305type InferEffs =
299306 '[ Fresh,
300− Writer (TypeVariable, SrcSpan),
307+ Reader SrcSpan,
301308 Writer Constraint,
302309 Writer (SrcSpan, Errors),
303310 Writer PredicateError,
@@ -312,8 +319,6 @@ type InferEffs =
312319
313320type InferM x = forall r. Members InferEffs r => Eff r x
314321
315−type InferM' x = forall r. Members (Reader SrcSpan ': InferEffs) r => Eff r x
316−
317322runSeqWriter :: forall s w r a. (IsSequence s, Element s ~ w) => Eff (Writer w ': r) a -> Eff r (a, s)
318323runSeqWriter = handleRelayS mempty (\s x -> return (x, s)) $ \s (Tell w) k -> k (cons w s) ()
319324
@@ -322,19 +327,18 @@ throwSrc e = do
322327 src <- ask @SrcSpan
323328 tell (src, e)
324329
325−throwSrcTV ::
330+throwTV ::
326331 Members
327332 '[ Reader SrcSpan,
328333 Writer (SrcSpan, e),
329− Writer (TypeVariable, SrcSpan),
330334 Fresh
331335 ]
332336 r =>
333337 e ->
334338 Eff r TypeVariable
335−throwSrcTV e = do
339+throwTV e = do
336340 throwSrc e
337− freshSrc
341+ fresh
338342
339343type VariableMap = Map VarName Scheme
340344
@@ -355,7 +359,7 @@ withBindings bindings m = do
355359
356360instantiate ::
357361 forall effs.
358− Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan), Writer Pred] effs =>
362+ Members '[Fresh, Writer Pred] effs =>
359363 Scheme ->
360364 Eff effs NType
361365instantiate s = do
@@ -377,12 +381,12 @@ instantiate s = do
377381 gets (M.lookup db) >>= \case
378382 Just t -> return t
379383 Nothing -> do
380− t <- freshSrc
384+ t <- fresh
381385 modify (M.insert db t)
382386 return t
383387
384388infer :: NExprLoc -> InferM NType
385−infer (Fix (Compose (Ann src x))) = runReader src $ case x of
389+infer (Fix (Compose (Ann src x))) = local (const src) $ case x of
386390 NConstant a -> return . NAtomic $ case a of
387391 NURI {} -> URI
388392 NInt {} -> Integer
@@ -394,13 +398,13 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
394398 NStr {} -> return $ NAtomic String
395399 NSym var ->
396400 get @VariableMap
397− >>= maybe (scheme . NTypeVariable <$> throwSrcTV (UndefinedVariable var)) return . M.lookup var
401+ >>= maybe (scheme . NTypeVariable <$> throwTV (UndefinedVariable var)) return . M.lookup var
398402 >>= instantiate -- I have no idea if this covers all cases.
399403 NList xs -> do
400404 xs' <- traverse infer xs
401405 traverse_ tell . fmap (uncurry (:~)) $ zip xs' (tail xs')
402406 case xs' of
403− [] -> NTypeVariable <$> freshSrc
407+ [] -> NTypeVariable <$> fresh
404408 y : _ -> return $ List y
405409 NUnary NNeg y -> do
406410 t <- infer y
@@ -414,19 +418,19 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
414418 NBinary NUpdate lhs rhs -> do
415419 lhsT <- infer lhs
416420 rhsT <- infer rhs
417− res <- NTypeVariable <$> freshSrc
421+ res <- NTypeVariable <$> fresh
418422 tell (lhsT // rhsT $ res)
419423 return res
420424 NBinary NApp lhs rhs -> do
421425 lhst <- infer lhs
422426 rhst <- infer rhs
423− rest <- NTypeVariable <$> freshSrc
427+ rest <- NTypeVariable <$> fresh
424428 lhst ~~ (rhst :-> rest)
425429 return rest
426430 NBinary NConcat lhs rhs -> do
427431 lhst <- infer lhs
428432 rhst <- infer rhs
429− t <- NTypeVariable <$> freshSrc
433+ t <- NTypeVariable <$> fresh
430434 let listt = List t
431435 lhst ~~ listt
432436 rhst ~~ listt
@@ -453,7 +457,7 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
453457 (set', var) <- lookupAttrSet p
454458 setT ~~ set'
455459 return var
456− Nothing -> freshSrc
460+ Nothing -> fresh
457461 case def of
458462 Nothing -> return ()
459463 Just defR -> do
@@ -473,14 +477,14 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
473477 NAbs param body -> do
474478 (paramT, varMap :: VariableMap) <- case param of
475479 Param name -> do
476− t <- freshSrc
480+ t <- fresh
477481 return (NTypeVariable t, M.singleton name . scheme $ NTypeVariable t)
478482 ParamSet set variadic binding -> do
479483 setBindings <-
480484 M.fromList <$> set
481485 `for` ( \(name, def) -> do
482486 t <- case def of
483− Nothing -> NTypeVariable <$> freshSrc
487+ Nothing -> NTypeVariable <$> fresh
484488 Just def' -> infer def'
485489 return (name, scheme t) -- TODO: This is bad: it probably shouldn't be a scheme
486490 )
@@ -518,7 +522,7 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
518522 condT <- infer cond
519523 condT ~~ NAtomic Bool
520524 infer body
521− NSynHole _ -> NTypeVariable <$> freshSrc
525+ NSynHole _ -> NTypeVariable <$> fresh
522526 where
523527 equality lhs rhs = do
524528 lhst <- infer lhs
@@ -578,14 +582,14 @@ normalizeBindings bindings = case bindings' of
578582 Just set -> \v -> Fix $ Compose $ Ann (SrcSpan src src) $ NSelect set (pure $ StaticKey v) Nothing
579583 in (\v -> fromName (pure v) (f v)) <$> names
580584
581−inferNormalizedBindings :: NormalizedBinding NExprLoc -> InferM' (Map VarName Scheme)
585+inferNormalizedBindings :: NormalizedBinding NExprLoc -> InferM (Map VarName Scheme)
582586inferNormalizedBindings = traverse inferNormalizedBindings'
583587 where
584− inferNormalizedBindings' :: NormalizedBinding' NExprLoc -> InferM' Scheme
588+ inferNormalizedBindings' :: NormalizedBinding' NExprLoc -> InferM Scheme
585589 inferNormalizedBindings' (F.Pure expr) = inferGeneral expr
586590 inferNormalizedBindings' (F.Free m) = scheme . NAttrSet <$> inferNormalizedBindings' `traverse` m
587591
588−inferNormalizedBindingsRecursive :: NormalizedBinding NExprLoc -> InferM' (Map VarName Scheme)
592+inferNormalizedBindingsRecursive :: NormalizedBinding NExprLoc -> InferM (Map VarName Scheme)
589593inferNormalizedBindingsRecursive n = do
590594 let components = case AM.topSort . AM.scc $ bindingGraph n of
591595 Left x -> [foldMap AM.vertexSet x]
@@ -596,7 +600,7 @@ inferNormalizedBindingsRecursive n = do
596600 toScheme (F.Pure t) = t
597601 toScheme (F.Free m) = scheme $ NAttrSet $ fmap toScheme m
598602
599−inferComponents :: NormalizedBinding NExprLoc -> [Set (NonEmpty VarName)] -> InferM' (NormalizedBinding Scheme)
603+inferComponents :: NormalizedBinding NExprLoc -> [Set (NonEmpty VarName)] -> InferM (NormalizedBinding Scheme)
600604inferComponents _ [] = pure M.empty
601605inferComponents n ((S.toList -> paths) : otherComponents) = do
602606 let bindings = catMaybes $ paths <&> \path -> (path,) <$> lookupExpr path n
@@ -604,7 +608,7 @@ inferComponents n ((S.toList -> paths) : otherComponents) = do
604608 traceSubtree (showExpr . bindingsToNExpr $ bindings)
605609 . inferGeneral' (NAttrSet . fmap toScheme)
606610 $ do
607− tvsExprs <- for bindings (\(a, b) -> (a,b,) . NTypeVariable <$> freshSrc)
611+ tvsExprs <- for bindings (\(a, b) -> (a,b,) . NTypeVariable <$> fresh)
608612 let tvsExprs' =
609613 foldl' (M.unionWith mergeBindings) M.empty $
610614 fmap (\(a, b, c) -> normalize a (b, c)) tvsExprs
@@ -713,10 +717,10 @@ getReferences expr@(Fix (Compose (Ann _ x))) = case x of
713717 (Nothing, other) -> (Nothing, other)
714718 _ -> (Nothing, getReferences u)
715719
716−inferBinding :: [Binding NExprLoc] -> InferM' (Map VarName Scheme)
720+inferBinding :: [Binding NExprLoc] -> InferM (Map VarName Scheme)
717721inferBinding = normalizeBindings >=> inferNormalizedBindings
718722
719−inferRecBinding :: [Binding NExprLoc] -> InferM' (Map VarName Scheme)
723+inferRecBinding :: [Binding NExprLoc] -> InferM (Map VarName Scheme)
720724inferRecBinding = normalizeBindings >=> inferNormalizedBindingsRecursive
721725
722726renderPretty :: Pretty x => x -> TL.Text
@@ -726,7 +730,7 @@ showExpr :: NExpr -> Text
726730showExpr = TL.toStrict . renderLazy . layoutPretty defaultLayoutOptions . P.group . prettyNix
727731
728732inferGeneral :: NExprLoc -> InferM Scheme
729−inferGeneral x@(Fix (Compose (Ann src _))) = runReader src . traceSubtree (showExpr . stripAnnotation $ x) $ do
733+inferGeneral x@(Fix (Compose (Ann src _))) = local (const src) . traceSubtree (showExpr . stripAnnotation $ x) $ do
730734 (t, p, keep, s) <- inferGeneral' id $ infer x
731735 solveAndClose p $ sub s $ keep :=> t
732736
@@ -774,9 +778,7 @@ rangeFromSet = RS.fromAscList . S.toAscList
774778
775779solveAndClose ::
776780 Members
777− '[ Writer (TypeVariable, SrcSpan),
778− Reader SrcSpan,
779− Fresh,
781+ '[ Fresh,
780782 Writer PredicateError,
781783 Writer UnifyingError
782784 ]
@@ -800,8 +802,6 @@ solveAndClose range (cs :=> t) = do
800802solveConstraints ::
801803 Members
802804 '[ Fresh,
803− Reader SrcSpan,
804− Writer (TypeVariable, SrcSpan),
805805 Writer Pred,
806806 Writer PredicateError,
807807 Writer Constraint
@@ -901,9 +901,7 @@ type AttrSetPath = NonEmpty Text
901901
902902lookupAttrSet ::
903903 Members
904− '[ Reader SrcSpan,
905− Writer (SrcSpan, Errors),
906− Writer (TypeVariable, SrcSpan),
904+ '[ Writer (SrcSpan, Errors),
907905 Writer Pred,
908906 Fresh
909907 ]
@@ -911,12 +909,12 @@ lookupAttrSet ::
911909 AttrSetPath ->
912910 Eff r (NType, TypeVariable)
913911lookupAttrSet (NESingle p) = do
914− set <- NTypeVariable <$> freshSrc
915− var <- freshSrc
912+ set <- NTypeVariable <$> fresh
913+ var <- fresh
916914 tell (HasField set (p, scheme . NTypeVariable $ var))
917915 return (set, var)
918916lookupAttrSet (p :|| ps) = do
919− set <- NTypeVariable <$> freshSrc
917+ set <- NTypeVariable <$> fresh
920918 (innerSet, var) <- lookupAttrSet ps
921919 tell $ HasField set (p, scheme innerSet)
922920 return (set, var)