anoma / geb

A Categorical View of Computation
https://anoma.github.io/geb/
GNU General Public License v3.0
28 stars 10 forks source link

Geb should use VampIR higher-order functions #89

Open rokopt opened 1 year ago

rokopt commented 1 year ago

Now that VampIR has higher-order functions, Geb should compile to them, as that should make them much more efficient than first-order functions translated from higher-order functions via Geb's currying/distributivity equivalence. (The equivalence will still be used to provide Lisp-style quote/unquote; it just won't be needed for higher-order function execution.)

@murisi provided examples of how to use VampIR higher-order functions:

https://github.com/anoma/vamp-ir/blob/main/tests/funcs.pir

lukaszcz commented 1 year ago

As far as I understand, VampIR higher-order functions are compile-time only, so they cannot non-trivially interact with field elements. Which means that while this optimisation can be used in the majority of cases, it cannot be used in general. I think that's what you mean by the "Lisp-style quote/unquote" because how otherwise would you compile e.g. (pair (lambda (index 0)) 0), i.e., storing a function inside a data-structure? Or creating an n-times composition of a given function where n depends on the (unknown) input? It seems that, in terms of the effect on the final circuit, using VampIR higher-order functions ultimately amounts to specialising each occurrence of a function as an argument to another function, pasting it into the body.

rokopt commented 1 year ago

As far as I understand, VampIR higher-order functions are compile-time only, so they cannot non-trivially interact with field elements. Which means that while this optimisation can be used in the majority of cases, it cannot be used in general. I think that's what you mean by the "Lisp-style quote/unquote" because how otherwise would you compile e.g. (pair (lambda (index 0)) 0), i.e., storing a function inside a data-structure? Or creating an n-times composition of a given function where n depends on the (unknown) input? It seems that, in terms of the effect on the final circuit, using VampIR higher-order functions ultimately amounts to specialising each occurrence of a function as an argument to another function, pasting it into the body.

Yes -- I believe this is all correct.

rokopt commented 1 year ago

Note: see the discussions in #105 for some things to remember when implementing this (in particular https://github.com/anoma/geb/pull/105#issuecomment-1523917163).

rokopt commented 1 year ago

Note: see the discussions in #105 for some things to remember when implementing this (in particular #105 (comment)).

In fact, those discussions make me wonder whether we should use VampIR higher-order functions (as suggested in this issue) at all, or just closure-convert what we can and quote/interpret what we can't within Geb itself before compiling to VampIR (via bitc).