A Categorical View of Computational Effects
ฝัง
- เผยแพร่เมื่อ 25 ก.ค. 2024
- Keynote by Dr. Emily Riehl
C◦mp◦se :: Conference
www.composeconference.org/
May 18, 2017
Slides: www.math.jhu.edu/~eriehl/compo...
Monads have famously been used to model computational effects, although, curiously, the computer science literature presents them in a form that is scarcely recognizable to a category theorist - I’d say instead that a monad is just a monoid in the category of endofunctors, what’s the problem? ;) To a categorical eye, computational effects are modeled using the Kleisli category of a monad, a perspective which suggests another categorical tool that might be used to reason about computation. The Kleisli category is closely related to another device for categorical universal algebra called a Lawvere theory, which may be a more natural framework to model computation (an idea suggested by Gibbons, Hinze, Hyland, Plotkin, Power and certainly others). This talk will survey monads, Lawvere theories, and the relationships between them and illustrate the advantages and disadvantages of each framework through a variety of examples: lists, exceptions, side effects, input-output, probabilistic non-determinism, and continuations. - วิทยาศาสตร์และเทคโนโลยี
I am leaving this comment here hoping that someone would find it useful. To the audience, I would strongly recommend that you watch the entire set of Category Theory videos from Bartosz Milewski on TH-cam, and probably after you are into a few videos come back and watch this video. It would be more interesting and informative that way - you would be able to relate to things much better, just my personal opinion.
So true. Just go ahead and watch the Category Theory for Programmers (section 1 of 3 should be enough) by Bartosz, which should get you familiar with the language of this talk.
I've watched *so* many Category Theory talks, and her explanations are *so clear* to me. She is great at explaining. I learned so much! Thank you!
This was such an awesome talk. I now see the bind operation in a completely different (and much clearer) light. The type signature (m a -> (a -> m b) -> m b), when flipped ((a -> m b) -> m a -> m b) can be seen as taking a function, g :: a -> m b, and "extending" it to a function g* :: m a - > m b, taking you to a simple world of composibility. It's incredible that a top-level mathematician can make something so clear in the field of programming, even when she doesn't program herself!
Hmm, cool, you're right!
Personally I find monads more enlightening by focusing on the Join function rather than Bind. Because Join cuts to the essential difference beteween Monads and Functors: Monads can not only map a function over the functor structure, but can "merge" the functor structure resulting from the function itself (the M of the Mb resulting from the function a --> Mb) with the existing functor structure (the M of the Ma). Join is just M(Mb) --> Mb i.e. flattening/joining/merging the nested functor structure with the outer one. This highlights precisely how Monads allow for expressing more powerful types of computation than Functors (or Applicatives for that matter).
Excellent, I love the simple mathematical overview of monads! Will try to understand the Lawvere theory connection going forward. (Can't wait to dive into "Category Theory in Context" by the speaker, which I just ordered).
But then I am a mathematician, not a computer scientist (having studied 30 years ago my math is a little rusty, now I'm learning category theory just for fun), can't say how well this talk suits the intended audience.
Category Theory in Context actually is my second book on Category Theory, the first one was “Category Theory” by Steve Awodey.
The mention of "wCPO" at 19:05 is omega complete partial order:
en.wikipedia.org/wiki/Complete_partial_order
pretty relevant in domain theory as found in scott strachey's denotational semantics
Great talk!
I finally understood monads. Thanks Dr Riehl!
when she clarified what she meant by "large function" she probably meant what computer scientists mean by "higher kinded types" e.g. type class constructors taking a type as an argument and producing a (different) type as a result.
«Large» here is in the sense of «too large to be considered a usual set-theoretically defined function», because usually (though not always), one assumes that a function's domain (and therefore its graph too) is a set; but here the domain would be the collection of all sets (or some other collection) which is (again, usually) too big to be a set. Check "class (set theory)" on wikipedia; look for "class function". In the example of this video, the domain of such "function" would be all the objects of 𝐒𝐞𝐭, of which there are too many to form their set (usually!).
We need more of them
As coeffects have increasingly become an object of research by computer scientists, has the notion of intensional semantics by Brookes and Geva become any more established in the C.S. community? That is, have models of computation taken on a more comonadic, less monadic, flavor since the '90s? Could anyone recommend any papers discussing these two perspectives?
As much as i wanted to understand something this talk is way over my head 😂
The guy from 44:06 is a spitting image of Gilfoyle from SV!
Gershum reminds me of a grown up version of the main Khaki Scout from 'Moonrise Kingdom', which is high praise indeed. (Comments Get Closed)
6.25, bottom right. There were pastries at this talk.
This question is probably not especially relevant to the topic of this video, but who knows -- perhaps someone in the audience might care to reply: Standard and higher category theory are very clearly topological in nature, but have there been any research attempts to geometrize category theory? Are there even any theoretical footholds for starting such research?
Hi declup - your point about the topological nature of higher category theory is correct; you have great intuition. In fact, the basis for much of higher category theory is the notion of a simplicial category, which is the notion of a topological simplex generalized to simplicial sets and simplicial categories. In fact, in this theory, you have a notion of 'geometric functors' and 'geometric realization' of these simplicial categories. If you'd like to know more, read Emily Riehl's Higher Category theory, and any books you can find on Homotopical Algebra. The foundation of this theory lives in the form of Quillen's model categories from Algebraic Topology.
@@epi6676 is this line of thinking what lead to homotopy type theory as a foundational mathematics?
@@elcapitan6126 yes
Can someone clarify the idea of a notion of computation? All she seemed to do was mention a lot of examples and explain that a T-program is a function A->TB where A and B are types representable as finite sets and that we can make a pure function out of a T-program with the codomain being B and the domain being the pre-image of B... looking at the examples it seems like a notion of computation applied to some type B is just some products and coproducts of B with some other types (exceptions, side effects, etc). How wrong am I?
I could find many interesting youtube videos about 'tagless final' or 'free monad'. You can define a computational program of algebraic models with Monads. It says that we can define description of computation (what-to-do) with monads without any detailed interpretations of how-to-do. It's more like a magic. BTW, I do Scala programming language these days.
I think she mentioned about computation a little.
for T = List
`(concat . map g . f ) ` is an example that has concrete computation ( They seems to be assumed. ) .
for T = Partiality
the computation is the trivial inclusion i.e. `do nothing` computation .
I think the answer is a bit simpler than the other replies (but I am years late so there is that). You can think of a program as just being a function that takes an input A and produces an output T B, where A and B are types in your programming language and T is some special kind of type of computation (list, future, maybe, option and so on). This is also known as a Kliesli arrow.
Note to the video creators: please keep the slides visible when the presenter is talking about their content, particularly when the content is a bit dense like this.
THIS! 1000 times this!
As a work around, it helps to open the PDF of the slides in another window and view the video and slides side by side. www.math.jhu.edu/~eriehl/compose.pdf
Excellent talk. But it would be even greater if all those stupid questions were asked at the end of the talk.
It's amusing how ingratiating category theorists have to be to the computer scientists!
what do you mean? I think she's just empathizing with an audience that isn't familiar with category theory but is familiar with the same notions from a Type theory point of view. Traditionally Category theory is seen as impractical abstract nonsense and Type theory extremely practical. So I guess she is trying to convince the audience they are one and the same hence equally practical.
@@elcapitan6126 makes sense!
I think the explanation is not very good, it's very confusing