Logs: freenode/#haskell
| 2021-04-14 21:04:17 | → | usr25 joins (~usr25@unaffiliated/usr25) |
| 2021-04-14 21:06:12 | × | hyperisco quits (~hyperisco@d192-186-117-226.static.comm.cgocable.net) (Ping timeout: 240 seconds) |
| 2021-04-14 21:06:14 | × | LKoen quits (~LKoen@65.250.88.92.rev.sfr.net) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 2021-04-14 21:07:42 | × | Alleria__ quits (~textual@mskresolve-a.mskcc.org) (Ping timeout: 265 seconds) |
| 2021-04-14 21:08:36 | <nicholasbulka> | I like the idea of natural transformations as analogies |
| 2021-04-14 21:10:25 | × | heatsink quits (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-04-14 21:10:36 | <nicholasbulka> | I've done a lot of self teaching over the years and I want to write down some of the techniques into a meta-learning book. Category theory seems like the best framework for something like that but the challenge seems to be how to make it accessible. |
| 2021-04-14 21:13:49 | → | dinciorip joins (~dincio@5.170.25.42) |
| 2021-04-14 21:16:23 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 2021-04-14 21:16:25 | → | chenshen joins (~chenshen@2620:10d:c090:400::5:b29e) |
| 2021-04-14 21:17:06 | × | slack1256 quits (~slack1256@191.113.234.51) (Remote host closed the connection) |
| 2021-04-14 21:18:37 | → | hololeap joins (~hololeap@gateway/tor-sasl/hololeap) |
| 2021-04-14 21:19:29 | <ski> | nicholasbulka : hm, so here goes (somewhat longish) |
| 2021-04-14 21:19:43 | <ski> | <OP> I'm just trying to vaguely make sense of category theory since I have been doing a bit of OCaml lately. I haven't been to uni since a very long time <ski> OP : ooc, what CT stuff ? <OP> ski: well, how it relates to the category of OCaml objects. Morphisms, the definition of purity, functors. Basically trying to code with more idiomatic patterns. I took a bit of a bottom-up approach. |
| 2021-04-14 21:19:57 | × | rj quits (~x@gateway/tor-sasl/rj) (Ping timeout: 240 seconds) |
| 2021-04-14 21:19:59 | <ski> | <someone> in the algebraic topology course im doing, this lecturer occasionally likes to use a little too much category theory for my liking, and i do like category theory in general but I feel like it obfuscates from the geometric arguments which one should learn too :/ <someoneelse> syntactic arguments are always better! * someoneelse runs <someone> i think it is important to formalize intuition of |
| 2021-04-14 21:20:05 | <ski> | course |
| 2021-04-14 21:20:17 | <ski> | <someoneelse> intuition is the fastest way of symbol manipulation, nothing else <someone> not denying that one should be able to write down a formal proof of something if required * someoneelse runs even faster <someoneelse> (just kidding) <ski> someoneelse,someone,OP : anyway, "properties, structure, stuff" is vaguely relevant |
| 2021-04-14 21:20:30 | <ski> | <OP> ski: well i certainly deal with stuff on a day to day basis. But I got what I came here for :D <OP> Any advice on an intro book on category theory? <someoneelse> ncatlab <someoneelse> it's not an intro, but outro |
| 2021-04-14 21:20:42 | <ski> | <ski> OP : hm, i see. perhaps reading about a monadic approach to side-effects, and how that relates to Kleisli categories could be relevant. (and perhaps Andrzej Filinski's "Representing Monads" paper, which can embed any monadic effect as a side-effect, given delimited continuations. see <http://hjemmesider.diku.dk/~andrzej/papers/>) <OP> its surely sounds relevant <OP> ok I'll look it up thanks a lot |
| 2021-04-14 21:20:56 | → | CrazyPython joins (~crazypyth@98.122.164.118) |
| 2021-04-14 21:20:59 | <ski> | <ski> well. my recommendation would be "Conceptual Mathematics: A first introduction to categories" by William ("Bill") F. Lawvere and Steven Schanuel <yetanother> you might consider Goldblatt's Topoi <OP> yes the Goldblatt looks really interesting <OP> oh well, next pay, next month. Thanks a lot. Very helpful |
| 2021-04-14 21:21:10 | <ski> | <ski> there's also a few books that relate a bit more to CS. like "Basic Category Theory for Computer Scientists" by Benjamin Pierce,"Categories, types, structures - An introduction to category theory for the working computer scientist" by Andrea Asperti,Guiseppe Longo in 1991 at <https://www.di.ens.fr/users/longo/files/CategTypesStructures/book.pdf>,"Categories and Computer Science" by R. F. Walters in |
| 2021-04-14 21:21:24 | <ski> | <ski> 1992,"Computational Category Theory" by D. E. Rydeheard,R. M. Burstall in 2001 at <http://www.cs.man.ac.uk/~david/categories/book/book.pdf>,<http://www.cs.man.ac.uk/~david/categories/> |
| 2021-04-14 21:21:35 | <ski> | <yetanother> Goldblatt is quite interesting, and offers pretty clear intro to categories and Topoi. There are some weaker parts concerning sheaves which might be supplemented . The book is cheap (Dover) IIRC. Well suited for those with an interest an foundations |
| 2021-04-14 21:21:52 | <ski> | <OP> yeah i was trying to shy away from less conceptual resources. I mean, there are already tons of resource for that online. I already know what a monad is in Haskell for practical purpose. I don't know, this category theory somehow piqued my interest. <yetanother> ski: don't forget Arbib and Manes <ski> 'sat a book ? haven't seen it <yetanother> I like Awodey and also Riehl quite a bit. |
| 2021-04-14 21:22:06 | <ski> | <yetanother> Yeah, one of the older CS related CT books <ski> yea, i was just about to mention Awodey <yetanother> Awodey's Oregon videos also quite good https://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html |
| 2021-04-14 21:22:21 | <ski> | * ski . o O ( "Seven Sketches in Compositionality - An Invitation to Applied Category Theory" by Brendan Fong,David I. Spivak in - 2018-10-12 at <https://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf>,<https://math.mit.edu/~dspivak/teaching/sp18/> ) <yetanother> OP: some haskell folks like Bartosz Milewski |
| 2021-04-14 21:22:31 | <ski> | * ski . o O ( "Toposes, Triples and Theories" by Michael Barr,Charles Wells in 2000 at <https://www.math.mcgill.ca/barr/papers/ttt.pdf> ; "Elementary Categories, Elementary Toposes" by Colin McLart in 1992 ) <yetanother> Hardly an intro <yetanother> (Bar) <OP> yetanother: yes I have watched these but he is a bit slow and the recording is bad (I am a bit of a princess at times) |
| 2021-04-14 21:22:42 | <ski> | <ski> yea, right, that's "Category Theory for Programmers" by Bartosz Milewski in 2018-10-21 at <https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/>,<https://github.com/hmemcpy/milewski-ctfp-pdf>. he also has some YouTube videos, talking about categorical stuff, as it applies to programming <ski> yetanother : yea, i didn't mean to imply it was .. just i was reminded of it |
| 2021-04-14 21:22:58 | <ski> | <OP> Honnestly I think I'll get the Goldblatt as a basis and go venture from there. <yetanother> Harper's "Trinity" ideas also interesting https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ |
| 2021-04-14 21:23:09 | <ski> | <OP> sadly my education in math comes from a degree in macroeconomics. The kind of things that does not really help you grow an interest in maths. I guess I'll go the uni again one day. I've heard my local uni isn't so bad, I'm in Paris. <ski> someoneelse : hehe, i was just reading the other day, Dijkstra expounding upon the virtues of "letting the symbols do the work" :) |
| 2021-04-14 21:23:24 | <ski> | <ski> OP : oh. also notice that the concept of (module) functors in the MLs is probably not that close to the CT one * ski . o O ( "On Functors" (in C++,Standard ML,Haskell,Prolog) by Peteris Krumins in 2010-05-17 at <http://www.catonmat.net/blog/on-functors/> ) <OP> well I sort of disagree, in Prolog, we call that a law or an operation. |
| 2021-04-14 21:23:31 | <ski> | <ski> yetanother : Lambek & Scott has some interesting comments about a potential reconciliation between platonism, formalism, intuitionism, in their "Introduction to Higher Order Categorical Logic" in 1986 .. <OP> meh, nominalism is everywhere in math :D <ski> iiuc, the Prolog term comes from logic, and possibly philosophy (of language. maybe Carnap ?) |
| 2021-04-14 21:23:44 | <ski> | <yetanother> Ski: it's on my shelf, but I need to fill in some more background first <ski> OP : elaborate ? * ski . o O ( <https://en.wikipedia.org/wiki/Elasticity_of_demand> ) <OP> oh he refers to the builtin. I thought he only refered to the first atom <OP> just a quibble <OP> but yes I agree, the terminology in cs seems rather vague |
| 2021-04-14 21:23:57 | <ski> | <OP> I'd say daunting at first when you try to learn many languages. At the end of the day, most people seem to remain in their enclosed religion. I mostly do ML for fun. Erlang for the money. <OP> but I got the gist of it, Haskell is closer to the terminology in use in math books |
| 2021-04-14 21:24:08 | <ski> | * ski had some vague ideas how that could possibly be related to derivatives of data structures <http://strictlypositive.org/diff.pdf>, combinatorial species <https://byorgey.wordpress.com/category/species/>, naperian containers <https://web.archive.org/web/20161104231529/http://sneezy.cs.nott.ac.uk/containers/blog/> |
| 2021-04-14 21:24:19 | <ski> | <OP> all right, back to studying thanks again everyone. I guess I'll come hang around here in a few days. See you. |
| 2021-04-14 21:24:22 | → | rj joins (~x@gateway/tor-sasl/rj) |
| 2021-04-14 21:24:33 | <nicholasbulka> | this is great, thank you! |
| 2021-04-14 21:24:35 | <ski> | * ski . o O ( "Society's role in mathematics" in 1998-11-21 at <https://www.cs.utexas.edu/users/EWD/transcriptions/EWD12xx/EWD1277.html>,"How Computing Science created a new mathematical style" in 1990-04-04 at <https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1073.html>,"Under the spell of Leibniz's Dream" in 2000-04-20 at |
| 2021-04-14 21:24:43 | <ski> | * ski <https://www.cs.utexas.edu/users/EWD/transcriptions/EWD12xx/EWD1298.html>, all by Edsger Wybe Dijkstra ) <ski> OP : to close with, i think the Lawvere & Schanuel book may be the easiest one to start with, for one without that much math experience. take care and have fun ! |
| 2021-04-14 21:24:47 | <ski> | (done) |
| 2021-04-14 21:25:03 | × | nicholasbulka quits (~nicholasb@2601:900:4301:da0:447b:5128:d97:8340) (Remote host closed the connection) |
| 2021-04-14 21:25:18 | <ski> | (hm, that was a bit longer than i thought. .. anyway, i thought some of the surrounding discussion could possibly also be of interest) |
| 2021-04-14 21:25:57 | → | nighmi joins (~felix@port-92-196-72-29.dynamic.as20676.net) |
| 2021-04-14 21:26:26 | → | pthariensflame joins (~pthariens@2600:6c52:727f:4200:5cd6:67f8:fcfa:33ac) |
| 2021-04-14 21:29:21 | × | pthariensflame quits (~pthariens@2600:6c52:727f:4200:5cd6:67f8:fcfa:33ac) (Client Quit) |
| 2021-04-14 21:30:13 | × | s00pcan quits (~chris@107.181.165.217) (Ping timeout: 240 seconds) |
| 2021-04-14 21:32:23 | × | remby quits (~remby@bras-base-london1483w-grc-43-65-95-173-128.dsl.bell.ca) (Quit: Leaving) |
| 2021-04-14 21:32:30 | → | s00pcan joins (~chris@075-133-056-178.res.spectrum.com) |
| 2021-04-14 21:32:49 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 252 seconds) |
| 2021-04-14 21:37:17 | × | s00pcan quits (~chris@075-133-056-178.res.spectrum.com) (Read error: Connection reset by peer) |
| 2021-04-14 21:38:36 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-04-14 21:40:05 | → | acidjnk_new joins (~acidjnk@p200300d0c72b9573c48ebca42f820036.dip0.t-ipconnect.de) |
| 2021-04-14 21:42:18 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Ping timeout: 240 seconds) |
| 2021-04-14 21:42:40 | → | s00pcan joins (~chris@075-133-056-178.res.spectrum.com) |
| 2021-04-14 21:43:15 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:e26e:cf9:1dd6:9615) (Ping timeout: 248 seconds) |
| 2021-04-14 21:43:19 | → | ericsagnes joins (~ericsagne@2405:6580:0:5100:3be6:c7d7:e232:14d0) |
| 2021-04-14 21:43:28 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 2021-04-14 21:44:01 | → | idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-04-14 21:44:14 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-04-14 21:45:41 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-04-14 21:48:18 | → | Tom19 joins (b2115c11@92-17.net.optinet.cz) |
| 2021-04-14 21:48:35 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 250 seconds) |
| 2021-04-14 21:48:44 | → | kristijonas joins (~kristijon@78-56-32-39.static.zebra.lt) |
| 2021-04-14 21:49:09 | × | mikoto-chan quits (~anass@gateway/tor-sasl/mikoto-chan) (Ping timeout: 240 seconds) |
| 2021-04-14 21:50:21 | × | __monty__ quits (~toonn@unaffiliated/toonn) (Quit: leaving) |
| 2021-04-14 21:52:23 | × | PyroLagus quits (PyroLagus@i.have.ipv6.on.coding4coffee.org) (Quit: ZNC / WeeChat) |
| 2021-04-14 21:52:31 | × | dxld quits (~dxld@rush.pub.dxld.at) (Remote host closed the connection) |
| 2021-04-14 21:52:43 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:3be6:c7d7:e232:14d0) (Ping timeout: 258 seconds) |
| 2021-04-14 21:52:45 | → | PyroLagus joins (PyroLagus@i.have.ipv6.on.coding4coffee.org) |
| 2021-04-14 21:53:08 | → | dxld joins (~dxld@rush.pub.dxld.at) |
| 2021-04-14 21:54:17 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 2021-04-14 21:54:31 | × | bwe_ quits (~bwe@2a01:4f8:1c1c:4878::2) (Ping timeout: 245 seconds) |
| 2021-04-14 21:54:39 | → | bwe joins (~bwe@unaffiliated/bwe) |
| 2021-04-14 21:55:01 | × | xff0x quits (~xff0x@2001:1a81:53de:e800:d3b4:413a:5958:6939) (Ping timeout: 258 seconds) |
| 2021-04-14 21:55:01 | × | i7c quits (UzrQ2PKvmb@unaffiliated/i7c) (Ping timeout: 258 seconds) |
| 2021-04-14 21:55:33 | → | xff0x joins (~xff0x@2001:1a81:53de:e800:d3b4:413a:5958:6939) |
| 2021-04-14 21:56:24 | × | coot quits (~coot@37.30.50.130.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 2021-04-14 21:56:50 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-14 21:56:52 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 240 seconds) |
| 2021-04-14 21:57:21 | × | Pickchea quits (~private@unaffiliated/pickchea) (Quit: Leaving) |
| 2021-04-14 21:58:07 | × | Sorna quits (~Sornaensi@077213203030.dynamic.telenor.dk) (Ping timeout: 252 seconds) |
| 2021-04-14 21:58:40 | × | haskellstudent quits (~quassel@213-225-6-101.nat.highway.a1.net) (Ping timeout: 252 seconds) |
| 2021-04-14 21:58:43 | × | Tom19 quits (b2115c11@92-17.net.optinet.cz) (Ping timeout: 240 seconds) |
| 2021-04-14 21:59:00 | ← | michalz parts (~user@185.246.204.61) ("Changed major mode") |
| 2021-04-14 22:00:32 | × | dinciorip quits (~dincio@5.170.25.42) (Quit: WeeChat 3.1) |
| 2021-04-14 22:01:39 | × | L29Ah quits (~L29Ah@unaffiliated/l29ah) (Ping timeout: 245 seconds) |
| 2021-04-14 22:04:29 | → | ericsagnes joins (~ericsagne@2405:6580:0:5100:1b7c:b2ef:9111:71fe) |
| 2021-04-14 22:04:43 | × | malumore_ quits (~malumore@151.62.114.211) (Remote host closed the connection) |
| 2021-04-14 22:04:46 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Read error: Connection reset by peer) |
| 2021-04-14 22:04:53 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 2021-04-14 22:06:24 | → | nicholasbulka joins (~nicholasb@2601:900:4301:da0:447b:5128:d97:8340) |
| 2021-04-14 22:06:35 | <nicholasbulka> | ski thanks again |
| 2021-04-14 22:06:58 | <ski> | np |
| 2021-04-14 22:09:01 | × | Tario quits (~Tario@201.192.165.173) (Ping timeout: 260 seconds) |
| 2021-04-14 22:09:32 | → | Tario joins (~Tario@201.192.165.173) |
| 2021-04-14 22:09:49 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:1b7c:b2ef:9111:71fe) (Ping timeout: 250 seconds) |
| 2021-04-14 22:10:59 | → | heatsink joins (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
All times are in UTC.