Hi Conal,
> I’ve cloned your gist and tried out an idea to simplify verifying the
> required constraints on linear map values.
>
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.
> Am I right in thinking that the first two (Obj) arguments proj1 and proj2
> serve as proofs that the types involved are legitimate for the category (k)?
>
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.
https://github.com/sjoerdvisscher/data-category/blob/master/Data/Category/Boolean.hs
> 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 fstL and sndL in 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 Category etc
> 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'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.
> 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.
>
I scanned through it and was quite impressed. Definitely something to dive
deeper into.
greetings,
Sjoerd
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
