Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Evaluate arbitrary lambdas in animation primitive #1169

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

georgefst
Copy link
Contributor

@georgefst georgefst commented Oct 26, 2023

The major limitation of #1164 is that we can only use trivial functions as the second argument to animate, without the evaluator getting stuck. That is, functions where only a substitution is needed for the function body to reach a normal form.

Consider an expression animate 5 (λt. circle (t × 2)). Note that both arguments are normal forms. The problem is that evaluating this requires evaluating circle (0 × 2), circle (0.1 × 2), circle (0.2 × 2) etc. in order to generate the frames of the animation. Whereas for all of our other primitives, once the arguments are in normal form, computing the normal form of the applied function is trivial. This all happens in the function primFunDef, which establishes the semantics of our primitive functions, and is not set up to be able evaluate further. Even at a higher level, it's not clear how we should handle this, given that the new expressions requiring evaluation are not guaranteed to be normalizing.

This PR lifts the trivial-functions restriction in most circumstances, in a hacky unprincipled way. It breaks all sorts of abstractions, and doesn't guarantee that evaluation respects the configured termination bound. Of course, it should not be merged in anything resembling its current form, but it's useful for exploring more complex animations. A proper solution will require some sort of reworking of the evaluator, and I'm not yet sure what that should look like. Alternatively, and this is my personal preference, we could just embrace the projections-based approach discussed in #1173.

@georgefst georgefst mentioned this pull request Oct 26, 2023
@georgefst georgefst mentioned this pull request Nov 14, 2023
@georgefst georgefst force-pushed the georgefst/animations branch 3 times, most recently from 7f164c1 to 85d1f94 Compare November 20, 2023 12:07
@georgefst georgefst force-pushed the georgefst/animations branch 2 times, most recently from 9a258af to 66c14ec Compare November 20, 2023 13:16
Previously, it was possible for example to take an expression `match (? : Maybe Animation) with {Nothing -> ? ; Just x -> ?}`, then, by raising `Animation`, create `match (? : Animation) with {Nothing -> ? ; Just -> ? ; _ -> ?}`. Now we ensure that those first two nonsensical branches are removed.

Signed-off-by: George Thomas <[email protected]>
Base automatically changed from georgefst/animations to main November 22, 2023 10:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant