Skip to content
This repository was archived by the owner on Apr 1, 2025. It is now read-only.

Conversation

@robrix
Copy link
Contributor

@robrix robrix commented Jul 18, 2019

This PR explores folds over Core without iter—direct recursion, fromScope, and so on.

I’m sorry to be removing iter and cata, but recursion schemes over nested datatypes require a bunch of extra machinery that I’d rather avoid.

@robrix robrix changed the base branch from master to scope-safety July 18, 2019 18:46
This was referenced Jul 18, 2019
@robrix robrix marked this pull request as ready for review July 18, 2019 20:41
Copy link
Contributor Author

@robrix robrix left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ready for review.

stripAnnotations (Var v) = Var v
stripAnnotations (Term t)
| Just c <- prj t, Ann _ b <- c = stripAnnotations b
| otherwise = Term (hmap stripAnnotations t)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is slightly less pretty than the iter definition, but is equivalent in effect and may even be a little faster (tho I certainly haven’t measured).

| otherwise = Term t


instance Syntax Core where
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Goodbye!

where bind (Ignored x) f = let x' = name x in (,) x' <$> local (x':) (getConst (unScope f))
prettyCore :: Style -> Term Core User -> AnsiDoc
prettyCore style = run . runReader @Prec 0 . go (pure . name)
where go :: (Member (Reader Prec) sig, Carrier sig m) => (a -> m AnsiDoc) -> Term Core a -> m AnsiDoc
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

go is a direct-recursive worker function, walking the Term via a helper continuation which we extend to deal with Incrs efficiently as we walk under binders.


-- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
Ann _ c -> go var c
where bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope f)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the real meat of the change: we use fromScope to transform the Scope () f a (which is isomorphic to f (Incr () (f a))) to f (Incr () a), and then call go to recur over it with an extended continuation. I.e. if var :: a -> m AnsiDoc, then incr (const (pure x')) var :: Incr () a -> m AnsiDoc. Using this continuation enables us to avoid performing fmaps as we recur through the structure.



interpret :: (Carrier sig m, Member eff sig, Syntax eff) => (forall a . Incr () (m a) -> m (Incr () (m a))) -> (a -> m b) -> Term eff a -> m b
interpret = iter id send
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we want to implement something like interpret again in the future, it should be easy enough since it shouldn’t actually require a Syntax instance to walk the Term direct-recursively, just an HFunctor instance.

@robrix robrix mentioned this pull request Jul 22, 2019
4 tasks
@robrix robrix requested a review from a team July 23, 2019 19:57
@robrix robrix changed the base branch from scope-safety to master July 29, 2019 14:55
@robrix robrix merged commit 5179e88 into master Aug 2, 2019
@robrix robrix deleted the break-hearts-not-builds branch August 2, 2019 18:28
@robrix robrix mentioned this pull request Aug 6, 2019
8 tasks
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants