compiling-to-categories / concat

Compiling to Categories
http://conal.net/papers/compiling-to-categories
BSD 3-Clause "New" or "Revised" License
431 stars 49 forks source link

Let ccc turn Coercions into categorical objects #103

Closed nomeata closed 1 year ago

nomeata commented 2 years ago

This (still PoC-level) patch, as asked for by @mikesperber, changes ccc to not use coerce when encountering a Cast, but actually descend into the given Coercion and build an arrow in the target category “implementing” that coercion, using repr, abst, fmap, compose, etc.

The high-level idea is to take a coercion co :: t1 ~ t2 and turn it into an arrow t1 `k` t2 in the target category.

It is still partial, and falls back to coerce when it finds a Coercion it cannot handle.

nomeata commented 2 years ago

While it works successfully on all coercions in a single, but non-trivial test case provided by Mike, it seems it cannot handle all coercions in the test case here.

In particular, when it finds as a coercion FunCo <t1> co :: (t1 -> a) ~ (t1 -> b) for co :: a ~ b, the current strategy is to use fmapC (goCoercion co), which requires `FunctorCat, which does not exist in all categories.

I am unsure if

nomeata commented 2 years ago

Effect of this patch on the golden tests: https://gist.github.com/86ed8d282ac59b1ff5ab02749d24395a

mikesperber commented 1 year ago

Patch to unbreak the test suite upcoming.