Logs: liberachat/#haskell
| 2021-05-27 07:56:07 | × | oxide quits (~lambda@user/oxide) (Ping timeout: 244 seconds) |
| 2021-05-27 07:56:11 | <kakuhen> | I see |
| 2021-05-27 07:56:12 | <joel135> | It would be cool to implement an actual category called Hask in agda somehow, and then somehow use it to talk to a haskell process. |
| 2021-05-27 07:56:42 | <kakuhen> | My interpretation of Bauer's argument was mostly "with the current handwavy definition, we can't even check off all the axioms of a category, and the following proposed solutions still have issues." |
| 2021-05-27 07:58:05 | → | haskman joins (~haskman@223.190.83.69) |
| 2021-05-27 07:58:14 | → | oxide joins (~lambda@user/oxide) |
| 2021-05-27 07:58:18 | dy | is now known as pissnet |
| 2021-05-27 07:58:23 | <joel135> | Perhaps one could cook up an adjunction between Hask and Set or something. |
| 2021-05-27 07:58:24 | pissnet | is now known as dy |
| 2021-05-27 07:59:01 | <dminuoso> | kakuhen: No, its not that we cant prove it, it's that nobody has defined it. |
| 2021-05-27 08:00:13 | <dminuoso> | kakuhen: If you dont specify what `f x = g x` even means, you cant check whether its correct. |
| 2021-05-27 08:00:50 | <kakuhen> | right, nobody has defined Hask so that it *is* a category |
| 2021-05-27 08:00:52 | → | ubert joins (~Thunderbi@p200300ecdf259d7974882ed522245916.dip0.t-ipconnect.de) |
| 2021-05-27 08:00:55 | → | michalz joins (~user@185.246.204.50) |
| 2021-05-27 08:01:16 | → | poljar joins (~poljar@93-143-155-14.adsl.net.t-com.hr) |
| 2021-05-27 08:01:53 | <kakuhen> | in any case, i'm very very new to haskell and i've read some things that have turned out to be false :< |
| 2021-05-27 08:02:06 | <kakuhen> | i'm assuming my next disappoint will be the fact that functors in haskell don't behave in any way like functors in math do. |
| 2021-05-27 08:02:21 | → | nsilv joins (~nsilv@212.103.198.210) |
| 2021-05-27 08:02:55 | <dminuoso> | kakuhen: To be fair, one should at the same time also consider https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf |
| 2021-05-27 08:03:10 | → | ddellacosta joins (~ddellacos@89.46.62.17) |
| 2021-05-27 08:03:10 | × | michalz quits (~user@185.246.204.50) (Remote host closed the connection) |
| 2021-05-27 08:03:21 | → | michalz joins (~user@185.246.204.60) |
| 2021-05-27 08:03:43 | <joel135> | I think Hask is a category to the same extent that you can do Euclidean category freehand. |
| 2021-05-27 08:03:54 | <dminuoso> | In this lose handwaving notion, you usually pretend that seq does not exist, and that your program terminates. |
| 2021-05-27 08:03:54 | × | poljar1 quits (~poljar@93-139-109-71.adsl.net.t-com.hr) (Ping timeout: 264 seconds) |
| 2021-05-27 08:04:25 | <joel135> | It is hard to draw circles. |
| 2021-05-27 08:04:58 | <joel135> | The sheet of paper is bounded. |
| 2021-05-27 08:05:03 | <kakuhen> | let me try it a few hundred times with my compass ! |
| 2021-05-27 08:05:10 | <dminuoso> | kakuhen: And in fact, folks like edwardk seem to pull a lot of weight from applying category theory to Haskell. |
| 2021-05-27 08:05:32 | <dminuoso> | So clearly it is useful to some degree. |
| 2021-05-27 08:05:33 | <kakuhen> | dminuoso: i appreciate the 2nd paper, but a lot of it goes over my head sadly. |
| 2021-05-27 08:06:04 | → | epolanski joins (uid312403@id-312403.brockwell.irccloud.com) |
| 2021-05-27 08:06:23 | → | dhil joins (~dhil@195.213.192.85) |
| 2021-05-27 08:06:48 | → | o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) |
| 2021-05-27 08:06:48 | × | epolanski quits (uid312403@id-312403.brockwell.irccloud.com) (Client Quit) |
| 2021-05-27 08:06:53 | <joel135> | s/category/geometry/ xD |
| 2021-05-27 08:07:00 | → | wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com) |
| 2021-05-27 08:07:11 | <kakuhen> | We already have cartesian closure, why not define euclidean closure :3c |
| 2021-05-27 08:07:53 | → | ubert1 joins (~Thunderbi@p200300ecdf259d79e6b318fffe838f33.dip0.t-ipconnect.de) |
| 2021-05-27 08:07:58 | × | ddellacosta quits (~ddellacos@89.46.62.17) (Ping timeout: 265 seconds) |
| 2021-05-27 08:08:24 | → | MasterControl joins (~Master@238.140.4.85.dynamic.wline.res.cust.swisscom.ch) |
| 2021-05-27 08:10:28 | → | nschoe joins (~quassel@178.251.84.79) |
| 2021-05-27 08:11:40 | × | o1lo01ol1o quits (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) (Ping timeout: 264 seconds) |
| 2021-05-27 08:12:11 | → | ku joins (~ku@2601:280:c780:7ea0:8d75:13f2:a7bb:13b1) |
| 2021-05-27 08:12:38 | → | boxscape joins (~boxscape@user/boxscape) |
| 2021-05-27 08:12:55 | × | hpc quits (~juzz@ip98-169-35-13.dc.dc.cox.net) (Ping timeout: 272 seconds) |
| 2021-05-27 08:13:31 | × | Pseudonym quits (~Pseudonym@118.211.110.39) (Quit: Going offline, see ya! (www.adiirc.com)) |
| 2021-05-27 08:14:08 | × | bhrgunatha quits (~bhrgunath@2001-b011-8011-6163-fde3-9a54-1125-48fe.dynamic-ip6.hinet.net) (Quit: Leaving) |
| 2021-05-27 08:14:12 | → | hpc joins (~juzz@ip98-169-35-13.dc.dc.cox.net) |
| 2021-05-27 08:15:48 | × | MidAutumnMoon quits (~MidAutumn@user/midautumnmoon) (Quit: Ping timeout (120 seconds)) |
| 2021-05-27 08:17:38 | → | allbery_b joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-05-27 08:19:04 | × | xandaros quits (~xandaros@user/xandaros) (Quit: WeeChat 3.1) |
| 2021-05-27 08:20:14 | × | alex3 quits (~Chel@BSN-77-82-41.static.siol.net) (Ping timeout: 252 seconds) |
| 2021-05-27 08:20:26 | → | autophagy joins (~mika@2a02:8109:8540:36a0::fccc) |
| 2021-05-27 08:20:35 | → | bfrk joins (~Thunderbi@200116b845a103000156427e7b23f5f6.dip.versatel-1u1.de) |
| 2021-05-27 08:20:40 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Ping timeout: 264 seconds) |
| 2021-05-27 08:21:57 | → | ddellacosta joins (~ddellacos@86.106.121.36) |
| 2021-05-27 08:22:31 | → | sondre joins (~sondrelun@eduroam-193-157-188-96.wlan.uio.no) |
| 2021-05-27 08:23:57 | × | img quits (~img@2405:6580:b1c0:2500:94ef:e7f9:57a3:5892) (Quit: ZNC 1.8.1 - https://znc.in) |
| 2021-05-27 08:24:13 | → | img joins (~img@2405:6580:b1c0:2500:94ef:e7f9:57a3:5892) |
| 2021-05-27 08:24:16 | → | alex3 joins (~Chel@BSN-77-82-41.static.siol.net) |
| 2021-05-27 08:25:33 | → | Boomerang joins (~Boomerang@xd520f68c.cust.hiper.dk) |
| 2021-05-27 08:26:17 | × | ddellacosta quits (~ddellacos@86.106.121.36) (Ping timeout: 252 seconds) |
| 2021-05-27 08:32:27 | × | dminuoso quits (~dminuoso@static.88-198-218-68.clients.your-server.de) (Changing host) |
| 2021-05-27 08:32:27 | → | dminuoso joins (~dminuoso@user/dminuoso) |
| 2021-05-27 08:35:35 | → | pe200012_ joins (~pe200012@119.131.208.84) |
| 2021-05-27 08:36:00 | × | pe200012 quits (~pe200012@120.236.162.14) (Ping timeout: 265 seconds) |
| 2021-05-27 08:37:28 | <tdammers> | bottoms are inevitable in a turing-complete language, aren't they |
| 2021-05-27 08:37:40 | → | tonyz joins (~tonyz@user/tonyz) |
| 2021-05-27 08:37:56 | <mniip> | 🥺 |
| 2021-05-27 08:38:06 | ← | tonyz parts (~tonyz@user/tonyz) () |
| 2021-05-27 08:38:27 | → | ddellacosta joins (~ddellacos@89.46.62.22) |
| 2021-05-27 08:39:51 | → | turion joins (~turion@2a02:810d:8ac0:251e:e8a3:1701:9e78:7013) |
| 2021-05-27 08:40:13 | × | haskman quits (~haskman@223.190.83.69) (Quit: Going to sleep. ZZZzzz…) |
| 2021-05-27 08:41:12 | → | lcp joins (~hellcp@83.24.148.243.ipv4.supernova.orange.pl) |
| 2021-05-27 08:41:22 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 2021-05-27 08:43:19 | × | ddellacosta quits (~ddellacos@89.46.62.22) (Ping timeout: 272 seconds) |
| 2021-05-27 08:43:28 | × | m_shiraeeshi quits (~shiraeesh@109.166.58.113) (Ping timeout: 264 seconds) |
| 2021-05-27 08:44:37 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 2021-05-27 08:48:03 | × | hnOsmium0001 quits (uid453710@id-453710.stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-05-27 08:49:41 | → | m_shiraeeshi joins (~shiraeesh@109.166.58.113) |
| 2021-05-27 08:50:04 | × | MasterControl quits (~Master@238.140.4.85.dynamic.wline.res.cust.swisscom.ch) (Ping timeout: 264 seconds) |
| 2021-05-27 08:52:14 | → | vonfry` joins (~user@240e:688:3:1010:d165:d0b6:b436:8121) |
| 2021-05-27 08:52:42 | → | MidAutumnMoon joins (~MidAutumn@user/midautumnmoon) |
| 2021-05-27 08:53:54 | × | vonfry quits (~user@240e:688:3:1010:d165:d0b6:b436:8121) (Read error: Connection reset by peer) |
| 2021-05-27 08:55:24 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:b043:8b77:c7da:42a0) |
| 2021-05-27 08:57:04 | → | ddellacosta joins (~ddellacos@86.106.121.82) |
| 2021-05-27 08:59:42 | × | MidAutumnMoon quits (~MidAutumn@user/midautumnmoon) (Quit: Ping timeout (120 seconds)) |
| 2021-05-27 09:00:03 | → | Torro joins (Torro@gateway/vpn/protonvpn/torro) |
| 2021-05-27 09:00:18 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:b043:8b77:c7da:42a0) (Ping timeout: 264 seconds) |
| 2021-05-27 09:01:30 | × | ddellacosta quits (~ddellacos@86.106.121.82) (Ping timeout: 264 seconds) |
| 2021-05-27 09:03:39 | → | space-shell joins (~space-she@88.98.247.38) |
| 2021-05-27 09:05:02 | <dminuoso> | /home/dminuoso/wobcom/projects/freyja/dist-newstyle/build/x86_64-linux/ghc-8.8.4/freyja-0.4.0.0/l/freyja-lib/noopt/build/freyja-lib/libHSfreyja-0.4.0.0-inplace-freyja-lib.a(IPUtils.o)(.text..LruUS_info+0x14): error: undefined reference to 'ipzm1zi7zi3zm4668157351bfd065b5138d0033c408000ad61c3db5993a261c8759c634d1374e_NetziIPv4_range_closure' |
| 2021-05-27 09:05:08 | <dminuoso> | Linker errors! Do I get a prize? |
| 2021-05-27 09:06:16 | <dminuoso> | Not bad, nuking dist-newstyle helped. |
| 2021-05-27 09:08:51 | × | dunham quits (~dunham@97-113-50-142.tukw.qwest.net) (Ping timeout: 272 seconds) |
| 2021-05-27 09:09:17 | → | MidAutumnMoon joins (~MidAutumn@user/midautumnmoon) |
| 2021-05-27 09:10:53 | × | jjhoo quits (~jahakala@dsl-trebng21-b048b5-171.dhcp.inet.fi) (Quit: leaving) |
| 2021-05-27 09:11:04 | → | jjhoo joins (jahakala@dsl-trebng21-b048b5-171.dhcp.inet.fi) |
| 2021-05-27 09:14:12 | → | ddellacosta joins (~ddellacos@86.106.121.109) |
All times are in UTC.