Open utterances-bot opened 2 years ago
There is a typo in the link to your review of adders and arrows: you wrote arrows and adders.
How would you go about implementing these ideas in a language such as Rust with a less powerful type system, but where you might observe significant performance gains from better parallelisation?
There is a typo in the link to your review of adders and arrows: you wrote arrows and adders.
Fixed, thanks.
How would you go about implementing these ideas in a language such as Rust?
I think the trick is to use Agda merely as a tool for thought. That is, lscan someRep
is an actual algorithm that divides and conquers an array to scan it. You can play around with someRep
to find one you like, and there's a easy function out of Rep
to compute what you should be doing with which array indices. Then you can just implement that in Rust, rather than needing to think deeply about how to fiddle the indices yourself.
Review: Generic Parallel Functional Programming :: Reasonably Polymorphic
https://reasonablypolymorphic.com/blog/generic-parallel-fp/index.html