08:03 <dborisog> Could you please share examples of a good functional code with a strong resemblance to category theory? -- e.g. polymorphic datatypes or functions as functors or natural transformations, correspondigly.

09:30 <porchetta> what does merlin use to compute the type of a symbol?

09:30 <porchetta> Is there a library that allows me to accomplish the same?

11:00 <kvik> porchetta: could be ocamlc -annot, or -bin-annot

11:43 <octachron> Merlin uses the compiler library directly.

13:42 <companion_cube> dborisog: what's the point of that? :p

13:46 <dborisog> Going through good code is a great learning tool, yet I do not trust my judgement to differentiate good code from bad code and pay attention to the former while discarding latter.

13:46 <companion_cube> right, but resemblance to category theory isn't related to good code :)

13:48 <dborisog> I am partially familiar with a powerful application of Bourbaki's mathematical structures for conceptual analysis and synthesis, and it seems it is applicable to datatype aspect of design if usef in software engineering.

13:50 <simpson> It sounds like an aesthetic question. Any lambda calculus will be tightly related to category theory automatically, and there exist hypergraph databases written by folks who either don't know or don't care that hypergraphs and categories are extremely similar structures.

13:51 <dborisog> Bourbaki's structures are based on 'internal' view of structures of objects, while category theory is based on 'external' view. It reminds me of the notion of functions, thus I do not exclude a possibility that a similarly powerful thinking tool could be created from category theory.

13:52 <companion_cube> to be frank, OCaml code is not purely functional code, and types are only an approximation of what the program does.

13:53 <companion_cube> software engineering really isn't CT, except maybe in some esoteric Haskell circles

13:53 <dborisog> Thus, answering your question, companion_cube, I would like to have examples of good code I can associate to categorical concepts.

13:53 <simpson> Also, to be frank from the other side, category theory is a descriptive tool for unifying concepts, not a prescriptive tool for design guidelines. (Other than the meta-pattern of "if it looks like a generic algebraic signature, then maybe it's an algebraic object")

13:54 <companion_cube> (tbh I never groked CT)

13:54 <simpson> dborisog: Maybe http://tunes.org/~iepos/joy.html would be a fun read, describing the internals of Turing categories https://golem.ph.utexas.edu/category/2019/08/turing_categories.html

13:54 <companion_cube> dborisog: if you want to see good functional APIs, maybe look at `cmdliner`? it's an applicative argument parser

13:55 <dborisog> companion_cube: unless you know Russian I cannot provide reference materials about application of Bourbaki's structures for conceptual analysis and synthesis. It is based on similarly abstract math yet it is very powerful tool.

13:55 <simpson> (I grok CT, mostly to cut through Haskeller memes but also because I wanted to be sure it wasn't really a magic panacea.)

13:55 <companion_cube> simpson: good for you :D

13:55 <companion_cube> I stick to simple algebra and logic

13:55 <dborisog> thank you

13:56 <simpson> companion_cube: I wish. It seems mostly just to bring me onto the losing sides of arguments on the Internet~

13:56 <companion_cube> heh at least you get the intellectual honesty

13:58 <simpson> And that's its own reward. Right now, being honest and open lets me study OCaml, and dash pointed me to https://caml.inria.fr/pub/docs/manual-ocaml/bindingops.html which seems like a very cool and borrowable idea.

14:19 <dborisog> In general, looking at source like https://github.com/statebox/awesome-applied-ct or books by Spivak, applied category theory is a very young discipline.

14:22 <porchetta> octachron, kvik: thanks

15:37 <notnotdan> dborisog: right, but "applied category theory" is not the same thing as programming patterns inspired by CT

15:45 <dborisog> In my understanding, "applied category theory" is a category theory applied to a knowledge domain, in other words, used for representation of knowledge and tools of this knowledge domain. Within this schema, category-theory-for-programming is an element or a subset of elements of applied category theory.

15:47 <simpson> Understandable. What makes this tough is that programming can be looked at as an application of linguistics and mathematics to a knowledge domain. So the category-theoretic concepts are everywhere: In parsers and compilers and data transformations.

15:47 <dborisog> I yet to think through the following example to something appliecable, but if I would design an information system that works with (chicken) eggs, I could use the categorical concept Product for representation of an egg with its yolk and whites.

15:48 <companion_cube> simpson: but how often does that bring you actual useful things?

15:49 <dborisog> An egg becomes a semantically rich algebraic data structure. I do not know what to do with it yet ( :D ), but it is an example of a construct that is native to OCaml.

15:52 <dash> dborisog: i assume you're talking about http://wiki.call-cc.org/eggs

15:53 <simpson> companion_cube: I'm not sure; there's a lot of possible things and I haven't tried many of them yet. Monoids seem *unbelievably* useful. Groups show up in cryptography. The rest, meh, yeah, it's all case-by-case and hit-or-miss.

15:54 <companion_cube> monoids are useful, but hardly need CT

15:54 <companion_cube> it's such a simple algebraic structure

15:54 <dborisog> dash: no, I have a diagram for it, but not sure how can I share it here )

