Lovely use of view patterns! It looks like it is not necessary to store the LM value, all that is needed is to store that VS2 s a b is satisfied.I’ve cloned your gist and tried out an idea to simplify verifying the required constraints on linear map values.
Yes, that's one of the reasons. The other reason is that BinaryProduct is a type family, so it is not possible to derive from the product what it originally was a product of. For example in the Boolean category with the false and true objects and an arrow from false to true, the binary product is conjunction, and there are multiple combinations that give the product false.Am I right in thinking that the first two (
Obj) argumentsproj1andproj2serve as proofs that the types involved are legitimate for the category (k)?
I'd go for (b). The proofs are just identity arrows, so you can usually use the src and tgt methods to retrieve them generically. I don't expect problems there.Admittedly passing around proof values instead of relying on constraints gives the whole library quite a unhaskelly feel, but it’s the only way I could find that really works well. And often it is possible to provide a public API for a specific category that constructs the proof values from the constraints, like I have done with
fstLandsndLin the gist.I wonder whether this trick is compatible for my goals with circuit synthesis and analysis. I want to express fairly general computations over
Categoryetc and then type-instantiate them into multiple interpretations in the form of categories of functions (for CPU execution), circuits, strictness/demand analysis, timing analysis, and hopefully others. (Rather than requiring the code to be written in this obscure categorical form, I intend to transform conventional pointful (function-specific) code via a (to-be-written) GHC plugin. Our goal is accept arbitrary Haskell code.) I hope there’s a way to either (a) preserve a simple notation like “fst” rather than “proj1 proofA proofB” or (b) automatically synthesize the proof arguments in a general/parametric enough way to allow a multitude of interpretations. I suppose I could instead replace the single generalizing GHC plugin with a number of plugins that produce different specializations of a single theoretical generalization. Wouldn’t be as elegant, though.
I scanned through it and was quite impressed. Definitely something to dive deeper into.BTW, have you see the new paper The constrained-monad problem? I want to investigate whether its techniques can apply to
Category& friends for linear maps and for circuits. Perhaps you’d like to give it a try as well. I got to linear maps as an elegant formulation of timing analysis for circuits.