why not take a break from <recent discourse> and help me figure out what an n-ary Let binding should look like?
I *think* what we need to do is to use the fact that List is a monad to define a Bind for List-indexed monads? Does this sound like it's on the right track?
"are neural networks a polycategory" - the greatest paper in the history of applied category theory, rejected by reviewer n2 after 12,239 pages of intricate coherence diagrams
7.8.2023 13:57"are neural networks a polycategory" - the greatest paper in the history of applied category theory, rejected by reviewer n2 after...dependent types puzzle N2: what does an n-ary Let binding look like?
there's a version for linear and Cartesian contexts
dependent types puzzle: how to generalise this pattern?
note: Multi-functors need to form a multicategory, so "functor from product category" does not count as an answer.
5.8.2023 21:34dependent types puzzle: how to generalise this pattern?note: Multi-functors need to form a multicategory, so "functor from product...can we define a relative monad w.r.t the environment comonad? ie we would have
return : w a -> m a
bind : m a -> (w a -> m a) -> m a
where 'w a' is a type of variables 'a' in an environment 'w'.
3.8.2023 19:17can we define a relative monad w.r.t the environment comonad? ie we would have return : w a -> m abind : m a -> (w a -> m a) ->...Watching the talks for ACT2023, as a category theorist I am glad that there are so many amazing tools being built in Python, Julia, etc, but as a functional programmer I feel like FP dropped the ball by not becoming the go-to family of languages for applied category
31.7.2023 15:52Watching the talks for ACT2023, as a category theorist I am glad that there are so many amazing tools being built in Python, Julia, etc, but...What is the right notion of "f algebra" for double categories?
Can I formulate something like an "f-algebra with relations" where the functor part gives me the constructors of an inductive type and the profunctor gives me the relations/equations/rewrites?
is there a name for these two different ways of defining a graph?
ie the definition on the left is using a set of nodes and edges with two maps inbetween, versus defining a graph as a set of vertices and a set of edges indexed by the vertices
@JacquesC2 what do I need to do to express Pi/Sigma through comma categories? do i need to form a pullback as a product in a comma category, and then show the adjunction between pullback and Pi/Sigma?
30.7.2023 15:40@JacquesC2 what do I need to do to express Pi/Sigma through comma categories? do i need to form a pullback as a product in a comma category,...first start on comma categories, we can use them to re-derive the category of algebras of an endofunctor
30.7.2023 15:30first start on comma categories, we can use them to re-derive the category of algebras of an endofunctorBig if true (up to size issues)
30.7.2023 13:08Big if true (up to size issues)finally going to try formalizing comma categories in Idris
what are some interesting examples that could be worth implementing?
29.7.2023 17:29finally going to try formalizing comma categories in Idriswhat are some interesting examples that could be worth implementing?@julesh suggested that it would have a bi-kleisli category. Is there an analogous notion of "bi-em category"
28.7.2023 12:14@julesh suggested that it would have a bi-kleisli category. Is there an analogous notion of "bi-em category"Suppose we have a functor F that's both a monad and a comonad.
Can we say something about the relationship between it's (co)kleisli and (co)EM categories?
28.7.2023 11:43Suppose we have a functor F that's both a monad and a comonad. Can we say something about the relationship between it's (co)kleisli...Monads have a very rich meta-theory, but what makes them special?
Can any of the meta-theory of monads be translated to other monoidal structures in the cat of endofunctors, ie day convolution?
27.7.2023 21:27Monads have a very rich meta-theory, but what makes them special? Can any of the meta-theory of monads be translated to other monoidal...the eilenberg-moore construction for an arbitrary functor using the freer algebra over that functor
27.7.2023 14:12the eilenberg-moore construction for an arbitrary functor using the freer algebra over that functoris it just me or are eilenberg-moore categories not as useful in functional programming?
we use kleisli categories all the time, but the em-adjunction just feels kind of tautological. what am i missing?
26.7.2023 00:08is it just me or are eilenberg-moore categories not as useful in functional programming? we use kleisli categories all the time, but the...adjoint folds? what about kan-extension folds?
25.7.2023 23:28adjoint folds? what about kan-extension folds?thinking of cancelling my GPT subscription. I don't know if GPT 4 is getting worse but more and more I keep getting better responses from GPT 3.5
23.7.2023 12:54thinking of cancelling my GPT subscription. I don't know if GPT 4 is getting worse but more and more I keep getting better responses...this isn't even a diss against mastodon, it's more just me realizing that id enjoy mastodon a lot more if it wasnt federated
18.7.2023 16:17this isn't even a diss against mastodon, it's more just me realizing that id enjoy mastodon a lot more if it wasnt federated