You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Burak Emir (Mar 26 2020 at 20:41):Maybe you all know this already, but there is an account on how the CCC model of lambda calculus was used for actual implementation: Cousineau, Curien, Mauny: The Categorical Abstract Machine. Science of Computer Programming 8 (1987) pp.173-202
Burak Emir (Apr 01 2020 at 09:34):Huwig, Poigne. "A note on the inconsistencies caused by fixpoints in a cartesian closed category" https://doi.org/10.1016/0304-3975(90)90165-E
Prop 2. Let C be a Cartesian closed category with fixpoints and an initial object. Then C is inconsistent.
Burak Emir (Apr 01 2020 at 10:20):^^ I am frequently missing a discussion of fixpoints when people discuss e.g. "the category of Haskell types". As a functional programmer, I'd clearly like to have product types, sum types and fixpoints, it looks harmless to admit the initial object as the "empty sum type".
Stelios Tsampas (Apr 01 2020 at 10:26):Burak Emir said:
Huwig, Poigne. "A note on the inconsistencies caused by fixpoints in a cartesian closed category" https://doi.org/10.1016/0304-3975(90)90165-E
Prop 2. Let C be a Cartesian closed category with fixpoints and an initial object. Then C is inconsistent.
This is very different to the commonplace initial algebra-final coalgebra constructions I know of. In other words, considering a fixpoint operator on morphisms in a CCC is very different to initial objects/final objects in categories of algebras/coalgebras over an endofunctor.
Stelios Tsampas (Apr 01 2020 at 10:28):Similarly in Haskell you have fixed points of endofunctors (whose initial algebra and final coalgebra coincide btw), but I imagine you are aware of the fact.
sarahzrf (Apr 01 2020 at 13:31):in haskell you don't have an initial object
sarahzrf (Apr 01 2020 at 13:32):undefined inhabits every type, and you can distinguish const 3 from const 4 by applying them to undefined no matter the domain
Stelios Tsampas (Apr 01 2020 at 14:12):sarahzrf said:
undefinedinhabits every type, and you can distinguishconst 3fromconst 4by applying them toundefinedno matter the domain
Yes I was being fast and loose, which is morally correct.
sarahzrf (Apr 01 2020 at 14:13):that's not how it works
sarahzrf (Apr 01 2020 at 14:13):stop using that phrase until youve actually read the paper
sarahzrf (Apr 01 2020 at 14:13):unless you have, in which case sorry
sarahzrf (Apr 01 2020 at 14:14):actually sorry regardless that's pretty obnoxious :|
sarahzrf (Apr 01 2020 at 14:15):people just. cite that paper all the time in places where it really doesn't apply
Stelios Tsampas (Apr 01 2020 at 14:20):sarahzrf said:
actually sorry regardless that's pretty obnoxious :|
Sheeeesh that was intense!
sarahzrf (Apr 01 2020 at 14:24):ahhhh i meant I was being obnoxious!!
Stelios Tsampas (Apr 01 2020 at 14:24):Apology accepted, but I absolutely do not retract my statement. The paper I have read, at the same time I can never claim that my comprehension of it (or anything else) is 100% accurate. But regardless, from my understanding of haskell, I have absolutely no issue with treating it as an order-enriched category where you get the coincidence I mentioned, fully aware of the (sad) reality...
Stelios Tsampas (Apr 01 2020 at 14:24):I know, don't worry :).
sarahzrf (Apr 01 2020 at 14:26):"treating it as an order-enriched category"—you mean placing the PER from that paper on the hom-sets?
sarahzrf (Apr 01 2020 at 14:26):(took me a second to parse since i dont usually think about PERs as orderings)
sarahzrf (Apr 01 2020 at 14:28):if that is what you mean, then it's still not obvious to me what's going on
sarahzrf (Apr 01 2020 at 14:28):what category are you enriching over, exactly? im not sure i've worked with a standard category whose objects are sets equipped w/ PERs
sarahzrf (Apr 01 2020 at 14:29):the most obvious thing would be, i guess, functions which need to respect the PER, but what about the category where the morphisms don't need to be defined outside of the PER's set of reflexive elements?
sarahzrf (Apr 01 2020 at 14:29):^these are actual questions im asking, not me trying to poke holes
sarahzrf (Apr 01 2020 at 14:31):anyway, formalities aside, it seems to me that at this point you're basically subquotienting the category to get a different one, which looks just like a total language
sarahzrf (Apr 01 2020 at 14:32):but at that point you don't have fixed points anymore, so...
sarahzrf (Apr 01 2020 at 14:32):what was the topic of discussion again? :)
Stelios Tsampas (Apr 01 2020 at 14:33):sarahzrf said:
"treating it as an order-enriched category"—you mean placing the PER from that paper on the hom-sets?
Yeah, I left that quite hanging. And true, I'm making quite a few jumps ahead.
sarahzrf (Apr 01 2020 at 14:35):srsly tho, if the original point was "having fixed points and an initial object → trivial", but you can only recover an initial object by switching to fast-and-loose mode, then there's no point in switching to fast-and-loose mode for this, because the point of fast-and-loose mode is forgetting about the properties that let you have fixed points!
Stelios Tsampas (Apr 01 2020 at 14:36):I like to take (the ideal) haskell as the Kleisli category of the Maybe (or "lift" or "error" monad). The hom-sets of this category come with a partial order. So, by results in (https://arxiv.org/pdf/0710.2505.pdf), their initial and final coalgebras coincide.
sarahzrf (Apr 01 2020 at 14:40):that monad is only the same as Maybe classically >.>
sarahzrf (Apr 01 2020 at 14:40):ok im being pedantic
Stelios Tsampas (Apr 01 2020 at 14:41):I agree :)
Andrew Hirsch (Apr 01 2020 at 14:42):Stelios Tsampas said:
I like to take (the ideal) haskell as the Kleisli category of the Maybe (or "lift" or "error" monad). The hom-sets of this category come with a partial order. So, by results in (https://arxiv.org/pdf/0710.2505.pdf), their initial and final coalgebras coincide.
This forces Haskell to be strict, though. You need the monad on both inputs and outputs to deal with laziness.
Andrew Hirsch (Apr 01 2020 at 14:43):I mean, for a lot of programs, strictness versus laziness doesn't matter for correctness reasoning, as long as you're not dealing with infinite data structures.
Andrew Hirsch (Apr 01 2020 at 14:44):But OTOH, Haskell programs often deal with infinite data structures.
Dan Doel (Apr 01 2020 at 15:02):Haskell's initial and final coalgebras still coincide, though.
Dan Doel (Apr 01 2020 at 15:03):You need to use different domain-ish models, though. Not just flat domains.
Dan Doel (Apr 01 2020 at 15:05):Although the harder part, in my experience, is getting people to agree that e.g. ML's initial and final coalgebras coincide, which is also the case.
Alexander Kurz (Apr 01 2020 at 15:05):Is it known for which subset of Haskell, Haskell is a category? I am thinking of the discussion at http://math.andrej.com/2016/08/06/hask-is-not-a-category/ ... Is it enough to ban seq from Haskell?
Dan Doel (Apr 01 2020 at 15:06):I think if you get rid of seq it might be a category, but a lot of constructions do not behave nicely, still.
Dan Doel (Apr 01 2020 at 15:07):Like, pairs are not products.
Max New (Apr 01 2020 at 15:07):Can you observe that pairs are not products if you don't have seq though?
Dan Doel (Apr 01 2020 at 15:11):Yes, because pattern matching can tell the difference. You could fix that, too, but it's a separate thing.
Dan Doel (Apr 01 2020 at 15:11):Sums are not coproducts, also, and there's really no easy way to fix that.
Dan Doel (Apr 01 2020 at 15:13):For weird trivia, as I recall, in the predecessor to Haskell, Miranda, pattern matching couldn't tell the difference, but it also had seq to ruin it.
Verity Scheel (Apr 01 2020 at 15:17):I thought either sums were coproducts or pairs were products? i.e. you can’t have both, but you could have one (depending on strict vs non-strict).
Max New (Apr 01 2020 at 15:17):you can have both but Haskell has neither because it's non-strictness is different from call-by-name lambda calculus
Dan Doel (Apr 01 2020 at 15:18):You could have products, but it requires case analysis on products to be "irrefutable".
Dan Doel (Apr 01 2020 at 15:18):So case undefined of (_, _) -> 3 should evaluate to 3.
Max New (Apr 01 2020 at 15:19):it makes sense if you think of having to implement pattern matching using projections
Verity Scheel (Apr 01 2020 at 15:21):okay
Nathanael Arkor (Apr 01 2020 at 15:21):I was under the impression that seq was the obstruction to having a category and undefined was the obstruction to having nice structure; if you remove both, do you address the problems?
Reid Barton (Apr 01 2020 at 15:22):If you could remove undefined, you wouldn't have to remove seq :upside_down:
Dan Doel (Apr 01 2020 at 15:23):Do you mean undefined the named definition? Or get rid of its underlying meaning from the entire language?
Dan Doel (Apr 01 2020 at 15:23):The latter is a pretty significant change.
Verity Scheel (Apr 01 2020 at 15:24):I think we should be clear that bottom is not just undefined = undefined, but all other forms of non-termination, including arbitrary fixpoints.
Nathanael Arkor (Apr 01 2020 at 15:25):maybe the question I really wanted to ask was: is there a nice categorical semantics for a lazy call-by-need calculus similar to Haskell?
Nathanael Arkor (Apr 01 2020 at 15:25):because you can have nice categorical models of calculi with fixed points, so that's not an insurmountable problem
Nathanael Arkor (Apr 01 2020 at 15:26):(maybe this means you don't have cartesian closure in the strictess sense, but you do have some weaker notion)
Dan Doel (Apr 01 2020 at 15:29):Usually it is suggested that directed-complete partial orders are used. I think you could have Cartesian closure, but not coproducts.
Stelios Tsampas (Apr 01 2020 at 15:30):Andrew Hirsch said:
Stelios Tsampas said:
I like to take (the ideal) haskell as the Kleisli category of the Maybe (or "lift" or "error" monad). The hom-sets of this category come with a partial order. So, by results in (https://arxiv.org/pdf/0710.2505.pdf), their initial and final coalgebras coincide.
This forces Haskell to be strict, though. You need the monad on both inputs and outputs to deal with laziness.
Yessss, but I felt @Burak Emir's issue was more about correctness/intution rather than Haskell's evaluation strategy.
Verity Scheel (Apr 01 2020 at 15:31):... this all feels a little like logicians trying to work around Gödel: “but what if we get rid of this, but leave that?” :joy:
Stelios Tsampas (Apr 01 2020 at 15:38):Alas, poor logicians! But that's what Agda went for, right? Let's just write an imperfect but consistent termination checker and let's roll with it :).
Max New (Apr 01 2020 at 15:47):It's entirely possible to have a call-by-name typed lambda calculus with all fixed points that is cartesian closed (but no coproducts). Note that the difference between a call-by-name and a call-by-need language is not observable if your only effects are divergence and crash (which is what Haskell supports)
Stelios Tsampas (Apr 01 2020 at 15:53):Hey Max :). And how do coproducts break the category? Or maybe you can give a reference instead :).
Alexander Kurz (Apr 01 2020 at 15:56):It seems to me that those who understand all of Haskell and Category Theory and Semantics do have a pretty good idea of which subsets of Haskell have which categorical properties. What disturbs me, is that this knowledge seems not be laid out anywhere in a format that is accessible to a wider community.
Alexander Kurz (Apr 01 2020 at 15:59):Just reading through the comments here, suggests that there are lots of subtleties and secret knowledge but not a lot of hard mathematical results. For example, pairing not being product sounds strange to me.
Alexander Kurz (Apr 01 2020 at 16:00):How important is it to have undefined in Haskell? I have only written very little Haskell, but I don't remember the need of undefined.
Dan Doel (Apr 01 2020 at 16:00):If you want to get rid of undefined, you have to get rid of unrestricted general recursion.
Dan Doel (Apr 01 2020 at 16:01):Which is a huge change.
Max New (Apr 01 2020 at 16:01):the inconsistency with coproducts is explained in that Huwig-Poigne note mentioned above
Max New (Apr 01 2020 at 16:05):The results about lambda calculus are some of the oldest results in programming language semantics. I think Dana Scott's 1972 paper "Continuous Lattices" contains a model of typed lambda calculus with fixed points. These are perfectly "hard" mathematical results
Stelios Tsampas (Apr 01 2020 at 16:13):Dan Doel said:
If you want to get rid of undefined, you have to get rid of unrestricted general recursion.
I will take your word for it. But I would like to know why getting rid of unrestricted general recursion is problematic for an everyday Haskell programmer.
Burak Emir (Apr 01 2020 at 16:15):If every program terminates, then your language is no longer Turing complete. Now, that doesn't have to be a problem - in program verification, I think it is pretty standard to talk about "partial correctness" which is "correctness assuming that the program terminates".
Dan Doel (Apr 01 2020 at 16:15):How many programs have you written in Agda?
Burak Emir (Apr 01 2020 at 16:16):me? zero : )
Dan Doel (Apr 01 2020 at 16:16):No, Stelios.
Dan Doel (Apr 01 2020 at 16:16):Anyhow, that is the problem. Have the everyday Haskell programmer use Agda instead. :)
Stelios Tsampas (Apr 01 2020 at 16:16):I don't know, how many does one write after 2-3 years of usage?
Stelios Tsampas (Apr 01 2020 at 16:17):I personally would have 0 problems with that.
Dan Doel (Apr 01 2020 at 16:17):I don't know. I've been using it much longer than that, and I think I have 0 programs written.
Stelios Tsampas (Apr 01 2020 at 16:17):Haha OK, let's go by a 1000 programs then.
Stelios Tsampas (Apr 01 2020 at 16:19):I have a very, very hard time coming up with a program showcasing that lack of Turing completeness, or general recursion, is a detrimental thing.
Reid Barton (Apr 01 2020 at 16:19):Stelios Tsampas said:
Dan Doel said:
If you want to get rid of undefined, you have to get rid of unrestricted general recursion.
I will take your word for it. But I would like to know why getting rid of unrestricted general recursion is problematic for an everyday Haskell programmer.
You couldn't have both length and infinite lists--or at least the type accepted by length could not be the type of a list that is infinite. The language would just cease to be Haskell very quickly.
Dan Doel (Apr 01 2020 at 16:20):Like, there are all kinds of arbitrary annoyances in writing Agda programs in practice. You can't write map and fold separately a lot of the time, you have to write some combined thing so that the termination checker can see that it works.
Stelios Tsampas (Apr 01 2020 at 16:20):Hehe, you could have length and infinite lists. Just not length for infinite lists ;).
Dan Doel (Apr 01 2020 at 16:20):So it actively prevents you from factoring your code in arbitrary useful ways.
Dan Doel (Apr 01 2020 at 16:22):You can (maybe) do better by using sized types, but then you have to plan ahead with everything or spend a lot of time adding them once you need them, and there's extra clutter.
Dan Doel (Apr 01 2020 at 16:23):Anyhow, the point is, there's no real language for doing this.
Dan Doel (Apr 01 2020 at 16:23):There are only toys.
Stelios Tsampas (Apr 01 2020 at 16:23):This isn't about Agda specifically, right? And I don't see how general recursion is what prevents these problems from being solved in Agda.
Reid Barton (Apr 01 2020 at 16:23):Even if there was such a language it would no longer be Haskell and so by definition its users would not be Haskell programmers.
Dan Doel (Apr 01 2020 at 16:23):Yeah, that too.
Burak Emir (Apr 01 2020 at 16:24):In other words: the trouble with getting rid of non-termination in any language is not so much that one wants to write non-terminating programs, but that one doesn't want to be restricted to a general enough language where termination can be automatically checked and ensured. Those checks comes with constraints, hoops to jump through or simply limitations on what you can do (and a good part of Haskell programmers wants to violently argue that it is just BETTER AT EVERYTHING while being Turing complete... so it would clash with that).
Dan Doel (Apr 01 2020 at 16:25):Yeah. I don't think you can't get close enough to work in a total language. But we're not there yet. It's an open research problem.
Burak Emir (Apr 01 2020 at 16:26):That's why I find that paper valuable; I believe the beautiful Lambek & Scott style CCC for a given simply-typed calculus does not go near fixpoints and non-termination.
Burak Emir (Apr 01 2020 at 16:27):... and I'd love if more people were aware of this. The denotational semantics with dcpo is something very different from the "objects are types".
Andrew Hirsch (Apr 01 2020 at 16:30):If you're at all concerned with real-world programming, you most emphatically want nonterminating programs. In particular, you want to allow servers, drivers, and a lot of other real-world code which runs a polling loop. For a simple web server, it checks the queue of requests and, if there's a head, pops it and responds to it. Otherwise, it just loops.
Andrew Hirsch (Apr 01 2020 at 16:31):If we're interested in giving semantics to real-world programs (which I am), we have to be able to talk about that server
Stelios Tsampas (Apr 01 2020 at 16:35):That is a good point. I can imagine a monad-based approach where notions of well-foundedness are lifted in a real-world setting such as this. For example, you can have an event system where the server runs in the backgorund but each event handler is a well-founded, terminating program.
Andrew Hirsch (Apr 01 2020 at 16:37):Right, a lot of the work in the FP community is in making real-world programs have nice mathematical structure like this. But that's a non-trivial refactoring of the program that a real-world Haskell programmer would write!
Gershom (Apr 01 2020 at 16:37):We should be careful not to fall into the trap that Conor McBride often warns about here. You _can_ write potentially nonterminating stuff in Agda and the like, you just have to be explicit about the _manner_ in which it doesn't terminate. There are a number of techniques for this sort of thing, which I won't go through. And for certainly nonterminating stuff, there's definitely plenty of work on "coinduction" in proof assistants and techniques for handling coinductive types. The problem isn't "you can't write nonterminating stuff" its "when you write terminating stuff, you need to do so in a way that lets the termination checker see it terminates, and when you write certainly coinductive stuff, you need to be able to do so in a way that it can be checked to be productive (i.e. provably continue to produce output)" etc
Gershom (Apr 01 2020 at 16:38):But all this stuff about Agda is a distraction from the difficulty of writing "in the total fragment of Haskell" which is what "categorists' informal Hask" is.
Burak Emir (Apr 01 2020 at 16:42):Yeah, if it were widely known that "categorists' informal Hask" is terminating, thus does not have general recursion and fixpoint combinators, this would certainly be a better state of affairs. If one wants to capture partial computation, the constructions needed are very different and it also has not much to do with the type theory / logic correspondence anymore.
Gershom (Apr 01 2020 at 16:42):As far as I know, producing models that are not just categorical but "nice" to category theorists of languages which are best modeled by domain theory (i.e. which can embed the untyped lambda calculus) remains an open research question, and it was one of the goals of the various sorts of synthetic and extended and axiomatic domain theories produced throughout the 80s. What you got (I believe, but I'm not an expert) was a lot of things which were categorically nice, and had some sort of nontermination, but didn't correspond to the way we want to compute. Scott's equilogical spaces are a favorite of mine in that regard.
Burak Emir (Apr 01 2020 at 16:44):Yes, there was a survey... let me dig it out. Dwight Spencer. A survey of categorical computation : fixed points, partiality, combinators, ... control? (edit: grammar)
Burak Emir (Apr 01 2020 at 16:47):That is where I got the Huwig Poigne reference from. Theorem 2.1 [HP86] A cartesian closed category with fixed points collapses to the trivial category 1 if it contains any of the following:
an initial object
a boolean algebra (coproduct) object, 2 (= 1 + 1)
equalizers for any pair of morphisms
a natural number object (NNO)
Dan Doel (Apr 01 2020 at 16:50):I don't think it makes sense to just write off any connection between type theory and logic and partial computation.
Gershom (Apr 01 2020 at 16:51):Ah, yes, let me add there are some purely categorical models for handling partiality and nontermination, but for reasons I don't recall, they're good settings for _studying_ such things or _representing_ such things, and more generally for considering computability, but not for "programming languages taking semantics in." One is the line of work on "realizability toposes" which starts with hyland's effective topos and builds off of taking semantics in PCAs. The other is more recent work by Cockett & co. on "Turing categories" which starts with a categorification of the idea of partial maps in terms of "restriction categories".
Burak Emir (Apr 01 2020 at 16:52):PCA?
Gershom (Apr 01 2020 at 16:52):Partial Combinatory Algebras.
I've asked some experts to explain to me the tradeoffs and differences between the above approaches a few times, but I'm afraid I've forgotten the details. I do recall that they really do look at "different levels" of the structure and so they aren't competing to do the same thing at all.
Dan Doel (Apr 01 2020 at 16:53):For an example for earlier, though: there is a typical 4 line quicksort example on lists in Haskell used as an intro for newbies. And there is also an entire research paper by Conor McBride showing how to write the same example in a way so that a structural recursion checker would accept it.
Burak Emir (Apr 01 2020 at 16:54):@Dan Doel I would agree, I personally justify to myself all the spare time that I sunk into type theory and logic that at the very least it would help create "pockets/islands of correctness" : ) I think a good deal of purely functional programming can serve as examples how to quickly and easily get correctness (I am not convinced that that extends to all Haskell).
Dan Doel (Apr 01 2020 at 16:56):There are probably better approaches than that paper, but it's not uncommon for people to write things in a way that is non-trivial to justify fully.
Burak Emir (Apr 01 2020 at 17:06):So Hask , the informal category of Haskell types, has
where terms do not involve fixpoint operates and thus cannot express general recursion.
It also doesn't explain the System F part, aka the polymorphic calculus.
We somehow adding an object Foo[A] for every type A that satisfies the constraints.
That then makes Hask not very Haskell specific (would work for any System F calculus).
Gershom (Apr 01 2020 at 17:13):People will usually try to call that "total Hask" or something, to indicate that they're aware of the issues. But also people can be very sloppy. There's also various richer models using fibers or indexing, pursued by Ghani, Johann, and others, which can handle indexed and non-regular types, etc.
Dan Doel (Apr 01 2020 at 17:13):I don't think you can throw out all fixpoints.
Dan Doel (Apr 01 2020 at 17:14):The point of the 'fast and loose' stuff is basically that you can imagine you're working with something like System F and reason well enough for practical purposes, though.
Gershom (Apr 01 2020 at 17:15):Good point dan, we still need some form of total recursion otherwise we can't like induct over a list...
Burak Emir (Apr 01 2020 at 17:15):Fold constants for every recursive data type?
Dan Doel (Apr 01 2020 at 17:25):I'm not sure it makes sense to try to define a syntactic thing for what people mean informally by "Hask".
Dan Doel (Apr 01 2020 at 17:28):I think people are often thinking about some informal semantics of the terms.
Dan Doel (Apr 01 2020 at 17:32):The purpose of the terms is to present the morphisms, not be them.
Burak Emir (Apr 01 2020 at 17:44):I thought the reason of being for Hask was that people want to grasp CT : )
Stelios Tsampas (Apr 01 2020 at 17:55):Dan Doel said:
The point of the 'fast and loose' stuff is basically that you can imagine you're working with something like System F and reason well enough for practical purposes, though.
There it is :).
Stelios Tsampas (Apr 01 2020 at 17:58):@Burak Emir I'd say it's quite the opposite.
Burak Emir (Apr 01 2020 at 18:00):Please explain - people do not want to grasp CT that is why there is Hask? :wink:
Stelios Tsampas (Apr 01 2020 at 18:02):I would say the motivation is to have a consistent, attractive, usable categorical framework that characterizes Haskell. Above all, it complements Haskell :).
Stelios Tsampas (Apr 01 2020 at 18:03):So it's CT for Haskell, not Haskell used to understand CT.
Stelios Tsampas (Apr 01 2020 at 18:04):Of course, anyone can have their own motivation for Hask. So I am expressing a (possible, I might be wrong) general sentiment, which I'm guessing you did as well. Don't let that discourage you from using Hask your way.
Burak Emir (Apr 01 2020 at 18:04):That is what I meant, too. Lots of folks who start with Haskell, then get curious about all cats.
Dan Doel (Apr 01 2020 at 18:05):Yeah, to some degree, what you come up with will depend on your goals.
Dan Doel (Apr 01 2020 at 18:07):So, for instance, complaints that "Hask isn't a category" don't make sense from the perspective, not of getting a rigorous categorical semantics of Haskell, but using Haskell as a close enough language to describe the actual content of categorical constructions.
Burak Emir (Apr 01 2020 at 18:08):Agree. I personally have not dealt with much Haskell for practical purposes, but enough exposure to PL theory. So I appreciate the Lambek & Scott route to CCC a lot more... Call it "from a pedagogical perspective"
Burak Emir (Apr 01 2020 at 18:08):And maybe cartesian closed multi categories would be even better.
Dan Doel (Apr 01 2020 at 18:09):Haskell is something you can type into a computer and have it show you results, and it's close enough to something with actual categorical semantics that the difference doesn't matter for just fooling around with stuff.
Dan Doel (Apr 01 2020 at 18:10):And you can see how the Yoneda lemma actually works, even if technically it doesn't exactly work.
Burak Emir (Apr 01 2020 at 18:10):Yes, I must admit it's pretty unique in that way.
Dan Doel (Apr 01 2020 at 18:11):You can also go backwards along that.
Dan Doel (Apr 01 2020 at 18:11):Some categorical facts map back into Haskell in ways that don't quite line up, but the difference doesn't really matter.
Dan Doel (Apr 01 2020 at 18:14):And if someone worked out all the gory details on a technically correct specification of what structure it actually is, it probably wouldn't make any difference to people just borrowing the close-enough ideas.