Lambda World 2019 - A categorical view of computational effects - Emily Riehl
2019 ж. 3 Қар.
24 884 Рет қаралды
In this Lambda World 2019 keynote, Emily Riehl discusses category theory and computational effects.
Slides are available here: www.math.jhu.edu/~eriehl/lambd...
------
Follow:
- / lambda_world
- / 47deg
- / emilyriehl
Visit:
-www.47deg.com/events for more details
-www.lambda.world
She's a brilliant presenter!
Thanks a lot, I have the book "Algebraic Theories" (with a preface by Lawvere), sitting on my bookshelf for more than a decade. This is a nice overview of things. Maybe someday it'll be of use to me :)
I wish we had some empirical examples on the application of lawvere theory, even if it is apples to fruits
The category of natural numbers with matrices only seems strange because this underlying structure is hidden: associate each number n with R^n. Then it's also clear why 0 is not allowed. There's no vector space R^0.
R^0 is a perfectly good vector space. It's zero-dimensional, has only one element (zero) and has a basis given by the empty set. (In fact it's a rather important space, being both the initial and terminal object in any category of vector spaces.) I think the only reason zero is excluded in the example brought up in this talk is that we usually don't have empty matrices in mind when we think of matrices. But there's nothing wrong with them, they're certainly useful in programming, and in fact Emily includes zero in her later ACT 2020 talk (kzhead.info/sun/htegddqqe3iApoU/bejne.html).
@@jonathanlong4042 Of course you are right about R^0, 0-dimensional with basis the empty set. Exactly! Maybe I was thinking something else? I will check out your link...
I read the paper suggested on proof and progress you pointed. More encompassing than the way we were taught. Thanks for including the symbolic which no longer seems in fancy due to connectionist AI turn of affairs.
Здорово упростили. Выкинув из выступление понятие монойда. Но все-таки стоило бы оставить.Иначе сразу непонятно зачем там IdA например. Для чего.
Identity required for isomorphism - my question answered ✅
Why not using the Kleisli algebras for the monads? What's the difference?
after 32:06 , the abstraction level just soared up to the sky...
Lmao and this is just the shit she does for fun.... higher dimensional category theory and homotopy type theory are about as scary as math gets
Yeah, now i see what you mean. they had us believe that we have a chance in the first half!=)
Ellen Ripley of math.
Perhaps, the highest of compliments one can be given.
30:15 His question sounded like it relates to composition of monads (e.g. compose list monad and maybe monad). In general monads do not compose but some specific monads are composable. I think his question relates to monad transformers....
I think that's the point of the talk: monads aren't composable, but if you choose to work with Lawvere theories instead you can have composition and other operations.
I don't quite understand how identity was defined for monads. For example around 24:26 for lists. I understand how pure works but I don't quite see how that is a function from the same object back to itself. I guess if we considere the object to be the set of plain As and also list As then we always stay inside the sambe object when using identity. But at least in haskell plain A and list A have different types? Will there not arise any problem from that? I guess maybe not?
As she said, categorical structures are not necessarily to be interpreted as sets and functions. They can be whatever you want as long as they satisfy the category definition. In this case the objects of the category are types, but morphisms (arrows) between objects A and B, are programs with input A and output TB (for a given T). In order to see if this choice of objects and arrows satisfy the category definition, one must define identity for this new arrows: an arrow from A to A (not a function, perhaps you're misguided by the word identity here), in this example an arrow from A to A is a program with input A and output TA. It doesn't matter they're not composable in the traditional sense, for that you can use the bind operator
@@joshuamartinez1506 Exactly. As long as we can define composition on the arrows in question (bind in the case of monad) then the identity arrow (monadic function) is that which when composed with any other arrow (monadic function) is equivalent to that other arrow. It is rather confusing at first glance because a lot of our initial intuition for categories comes from sets and functions. In this case it's clear that objects in categories are only defined so that we can talk about arrow composition.
Bind's signature is (A -> T) -> T -> T. Return or Pure's signature is A -> T, so.... if you pass Return (Pure) to Bind you get (A -> T) -> T -> T which reduces to T -> T which is the identity function. Given that a monad always has a bind and return function by definition, you're good. A category requires Associativity and Identity, bind is associative, and identity can be constructed from bind/return. If you didn't have a return aka pure you wouldn't be able to get identity and therefore it wouldn't be a category. She specifically said "It is not an identity function, but it plays the role of an identity function", but putting return into bind is a simple way to get your identity arrow for T -> T .
The confusion might have arisen because on this slide she erroneously put the squiggly arrow for id_A from A to list (A), instead of from A to A. The straight arrow, on the other hand, which does represent a function, was correctly described.
27:23 I understand this question as is there another way except flatMap to fulfil the monad conditions with lists? Any bind with return should do nothing and any f looking like A -> list(B) should give the same result if instead of calling on A it would be called on return(A) followed by bind(f). It is not easy to come with a working example for lists, and for Maybe there simply no other implementation obiding these rules
"associative" is easy to motivate: composition is defined for 2 things, and associativity tells you how to compose 3 things. (More precisely, it tells you that the two natural ways are equal).
after a year in Category theory those seem very normal but someone that has no idea about Category theory probably this is chaos.
I study non linear dynamics and chaos and this is harder lol
@@josemaria_landa If you're comfortable writing functional programming you see a lot of stuff like this with a bit more practical usage, makes it a LOT easier to conceptualize. Ironically I have almost no category theory knowledge other than the definition of a monad, but having used them to solve practical problems it wasn't that hard to know yeah bind aka flatmap maps (runs a function on each item in the list returning a new list) and then flattens (concatenates a list of lists into a single list). That's useful because it allows us to compose t -> List functions like t -> t. An example would be if you have a function countTo, which takes a number like 5, and returns a list [1,2,3,4,5], but you want to do it twice, you can use bind to make that happen. countTo 5 -> [1,2,3,4,5] and then we bind to countTo again, and we get [[1],[1,2],[1,2,3],[1,2,3,4],[1,2,3,4,5]] in the map, and then it flattens to [1, 1,2, 1,2,3, 1,2,3,4, 1,2,3,4,5] for the final result. it allows us to compose integer -> List and integer -> List by having an intermediate value of List and using concatenate to flatten to just List. It's easy to overthink it, also if you're not familiar with it there's definitely a lot of jargon. I didn't graduate from university, barely got a C in calculus, have a learning disability but for the most part I was able to keep up. I suspect it's hard to get a handle on categories if you lack a specific thing to think about instead of always thinking of things in the abstract. I find lists an intuitive specific thing to think about because we use them constantly in software development. What I don't understand is how a lawvere theory just lets us compose different kinds of monad. I presume this is somehow analogous to monad transformers, but what's deeply unclear is how this would even work or what usage would look like.
I wonder if 30 years from now we'd be able to group people by whether they understood certain concepts or not. Similar to how we define different types of human ancestors. Anyhoo, great lecture, didnt feel like it was completely beyond my comprehension
I was very distracted…
kzhead.info/sun/htexYsOCgqJ4Zo0/bejne.html is what bothers me about Category Theorists. A re-specification of a perfectly reasonable practical programming question in to highfaluting academic lingo is a bit arrogant me thinks. The need for category theory in computation comes precisely from the practical need in programming. I am not suggesting that Emily Riehl is arrogant but taking Category Theory away from its practical necessities in Software Development is defeating to the cause of totally embedding and applying Category Theory as a bedrock of Software Engineering.
This is a mathematician giving a mathematics talk in mathematical language. When presented with a question about the content, it only makes sense to frame it in the same way that the rest of the presentation is framed, so that it can be answered via the material in or related to said presentation. She is not a programming professor and the question was not asked in a vacuum, so there's no reason that she should give an explanation in a different format, nor is there any reason to believe the person asking the question would even want that. Further, the answer to that particular question (that a different choice of list composition defines a different monad structure) really is dependent on the mathematical formalism being discussed. Aside from that, your view seems exceedingly closed-minded. Category theory doesn't exist only for computation, and computation doesn't exist only for programming. General theory getting specified to particular applications happens all the time, if you're only interested in the very base level of application then don't watch a lecture about the theory. On the other hand, abstraction is a crucial part of programming even in the very base level, so category theory (which is in a sense an abstraction of abstractions) is a reasonable level of abstraction for a programmer to be thinking at. If you want category theory to be the bedrock of software engineering, you have to actually understand category theory.
also category theory is a language that came out of algebra and topology. so certainly mathematicians have a right to use it.
So bridging understanding and translating two different perspectives is "arrogant"? By your logic, the programming question is just as well arrogant, "highfaluting academic lingo" to the mathematician.
Category theory is not mathematics or computational theory for that matter... It is a symbolic cognitive mapping of derivatives from a structured order of systems replicated as map symbol system think... etc... If one has studied any kind of hermenutical or alchemical explorations of language and systems this all becomes a rather obvious game of associative patterning, very reminicient of the kabbalah and mandala based conceptual frameworks. It is not enough to say this is gobbiligook or that this is some amazing new territory of exploration... pay attention to the general use of terms and the symbols oriented along the exploratory process. This all seems to be systemic breakdown of a field of consciousness considering the territory of metaphysics as reoriented along the praxis of programming mathematical computer functionality and the sublimation of the territory into the map... ill leave you with this thought... it would be possible to completely reinvent an entire symbolic language and mathematics based on an intended meaning system relational to it... monads.... leibniz... solar systems... quantumn fields... tesla feeding pigeons in the park, shaking his head for decades in utter disbelief at the ability of the mind to mask itself from reality... lost in the wilderness of the exegesis of knowledge sorcery. This is all not a real territory offering new answers except as outgrowth of its intention, like a painter painting a painting. If i am trying to figure out what is going on in economics I can program a computer with all the data using every seperate system of analysis and then filter through the various answers and then interalte them based on secondary considerations or third fourth or fifth... this realm of information analysis is not the real world and never ever will be... unless through conditional patterning certain systems can be forced to be patterned and controlled this way... think of advanced shipping logistics of Amazon or FedEX... imagine trapping the world in an incredibly accurate map... that then crumbles around itself confronted with the everpresent cosmolocial fact of Kants Noumenon! stop the sorcery! mill was the most evil moralist ever. good and truth are not relative... human faculty must only use that way of thinking as discursive dialectical analysis.
Bro. Can u recommend some reading?
Can you recommend some reading pls
That's some overcomplicated way to tell the associativity of monad's "join" natural transformation property join . fmap join == join . join "join" after "joining" within is the same as "joining" after "joining" from outside
Take a drink every time computation or computational is said.