-
Notifications
You must be signed in to change notification settings - Fork 3.5k
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
[Relay][Prelude] Remove Peano nats from the prelude #3045
Conversation
Please review @jroesch, @MarisaKirisame, @zhiics |
Indeed, the VM updates have unblocked this PR, so I think it can be reviewed now. @MarisaKirisame I think I think it may be a problem with the actual gradient produced because the type checker reports failing to unify edit: I think the error is because |
…ion in global function)
it is failing because test_pow use iterate which use natrual number. it is design specifically to test adt and pattern matching work for reverse mode. can you add nat in that test? |
I think the type error is happening because there are globals (namely iterate) left in the final gradient, even though the gradient pass assumes that DeGlobal gets rid of them all (but it doesn't handle global functions that are recursive) |
ping @MarisaKirisame @jroesch @joshpoll please review again and see if we can move on to merge it in |
@slyubomirsky @MarisaKirisame did you resolve the previous thread of conversation? |
@slyubomirsky can you move the nats into a common file, and restore the test in anf and gradient into exactly the same as before? I am explicitly trying to test pattern matching there. |
That will be an easy change, thanks for explaining those tests for me. |
…they were previously important
Thanks, @MarisaKirisame @slyubomirsky @jroesch , this is now merged |
@jroesch and others have noted that the Peano (unary) nat, other than being a convenient example for ADTs, is not actually very useful outside of proof assistants and should be replaced with integer scalars.
This PR removes nats from the prelude and replaces them with integer scalars in other functions. Unfortunately, there appear to be issues with the interpreter that prevent the scalar operations from properly being lowered, so I have left this PR as a WIP until those issues can be fixed and allow the tests to work. (@MarisaKirisame says the bug encountered here is most likely fixed in the VM PR.)