15:56 <dborisog> dash: here it is https://drive.google.com/open?id=1MY9wLxqyXr-AVQZSIdgN7zhIQPF4o2dK :D

15:57 <dash> well, the ologs paper talks about spiderwebs, right

15:57 <dash> i guess eggs are just as fair a target

15:59 <dborisog> dash: originally, I created a Russian version with funny names of functions like "squeeze the yolk" )

16:03 <dborisog> companion_cube: in my current "understanding", CT becomes a useful to software engineering if one starts thinking categories at the end designing concise and semantically rich data types operated by a polymorphic functions -- the minimum number of functions to fully process a holistic software for a knowledge domain.

16:04 <notnotdan> dborisog: it's just that the phrase 'Applied Category Theory' refers to a specific strain of research

16:04 <notnotdan> to be honest i am still not sure what are you looking for

16:06 <notnotdan> it's hard for me to judge what you are talking about but have you looked at Curry-Howard correspondence for example? or categorical semantics of programmign languages in general?

16:11 <dborisog> notnotdan: I read about Curry-Howard (and Lambek, for category theory) isomorphis yet I need a considerable way to go for it to become native to me. As for the thing I want to do with CT...

16:13 <dborisog> Using an egg analogy, the following two URLs contain a detailed nutritional information for a whole raw egg ( https://nutritiondata.self.com/facts/dairy-and-egg-products/111/2 ) and raw egg yolk ( https://nutritiondata.self.com/facts/dairy-and-egg-products/113/2 ).

16:19 <dborisog> It has several groups of descriptors, and if you would look at fats & fatty acids section, you'll see that another few levels of hierarchy. egg--fats--monosaturated--14:01; as well as aggregators like "total trans fatty acids". If I would to design and develop software for USDA (the source of this data), I would like to write a minimal number of functions possible, so if needed, I can logically proove that functions have no errors in design and

16:19 <dborisog> implementations. For example, use the same function to count the volume of 14:01 per one egg, total fast per one egg, total vitamin A per ten yolks.

16:19 <dborisog> Or compare a chicken egg to duck egg for a fatty acid, stuff like that.

21:47 <GeoffK> A one liner, what am i missing?

21:48 <GeoffK> open_out_gen [Open_text;Open_append;Open_creat] 644 "a.txt" |> close_out;;

21:48 <GeoffK> file perms i get: --w----r-T

21:50 <companion_cube> 0o644 ?

21:50 <GeoffK> ah

21:51 <GeoffK> yep, much appreciated.

21:51 <dash> GeoffK: 644 probably not what you want :)

21:51 <dash> yeah that

21:51 <GeoffK> whys that dash?

21:52 <dash> because it's not 0o644

21:52 <GeoffK> totally agreed