search

anoma / geb

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

Uncurry Pipeline Usage #106

Open agureev opened 1 year ago

agureev commented 1 year ago

Now that we tested out uncurry so that our compilation can be intuitively tested pointwise both in Geb and in Poly instead of passing through the additional isomorphisms, we have a question regarding how to actually implement it.

uncurry currently needs three arguments, two for domain and codomain of the exponential object and one for the morphism we are applying it two. The domain/codomain are needed since we don't have accessors to so-hom-obj.

In order to not burden the user with providing explicit types, we will have to figure out (at least initially until higher-order function translation to Vamp-IR is implemented) how to streamline this process.

rokopt commented 1 year ago

Does #107 address this?

rokopt commented 1 year ago

Can this be closed as fixed by #115 ?

rokopt commented 1 year ago

Can this be closed as fixed by #115 ?

Not yet -- Artem is still working on more required indexing changes.

agureev commented 1 year ago

Made improvements in #127. That is, now given a term whose type is an n-iterated fun-type with codomain A such that A is not of type fun-type, it compiles to an n-argument function in Vamp-IR.

However, that does not suffice for general cases. E.g. compiling (pair (unit) (lambda (list (coprod so1 so1)) (index 0))) will still give out a quoted function on the right.

agureev commented 1 year ago

Note that #138 changes the compilation to optimize costly uncurry with a simple replacement strategy.