justinlubin / cobbler

Refactor programs to use library functions!
5 stars 0 forks source link

Add eta-expansion to FP synthesis to support enumerating higher-order arguments #36

Closed justinlubin closed 1 year ago

justinlubin commented 1 year ago

Currently, we expand?0 : List Int to, e.g., map (?1 : T1 -> Int) (?2 : List T1), but this should get further expanded to map (\x1 . (?3 : T1)) (?2 : List T1) so that we can further expand ?3 with other functions in the library. That way, we can always simply look at the codomain of functions to perform unification as we do currently.

Implementation-wise, we will need to (1) support abstractions in the expand function; moreover, (2) when expanding a hole with the new unification process, holes at arrow types need to be eta-expanded.

justinlubin commented 1 year ago

Note: may not actually want to do this because such arguments are never fused, so it will simply slow down enumeration.

justinlubin commented 1 year ago

For reason mentioned above, will not implement this (for now, at least).