I'm trying to implement the composition product of monomial endofunctors for the van Laarhoven encoding. It is very hard.
=> More informations about this toot | More toots from julesh@mathstodon.xyz
@julesh :D are you making progress?
=> More informations about this toot | More toots from zanzi@mathstodon.xyz
@zanzi I made what might be a bunch of progress but then got stuck. I expected it to be very hard and it did not disappoint
=> More informations about this toot | More toots from julesh@mathstodon.xyz
@zanzi I expect it to be a more complicated version of the tensor product, which in Kmett's source code looks like this:
=> More informations about this toot | More toots from julesh@mathstodon.xyz
@julesh @zanzi So are you looking for something of type LensLike f (s, t -> s') (t, t') (a, b -> a') (b, b')?
What makes you interested in the van Laarhoven encoding?
=> More informations about this toot | More toots from sjoerd_visscher@types.pl
@julesh @zanzi Ah, your new blogpost clarifies things. I’m wondering what it means that the Interaction data type is the free monad on a monomial.
=> More informations about this toot | More toots from sjoerd_visscher@types.pl
@sjoerd_visscher @julesh Yeah, the Interaction data type is a bit mysterious, I'd be curious if you have some ideas about it!
=> More informations about this toot | More toots from zanzi@mathstodon.xyz
@zanzi @sjoerd_visscher Wow, this is a very interesting observation. So these "monadic traversals" are kleisli arrows for the free monad on a monomial
By the way, the reason I used vL lenses in this post was mostly for fun. But the actual reason I care about them is because of my "less pointless lenses" trick (I have a blog post on that from a couple of years ago, and a paper on it that I'll finish Any Month Now)
https://julesh.com/2023/01/14/making-haskell-lenses-less-pointless/
=> More informations about this toot | More toots from julesh@mathstodon.xyz
@julesh @zanzi @sjoerd_visscher I've used these monadic traversals before (called them journeys because "monadic traversal" seemed to imply something else) for a toy jq implementation: https://github.com/ncfavier/jq-optics
=> More informations about this toot | More toots from ncf@types.pl
@julesh @zanzi @sjoerd_visscher Your (and my) conjecture can probably be proved using https://arxiv.org/abs/1402.1699
=> More informations about this toot | More toots from ncf@types.pl
@ncf @zanzi @sjoerd_visscher Wow!! Very nice!
I'll probably edit my post to include a link to this
=> More informations about this toot | More toots from julesh@mathstodon.xyz
@ncf @julesh @sjoerd_visscher Ah, well, done!
I was wondering if it would end up being isomorphic to s -> Free (IxStore a b) t, so glad to see that it's true.
@Andrev you mentioned that you can get this using kleene star over containers, is that with the composition product?
=> More informations about this toot | More toots from zanzi@mathstodon.xyz
@zanzi @ncf @julesh @sjoerd_visscher yes
=> More informations about this toot | More toots from Andrev@types.pl
@Andrev @ncf @julesh @sjoerd_visscher cool! I wonder if that's related to the fact that it's a free monad, then
=> More informations about this toot | More toots from zanzi@mathstodon.xyz
@julesh @ncf @zanzi @Andrev what’s IxStore?
=> More informations about this toot | More toots from sjoerd_visscher@types.pl
@sjoerd_visscher @julesh @zanzi @Andrev What the paper calls PStore:
data IxStore a b t = IxStore a (b → t)
=> More informations about this toot | More toots from ncf@types.pl
@ncf @julesh @zanzi @Andrev Ah, the monomial.
=> More informations about this toot | More toots from sjoerd_visscher@types.pl
@sjoerd_visscher @ncf @julesh @Andrev how do you define monomials in haskell?
=> More informations about this toot | More toots from zanzi@mathstodon.xyz This content has been proxied by September (3851b).Proxy Information
text/gemini
