Logs on 2022-07-12 (liberachat/#haskell)
| 00:05:04 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 00:05:50 | → | talismanick joins (~talismani@2601:200:c100:3850::dd64) |
| 00:06:46 | <talismanick> | Not Haskell-related necessarily, but tangential - I have some questions about the effectful semantics pf linear logic |
| 00:07:35 | <talismanick> | I've been reading up on it, and while it does model resource transitions neatly, it seems less straightforward to model effects compared to, say, uniqueness typing |
| 00:08:10 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 240 seconds) |
| 00:08:42 | <talismanick> | But, given a single "world variable", it's straightforward to model effects with function composition - the effect is whatever the function substituted in the world argument before returning it |
| 00:08:59 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 00:09:36 | <talismanick> | and, functions are naturally represented in first order logic as a 2-argument predicate with the first variable moded "in" and the second "out" (no clue if the notion of variable modes appears in formal studies of logic, but it's quite helpful in programming with Prolog) |
| 00:10:46 | <talismanick> | My question is, is there a similar notion of "in and out moding of 2-predicates" in linear logic to represent sequential state transitions in a referentially-transparent-but-imperative fashion? |
| 00:11:09 | → | alice1 joins (~alice@ip68-3-91-223.ph.ph.cox.net) |
| 00:11:43 | × | alice1 quits (~alice@ip68-3-91-223.ph.ph.cox.net) (Client Quit) |
| 00:11:45 | <talismanick> | Can Haskell's linear types (on arrows, right?) enforce that for the "linear logical counterpart to a function in classical logic"? |
| 00:15:38 | <talismanick> | (on a related note, if categories are like groups... arrows are like homomorphisms?) |
| 00:17:00 | → | mikoto-chan joins (~mikoto-ch@d59mf84twhjn22gzzgy-4.rev.dnainternet.fi) |
| 00:17:24 | <talismanick> | and, for those confused by what I mean by "moding", take a predicate in Prolog with head foo(X,Y) |
| 00:19:03 | <talismanick> | If, when called with some input for X, i.e. `foo(arg, Y)`, Y is bound to a single output (X is in, Y is out because X is grounded and Y is free at calling), it can be straightforwardly translated to a function `foo X -> Y` |
| 00:22:23 | × | gurkenglas quits (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) (Ping timeout: 244 seconds) |
| 00:27:54 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 00:30:57 | × | mikoto-chan quits (~mikoto-ch@d59mf84twhjn22gzzgy-4.rev.dnainternet.fi) (Ping timeout: 276 seconds) |
| 00:31:03 | × | vglfr quits (~vglfr@88.155.25.62) (Ping timeout: 260 seconds) |
| 00:32:02 | → | seriously joins (~seriously@ool-18bd55d4.dyn.optonline.net) |
| 00:35:43 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 00:40:34 | × | Deide quits (~deide@user/deide) (Quit: Client limit exceeded: 20000) |
| 00:42:58 | × | xff0x quits (~xff0x@2405:6580:b080:900:1ebc:3cfb:759f:a6de) (Ping timeout: 240 seconds) |
| 00:47:42 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 244 seconds) |
| 00:49:08 | <talismanick> | Quiet channel today, innit? |
| 00:49:23 | → | Deide joins (~deide@user/deide) |
| 00:49:25 | <geekosaur> | it was busier earlier |
| 00:49:44 | <geekosaur> | I'm around but the only parts of what you said that I really understood were the Prolog parts 🙂 |
| 00:50:52 | <talismanick> | Funny, I explained those because I figured the Haskell crowd would be familiar with the other parts (I'm not so well-versed in type theory or mathematical at large - I'm mostly piecing it together from basic knowledge of abstract algebra) |
| 00:51:08 | <talismanick> | mathematical logic at large* |
| 00:51:33 | <geekosaur> | not all of us are experts on that stuff |
| 00:51:52 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 00:52:44 | <hpc> | yeah, i only learned haskell after realizing i was too stupid to get by with just python :D |
| 00:53:04 | <talismanick> | Linear logic itself is simple, almost stupidly so (a rule language for expressing "you can't have your cake and eat it too" instead of true/false, as Wadler put it); the hard part is all the machinery to connect it with other math/logic |
| 00:56:42 | <talismanick> | I came across that revealing quote in "A Taste of Linear Logic", which does a good job as a mechanistic, programmer-accessible intro to the concepts |
| 00:56:43 | <talismanick> | https://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf |
| 00:57:23 | <talismanick> | Although, the impression I get from self-studying logic is that it would be helpful to first appreciate why FOL is taught first, due to the importance accorded by Lindstrom's theorem |
| 00:57:33 | → | causal joins (~user@50.35.83.177) |
| 00:59:47 | <talismanick> | also, I misquoted - Wadler is far more eloquent |
| 00:59:54 | × | reza[m] quits (~rezaphone@2001:470:69fc:105::3eda) (Quit: Client limit exceeded: 20000) |
| 01:02:06 | × | thewaves quits (~thewaves@2001:470:69fc:105::2:2eef) (Quit: Client limit exceeded: 20000) |
| 01:02:34 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 01:03:26 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 01:04:46 | × | Yehoshua quits (~yehoshua@2001:470:69fc:105::1:593f) (Quit: Client limit exceeded: 20000) |
| 01:07:20 | → | desophos joins (~desophos@50.229.86.138) |
| 01:07:30 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 240 seconds) |
| 01:07:44 | × | desophos quits (~desophos@50.229.86.138) (Client Quit) |
| 01:08:10 | → | desophos joins (~desophos@50.229.86.138) |
| 01:10:35 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:13:00 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 01:14:13 | → | sayola1 joins (~sayola@dslb-088-078-152-210.088.078.pools.vodafone-ip.de) |
| 01:14:48 | × | sayola quits (~sayola@dslb-088-078-152-210.088.078.pools.vodafone-ip.de) (Ping timeout: 276 seconds) |
| 01:15:33 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 01:16:43 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:21:48 | <talismanick> | Also, logic is comparatively easy to study AFAICT (and I absolutely do not mean that as a flex) if you have the time to burn |
| 01:22:03 | → | reza[m] joins (~rezaphone@2001:470:69fc:105::3eda) |
| 01:22:03 | → | Yehoshua joins (~yehoshua@2001:470:69fc:105::1:593f) |
| 01:22:03 | → | thewaves joins (~thewaves@2001:470:69fc:105::2:2eef) |
| 01:22:13 | <talismanick> | As in, it's not something which should be conceptually difficult for a lot of people, unlike, say, real analysis |
| 01:22:53 | <talismanick> | maybe I just haven't run into the "hard parts" yet |
| 01:23:22 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 01:26:12 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 276 seconds) |
| 01:26:57 | × | monaaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 244 seconds) |
| 01:28:31 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 01:29:01 | → | monaaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 01:29:40 | → | Cajun joins (~Cajun@user/cajun) |
| 01:35:51 | × | alexfmpe[m] quits (~alexfmpem@2001:470:69fc:105::38ba) (Quit: Client limit exceeded: 20000) |
| 01:36:05 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 272 seconds) |
| 01:42:31 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 01:49:03 | × | desophos quits (~desophos@50.229.86.138) (Quit: Leaving) |
| 01:49:05 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 01:51:29 | → | dsrt joins (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 01:52:52 | Hash | is now known as stoned |
| 01:53:53 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 02:00:35 | × | zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 02:00:47 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 272 seconds) |
| 02:00:47 | × | machinedgod quits (~machinedg@d172-219-86-154.abhsia.telus.net) (Ping timeout: 272 seconds) |
| 02:03:00 | → | zaquest joins (~notzaques@5.130.79.72) |
| 02:06:01 | → | nate4 joins (~nate@98.45.169.16) |
| 02:12:30 | × | monaaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 240 seconds) |
| 02:13:17 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 02:14:48 | → | monaaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 02:16:24 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 02:18:30 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 240 seconds) |
| 02:19:56 | → | yauhsien joins (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) |
| 02:23:50 | × | monaaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 240 seconds) |
| 02:26:09 | → | monaaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 02:28:54 | × | td_ quits (~td@muedsl-82-207-238-180.citykom.de) (Ping timeout: 276 seconds) |
| 02:30:15 | → | td_ joins (~td@94.134.91.223) |
| 02:34:38 | × | monaaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 244 seconds) |
| 02:36:20 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 02:36:31 | → | monaaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 02:41:30 | × | monaaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 240 seconds) |
| 02:42:51 | → | monaaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 02:44:23 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:44:23 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 02:44:23 | finn_elija | is now known as FinnElija |
| 02:47:38 | → | frost joins (~frost@user/frost) |
| 02:49:06 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 02:49:09 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 02:50:31 | → | jargon joins (~jargon@184.101.188.251) |
| 02:53:58 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 02:55:53 | × | nate4 quits (~nate@98.45.169.16) (Ping timeout: 272 seconds) |
| 03:02:13 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 272 seconds) |
| 03:14:52 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 03:16:05 | → | bilegeek joins (~bilegeek@2600:1008:b026:a23d:b3a1:a087:edc0:7dfb) |
| 03:19:04 | × | seriously quits (~seriously@ool-18bd55d4.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 03:20:35 | × | monaaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds) |
| 03:22:14 | → | monaaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 03:22:31 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 03:40:16 | × | mvk quits (~mvk@2607:fea8:5ce3:8500::909a) (Ping timeout: 244 seconds) |
| 03:48:13 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 03:55:15 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 03:55:40 | → | zxx7529 joins (~Thunderbi@user/zxx7529) |
| 03:58:52 | × | m1dnight quits (~christoph@78-22-0-121.access.telenet.be) (Ping timeout: 244 seconds) |
| 04:00:46 | → | m1dnight joins (~christoph@78-22-0-121.access.telenet.be) |
| 04:01:15 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 04:01:15 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 04:01:37 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 04:02:18 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 04:03:10 | × | finsternis quits (~X@23.226.237.192) (Remote host closed the connection) |
| 04:05:06 | × | jargon quits (~jargon@184.101.188.251) (Remote host closed the connection) |
| 04:11:26 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 268 seconds) |
| 04:11:52 | × | enthropy quits (~enthropy@24-246-69-9.cable.teksavvy.com) (Ping timeout: 252 seconds) |
| 04:12:05 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 04:14:18 | × | rembo10 quits (~rembo10@main.remulis.com) (Quit: ZNC 1.8.2 - https://znc.in) |
| 04:15:16 | → | rembo10 joins (~rembo10@main.remulis.com) |
| 04:23:48 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 04:26:08 | × | motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 260 seconds) |
| 04:26:53 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 04:29:52 | × | noteness quits (~noteness@user/noteness) (Remote host closed the connection) |
| 04:30:14 | → | noteness joins (~noteness@user/noteness) |
| 04:36:39 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 04:43:49 | × | dsrt quits (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 244 seconds) |
| 04:52:08 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 04:56:36 | → | dsrt joins (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 04:59:07 | → | mmhat joins (~mmh@p200300f1c7090723ee086bfffe095315.dip0.t-ipconnect.de) |
| 05:01:05 | → | merijn joins (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 05:06:56 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 268 seconds) |
| 05:09:15 | × | cony_mony[m] quits (~conymonym@2001:470:69fc:105::2:2ea2) (Quit: Client limit exceeded: 20000) |
| 05:10:16 | → | mbuf joins (~Shakthi@122.165.55.71) |
| 05:16:53 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 05:17:45 | × | merijn quits (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 272 seconds) |
| 05:18:03 | × | zxx7529 quits (~Thunderbi@user/zxx7529) (Ping timeout: 260 seconds) |
| 05:19:42 | × | Cajun quits (~Cajun@user/cajun) (Ping timeout: 252 seconds) |
| 05:32:00 | → | vglfr joins (~vglfr@88.155.25.62) |
| 05:45:00 | → | zxx7529 joins (~Thunderbi@user/zxx7529) |
| 05:46:04 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 05:47:48 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 05:52:00 | → | Midjak joins (~Midjak@82.66.147.146) |
| 05:52:40 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 05:58:00 | × | Franciman quits (~Franciman@mx1.fracta.dev) (Max SendQ exceeded) |
| 05:58:14 | → | Franciman joins (~Franciman@mx1.fracta.dev) |
| 06:02:16 | → | dsp joins (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 06:05:38 | → | gmg joins (~user@user/gehmehgeh) |
| 06:07:42 | → | _ht joins (~quassel@231-169-21-31.ftth.glasoperator.nl) |
| 06:16:24 | × | dsrt quits (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 260 seconds) |
| 06:16:26 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 06:17:07 | → | gmg joins (~user@user/gehmehgeh) |
| 06:17:55 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 272 seconds) |
| 06:18:12 | → | dsrt joins (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 06:19:08 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:19:18 | × | monaaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds) |
| 06:21:48 | → | polux8 joins (~polux@51-15-169-172.rev.poneytelecom.eu) |
| 06:22:01 | → | neightchan joins (~nate@98.45.169.16) |
| 06:22:08 | → | dostoevsky6 joins (~5c42c5384@user/dostoevsky) |
| 06:22:38 | → | danso_o joins (danso@danso.ca) |
| 06:22:47 | → | kraftwerk28_ joins (~kraftwerk@178.62.210.83) |
| 06:22:59 | → | ajb- joins (~ajb@mimas.whatbox.ca) |
| 06:23:05 | → | sndr joins (~sander@user/sander) |
| 06:23:05 | → | burning_crusade joins (~asturias@2001:19f0:7001:638:5400:3ff:fef3:8725) |
| 06:23:09 | → | rush joins (~sloorush@52.187.184.81) |
| 06:23:20 | → | shriekingnoise_ joins (~shrieking@201.212.175.181) |
| 06:23:45 | → | Furor joins (~colere@about/linux/staff/sauvin) |
| 06:23:51 | → | haskl[error] joins (~haskl@user/haskl) |
| 06:24:01 | × | Qudit quits (~user@user/Qudit) (Remote host closed the connection) |
| 06:24:01 | × | kraftwerk28 quits (~kraftwerk@178.62.210.83) (Quit: ZNC 1.8.2 - https://znc.in) |
| 06:24:01 | × | ajb quits (~ajb@mimas.whatbox.ca) (Quit: bye) |
| 06:24:02 | × | natechan quits (~nate@98.45.169.16) (Read error: Connection reset by peer) |
| 06:24:02 | × | dostoevsky quits (~5c42c5384@user/dostoevsky) (Quit: Ping timeout (120 seconds)) |
| 06:24:02 | × | dumptruckman quits (~dumptruck@23-239-13-163.ip.linodeusercontent.com) (Quit: ZNC - https://znc.in) |
| 06:24:02 | × | danso quits (~danso@danso.ca) (Quit: ZNC - https://znc.in) |
| 06:24:03 | × | mzan quits (~quassel@mail.asterisell.com) (Remote host closed the connection) |
| 06:24:03 | × | auri_ quits (~auri@fsf/member/auri) (Remote host closed the connection) |
| 06:24:03 | × | carbolymer quits (~carbolyme@dropacid.net) (Remote host closed the connection) |
| 06:24:03 | dostoevsky6 | is now known as dostoevsky |
| 06:24:04 | × | polux quits (~polux@51-15-169-172.rev.poneytelecom.eu) (Quit: Ping timeout (120 seconds)) |
| 06:24:04 | × | shriekingnoise quits (~shrieking@201.212.175.181) (Quit: Quit) |
| 06:24:04 | × | dwt_ quits (~dwt_@c-98-198-103-176.hsd1.tx.comcast.net) (Quit: ZNC 1.8.2 - https://znc.in) |
| 06:24:04 | × | sloorush quits (~sloorush@52.187.184.81) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 06:24:04 | × | noctux quits (~noctux@user/noctux) (Read error: Connection reset by peer) |
| 06:24:04 | × | sander quits (~sander@user/sander) (Quit: So long! :)) |
| 06:24:04 | × | haskl quits (~haskl@user/haskl) (Quit: Uh oh... ZNC disconnected.) |
| 06:24:04 | × | red-snail quits (~snail@static.151.210.203.116.clients.your-server.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 06:24:04 | × | remedan quits (~remedan@octo.cafe) (Quit: Bye!) |
| 06:24:04 | × | nibelungen quits (~asturias@45.77.27.149) (Quit: ZNC 1.8.2+deb1+focal2 - https://znc.in) |
| 06:24:04 | × | Inoperable quits (~PLAYER_1@fancydata.science) (Quit: All your buffer are belong to us!) |
| 06:24:04 | × | JimL quits (~quassel@89-162-2-132.fiber.signal.no) (Remote host closed the connection) |
| 06:24:04 | × | wagle quits (~wagle@quassel.wagle.io) (Remote host closed the connection) |
| 06:24:04 | × | dcoutts_ quits (~duncan@host86-176-29-6.range86-176.btcentralplus.com) (Remote host closed the connection) |
| 06:24:04 | × | Colere quits (~colere@about/linux/staff/sauvin) (Remote host closed the connection) |
| 06:24:04 | × | brettgilio quits (~brettgili@c9yh.net) (Quit: Ping timeout (120 seconds)) |
| 06:24:04 | → | dcoutts_ joins (~duncan@host86-176-29-6.range86-176.btcentralplus.com) |
| 06:24:04 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 06:24:04 | → | red-snail1 joins (~snail@static.151.210.203.116.clients.your-server.de) |
| 06:24:04 | × | _ht quits (~quassel@231-169-21-31.ftth.glasoperator.nl) (Quit: No Ping reply in 180 seconds.) |
| 06:24:05 | polux8 | is now known as polux |
| 06:24:11 | × | wolfshappen_ quits (~waff@irc.furworks.de) (Read error: Connection reset by peer) |
| 06:24:11 | sndr | is now known as sander |
| 06:24:15 | → | brettgilio5 joins (~brettgili@c9yh.net) |
| 06:24:24 | × | Furor quits (~colere@about/linux/staff/sauvin) (Max SendQ exceeded) |
| 06:24:28 | → | auri joins (~auri@fsf/member/auri) |
| 06:24:30 | → | dumptruckman joins (~dumptruck@23-239-13-163.ip.linodeusercontent.com) |
| 06:24:31 | → | mzan joins (~quassel@mail.asterisell.com) |
| 06:24:31 | → | JimL joins (~quassel@89-162-2-132.fiber.signal.no) |
| 06:24:32 | → | carbolymer joins (~carbolyme@dropacid.net) |
| 06:24:32 | → | noctux joins (~noctux@user/noctux) |
| 06:24:38 | × | stefan-_ quits (~cri@42dots.de) (Ping timeout: 240 seconds) |
| 06:24:40 | → | wolfshappen joins (~waff@irc.furworks.de) |
| 06:24:42 | × | Clint quits (~Clint@user/clint) (Ping timeout: 264 seconds) |
| 06:24:42 | × | zer0bitz quits (~zer0bitz@2001:2003:f748:2000:a9fb:fc4a:9560:a9be) (Ping timeout: 264 seconds) |
| 06:24:46 | → | Furor joins (~colere@about/linux/staff/sauvin) |
| 06:24:52 | → | zer0bitz joins (~zer0bitz@2001:2003:f748:2000:1a4:ed4b:5e9f:8674) |
| 06:24:53 | × | vglfr quits (~vglfr@88.155.25.62) (Ping timeout: 272 seconds) |
| 06:24:53 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 272 seconds) |
| 06:24:54 | × | nckx quits (~nckx@tobias.gr) (Quit: Updating my Guix System <https://guix.gnu.org>) |
| 06:24:56 | → | kritzefitz_ joins (~kritzefit@debian/kritzefitz) |
| 06:24:57 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 06:24:58 | × | heath quits (~heath@user/heath) (Ping timeout: 240 seconds) |
| 06:24:58 | × | hiredman quits (~hiredman@frontier1.downey.family) (Ping timeout: 240 seconds) |
| 06:25:01 | → | remedan joins (~remedan@octo.cafe) |
| 06:25:05 | → | _ht joins (~quassel@231-169-21-31.ftth.glasoperator.nl) |
| 06:25:13 | → | wagle joins (~wagle@quassel.wagle.io) |
| 06:25:14 | × | cross quits (~cross@spitfire.i.gajendra.net) (Ping timeout: 268 seconds) |
| 06:25:18 | × | AWizzArd quits (~code@gehrels.uberspace.de) (Ping timeout: 264 seconds) |
| 06:25:18 | × | triteraflops quits (~triterafl@user/triteraflops) (Ping timeout: 264 seconds) |
| 06:25:18 | × | dknite quits (~dknite@49.37.45.188) (Ping timeout: 264 seconds) |
| 06:25:18 | × | mjacob quits (~mjacob@adrastea.uberspace.de) (Ping timeout: 264 seconds) |
| 06:25:26 | × | kritzefitz quits (~kritzefit@debian/kritzefitz) (Remote host closed the connection) |
| 06:25:26 | → | Clint joins (~Clint@user/clint) |
| 06:25:34 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 06:25:37 | → | triteraflops joins (~triterafl@user/triteraflops) |
| 06:25:41 | → | dknite joins (~dknite@49.37.45.188) |
| 06:25:41 | → | cross joins (~cross@spitfire.i.gajendra.net) |
| 06:25:42 | → | nckx joins (~nckx@tobias.gr) |
| 06:25:48 | → | mjacob joins (~mjacob@adrastea.uberspace.de) |
| 06:25:56 | → | heath joins (~heath@user/heath) |
| 06:25:59 | → | hiredman joins (~hiredman@frontier1.downey.family) |
| 06:26:01 | → | AWizzArd joins (~code@gehrels.uberspace.de) |
| 06:26:18 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 06:26:30 | → | stefan-_ joins (~cri@42dots.de) |
| 06:27:27 | → | In0perable joins (~PLAYER_1@fancydata.science) |
| 06:29:48 | kritzefitz_ | is now known as kritzefitz |
| 06:30:10 | × | Batzy quits (~quassel@user/batzy) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 06:30:45 | → | dwt_ joins (~dwt_@c-98-198-103-176.hsd1.tx.comcast.net) |
| 06:30:52 | × | bilegeek quits (~bilegeek@2600:1008:b026:a23d:b3a1:a087:edc0:7dfb) (Quit: Leaving) |
| 06:31:15 | <tomsmeding> | talismanick: if you try in a french-language chat you'd have more success with linear logic, I think :p |
| 06:31:17 | → | alexfmpe[m] joins (~alexfmpem@2001:470:69fc:105::38ba) |
| 06:31:17 | → | cony_mony[m] joins (~conymonym@2001:470:69fc:105::2:2ea2) |
| 06:32:06 | <tomsmeding> | It's almost a meme how french theoretical CS people explain everything in terms of linear logic, because they know that well, and the rest of the world doesn't really understand and does it their way |
| 06:32:42 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:32:44 | → | Batzy joins (~quassel@user/batzy) |
| 06:32:46 | <tomsmeding> | They even try to explain differentiation using linear logic! |
| 06:32:57 | <talismanick> | tomsmeding: Ah, that's too bad - I speak Spanish, but not French. Is it still so obscure that interest is restricted to Girard's native tongue? It feels like it has a far larger presence on the Internet than in "the real world". |
| 06:33:32 | <talismanick> | and, I've heard of "differential linear logic", which... I presume is a differentiable programming interpretation? |
| 06:33:38 | <tomsmeding> | Sure it has more presence, but actual research is mostly concentrated in France -- and as a side-effect, also general knowledge among theoreticians |
| 06:33:49 | <tomsmeding> | Sort of :D |
| 06:33:52 | <tomsmeding> | But it's weird |
| 06:35:29 | <tomsmeding> | talismanick: I don't know, but it feels weird to me to capture linear functions in a 2-predicate |
| 06:36:00 | <edwardk> | talismanick: https://github.com/ekmett/linear-logic might be fun for you to mine through |
| 06:36:26 | <ski> | people often seem to conflate linearity with uniqueness |
| 06:36:26 | <edwardk> | that is basically FILL encoded into haskell |
| 06:36:27 | <tomsmeding> | Because the point of linear functions (or, at least, of resource-linear functions as in Linear Haskell / Rust / Clean / whatever) is to not only be interested in _what_ the function computes, but also _how_ it goes about doing that |
| 06:36:32 | <edwardk> | ski: +1 |
| 06:37:04 | <talismanick> | ski: That's the impression I got. Capturing state with linearity seems more... tricky. |
| 06:37:52 | → | NaturalNumber joins (~monadam@137.229.82.64) |
| 06:37:56 | <edwardk> | linearity is a promise to not contract or weaken, uniqueness is a promise that nobody else has contracted (and hence trivially, also weakened it) yet. |
| 06:38:08 | <ski> | "given a single \"world variable\", it's straightforward to model effects with function composition - the effect is whatever the function substituted in the world argument before returning it" -- doesn't seem to be the case for continuation effects (e.g.), no ? |
| 06:39:05 | <edwardk> | a function that takes a linear world and gives back a linear world or one that takes a unique world and gives back a unique world both achieve the same goal, but the reasoning runs completely backwards, one preserves an invariant from output to input, the other from input to output |
| 06:39:16 | <talismanick> | ski: Didn't Haskell used to do I/O with continuations before monads? It's messy in practice but straightforward theorywise, AFAICT. |
| 06:39:37 | <tomsmeding> | Monads are continuations :p |
| 06:39:45 | <tomsmeding> | :t (>>=) |
| 06:39:46 | <lambdabot> | Monad m => m a -> (a -> m b) -> m b |
| 06:39:46 | <edwardk> | talismanick: technically it never used continuations. it started with lazy streams of inputs to outputs |
| 06:40:03 | <edwardk> | the continuation thing is an almost-happened step in between that and monads |
| 06:40:09 | <tomsmeding> | :t interact |
| 06:40:11 | <lambdabot> | (String -> String) -> IO () |
| 06:40:14 | <talismanick> | ah, I see |
| 06:41:01 | <ski> | ("no clue if the notion of variable modes appears in formal studies of logic" -- not much, that i know (although perhaps one could draw a parallel to inductive type indices vs. types defined by structural recursion) .. one can make declarative interpretations of modes (together with associated determinisms), though. one can do this for Mercury, e.g. .. translating to universal, existential, and unique |
| 06:41:05 | <talismanick> | tomsmeding: I suppose it's more so that they can faithfully capture the concrete behavior of functions beyond the rivial case of "take a single world argument, return it modified"? |
| 06:41:07 | <ski> | quantifiers) |
| 06:41:39 | <talismanick> | (linear predicates) |
| 06:41:41 | <ski> | ("on a related note, if categories are like groups... arrows are like homomorphisms?" -- arrows ? like the type class `Arrow' or ?) |
| 06:41:56 | <talismanick> | ski: I meant in the formal, category-theoretic sense |
| 06:42:01 | <talismanick> | I'm no algebra expert :) |
| 06:42:06 | <tomsmeding> | ski: (->) |
| 06:42:15 | <talismanick> | arrows are the same thing as morphisms, right? |
| 06:42:22 | <tomsmeding> | In CT, yes |
| 06:42:25 | <tomsmeding> | In Haskell, no |
| 06:42:31 | <tomsmeding> | Unfortunate name clash |
| 06:42:51 | <talismanick> | ugh |
| 06:42:53 | → | wildsebastian joins (~wildsebas@2001:470:69fc:105::1:14b1) |
| 06:43:11 | <tomsmeding> | `Arrow` is a completely different think in Haskell |
| 06:43:14 | <edwardk> | in haskell Arrow refers to a Freyd category, which is a godawful messy beasst |
| 06:43:15 | <tomsmeding> | *thing |
| 06:43:21 | → | schweers joins (~user@2001:9e8:be64:4500:aaa1:59ff:fe3f:235c) |
| 06:43:46 | <talismanick> | I figured something beyond my understanding was afoot when I came across the Arrow typeclass in descriptions of FRP and stateful automata |
| 06:44:04 | <ski> | "is there a similar notion of \"in and out moding of 2-predicates\" in linear logic to represent sequential state transitions in a referentially-transparent-but-imperative fashion?" -- hm .. i haven't seen it. i have thought a little bit about wanting to talk about something like linearity of terms in Lolli (linear logic programming language, based on lambdaProlog) .. but i didn't really get that far |
| 06:44:12 | <edwardk> | talismanick: if you walk away slowly and pretend you never saw the class, nothing of value will be lost =P |
| 06:44:25 | <talismanick> | "I know 'Hask isn't a category', but isn't it that functions are arrows, type are objects in Hask?" |
| 06:44:43 | <tomsmeding> | talismanick: you mean capturing yhe behaviour of a linear function without necessarily having the material in that representation to _prove_ that it conforms to the linearity restrictions? |
| 06:44:46 | <ski> | edwardk : well, you pointed out that to me, initially :) |
| 06:45:04 | <edwardk> | ski: hah. repeating it mostly for the crowd =) |
| 06:45:34 | <edwardk> | i do wish uniqueness fit cleanly into QTT like the other modalities |
| 06:45:38 | <talismanick> | tomsmeding: Well, isn't that the pipe dream of functional programming since Backus? To provide programs with declarative meaning and let the compiler figure out what that looks like on hardware |
| 06:46:16 | <talismanick> | (if I understand what you're saying correctly) |
| 06:46:31 | <tomsmeding> | talismanick: I mean, yes, but the point of adding resource-linear types to a _programming language_ is to shift that responsibility partway to the programmer |
| 06:46:46 | <ski> | talismanick: "Didn't Haskell used to do I/O with continuations before monads?" -- yes. and the CPS was done to use the Dialogue-style I/O in a more principled (less brittle, more robust) way |
| 06:47:23 | nerdypepper | is now known as aksnay |
| 06:47:30 | aksnay | is now known as akshay |
| 06:47:32 | <edwardk> | ski: re linear logic in logic programming, i did spend a fair bit of time playing around with a home-grown linear-LF using QTT, but i got too ambitious in terms of type inference and it kind of fell apart |
| 06:47:38 | <tomsmeding> | To give the programmer control over specifying that certain things must be done sequentially -- and this sequentislity requirement becomes a guarantee that you can then use in the implementation to do something more efficient |
| 06:48:13 | <edwardk> | the motivation is that having proper substructural types using QTT means i can then use it to reason using HOAS about languages that _themselves_ use some (possibly) coarser semiring choice of QTT. |
| 06:48:25 | Furor | is now known as Colere |
| 06:48:26 | × | _ht quits (~quassel@231-169-21-31.ftth.glasoperator.nl) (Remote host closed the connection) |
| 06:48:30 | <talismanick> | That's true. I wonder if there exists something akin to a "multilinear logic" with selective linearity on arguments |
| 06:48:34 | <ski> | (Andrew Appel has a chapter that uses an opaque `Answer' type as the target type of CPS. this is pretty similar to the `type Dialogue = [Response] -> [Request]' stuff, except the latter is transparent) |
| 06:48:55 | <talismanick> | (I came across work on a "tensorial logic", which seemed interesting in its own right, but it wasn't what I was looking for) |
| 06:48:59 | <tomsmeding> | talismanick: like `f :: a %1-> b -> c` in linear haskell? :P |
| 06:49:17 | <edwardk> | otherwise using an LF to reason about another type system, that uses quantitative types, linear types, etc. is a mess, because the whole selling point is that you get HOAS, but then HOAS falls apart or can't express all your envariables, and you are forced to use De Bruijn like a barbarian in a deliberately crippled language that makes that hard to pay for HOAS you can't use! |
| 06:49:18 | <talismanick> | I suppose you do get it naturally out of currying... |
| 06:49:30 | <tomsmeding> | Takes two arguments, the first linearly and the second non-linearly |
| 06:49:51 | <edwardk> | talismanick: selective linearity and the work on "Quantitative Type Theory" are basically the same idea |
| 06:49:59 | <tomsmeding> | edwardk: sorry, LF? |
| 06:50:07 | <ski> | (er, Appel has a chapter with that, in his "Modern Compiler Implementation in (Java|C|ML)" in 1997,1998 at <https://www.cs.princeton.edu/~appel/modern/>) |
| 06:50:08 | <edwardk> | LF = logical framework, like twelf |
| 06:50:09 | <talismanick> | okay, that sounds like a new term for me to read up about |
| 06:50:12 | <tomsmeding> | Thanks |
| 06:50:13 | <talismanick> | thanks for the reference |
| 06:50:35 | <edwardk> | a deliberately crippled notion of dependent types, where it is crippled enough that HOAS works. unlike in say, coq or agda |
| 06:51:07 | <edwardk> | logical frameworks get used like typed prolog a lot. with modes, etc. |
| 06:51:29 | <talismanick> | (I wondered at first, "is QTT an acronym for Cubical Type Theory, perhaps?") |
| 06:51:33 | <tomsmeding> | I don't know anything about LFs :) |
| 06:52:58 | <ski> | edwardk : hm, i think i may've downloaded some Linear version of Twelf at some point, but didn't get as far as playing around with it |
| 06:53:19 | <tomsmeding> | talismanick: that would be 🧊TT |
| 06:54:22 | <talismanick> | tomsmeding: your joke fails because it shows up as :ice-cube : (in plain text) in Emacs! |
| 06:54:31 | <tomsmeding> | Lol |
| 06:54:35 | <talismanick> | (I disabled emojis because Unicode is hanging it for some reason) |
| 06:54:50 | <tomsmeding> | Sad that there is no plain cube in unicode |
| 06:54:58 | <edwardk> | https://www.irccloud.com/pastebin/SZklR7W2/example.lf |
| 06:55:00 | <talismanick> | or, some Unicode - it'd be nice if "everything broke" so I knew "Unicode is the problem" and could fix it |
| 06:55:12 | <edwardk> | ^- there is a sketch of how you use an LF relative to a prolog or datalog program |
| 06:55:30 | <edwardk> | the <- arrow is just that a flipped arrow |
| 06:55:47 | <edwardk> | rule2 has an implicit pi type in its signature |
| 06:56:01 | <talismanick> | edwardk: backwards implication, like in a Horn clause? |
| 06:56:36 | <talismanick> | oh, definitely it - just looked |
| 06:57:05 | <tomsmeding> | edwardk: so I could read rule1 as having type `parent X Y -> ancestor X Y`? |
| 06:57:06 | <edwardk> | rule2 : Π X Y Z : name. parent X Y -> ancestor Y Z -> ancestor X Z |
| 06:57:10 | <edwardk> | yep |
| 06:57:12 | <tomsmeding> | Right |
| 06:57:24 | <edwardk> | er with the right variables |
| 06:57:31 | <edwardk> | X Y and Y Z |
| 06:57:55 | <edwardk> | haskell-like n that using a variable (in upper case here) implicitly quantifies it |
| 06:57:57 | <tomsmeding> | Both of our messages are correct, right? |
| 06:58:03 | <edwardk> | yes |
| 06:58:34 | <ski> | "envariables" ? |
| 06:58:36 | <edwardk> | the convention is to write with the <- in LFs so it reads more like the :- in datalogg |
| 06:58:38 | <tomsmeding> | So is this term search? |
| 06:58:41 | <edwardk> | yeah |
| 06:58:53 | <tomsmeding> | Cool |
| 06:58:59 | <edwardk> | program synthesis as a 'proof-relevant' version of prolog |
| 06:59:07 | <tomsmeding> | Neat |
| 06:59:17 | <edwardk> | types as judgments, there's some neat reasoning you can do within this framework |
| 06:59:35 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 06:59:35 | × | boxscape quits (~boxscape@user/boxscape) (Quit: Client limit exceeded: 20000) |
| 06:59:44 | <ski> | `fact1',`fact2',`rule1',`rule2' act like data constructors for `parent' and `ancestor' (just like `bob',`nancy' are for `name') -- you can match on them |
| 06:59:54 | <edwardk> | whats interesting is you can just hallucinate whatever types you want into scope. like the equivalent of asserting data constructors with assumptions |
| 06:59:58 | → | acidjnk joins (~acidjnk@p200300d6e7058634bd1cff6d17bc0490.dip0.t-ipconnect.de) |
| 06:59:59 | → | boxscape joins (~boxscape@user/boxscape) |
| 07:00:12 | <edwardk> | matching is forbidden =) |
| 07:00:27 | <edwardk> | the point of an LF is that it gives you no tools for pattern matching |
| 07:00:31 | <edwardk> | so. HOAS is always valid |
| 07:00:34 | <edwardk> | no exotic terms can exist |
| 07:00:41 | <tomsmeding> | Yeah I was wondering what would happen if you'd allow matching on the proof here :p |
| 07:01:10 | <edwardk> | the nice thing is you can write a lambda calculus with something like: tm : type; lam : (tm -> tm) -> tm; app : tm -> tm -> tm |
| 07:01:18 | <edwardk> | and you get the 'var' case for free |
| 07:01:20 | <ski> | yea, you can't match in terms (expressions). you can only match during search (of solutions / proof of a goal) |
| 07:01:25 | <edwardk> | lam (\x -> x) |
| 07:01:29 | <tomsmeding> | Right, funny thing is that when I was first explained HOAS in a lecture, first thing I did in the break was show the teacher what I now know is an exotic term, and ask how can this possibly work |
| 07:02:03 | <edwardk> | because i can know that the function i hand in which is given an abstract 'tm' can't match on it in any way |
| 07:02:13 | <tomsmeding> | Yeah that's nice about hoas |
| 07:02:29 | <ski> | calling `parent bob X' is matching that goal with the clause (fact) `parent bob nancy', so that `X' becomes `nancy' |
| 07:02:31 | <edwardk> | this makes reasoning about "meta-theory" in an LF very nice. because there i'm reasoning about an arbitrary LF program, not an arbitrary Coq program or the like |
| 07:02:39 | <tomsmeding> | But it's godawful to work with if you want to do something to the terms you're representing in hoas form |
| 07:02:53 | → | christiansen joins (~christian@83-95-137-75-dynamic.dk.customer.tdc.net) |
| 07:02:56 | <ski> | (and ditto for calling `ancestor', which calls `parent') |
| 07:03:02 | <edwardk> | well, in dependent type land you are usually stuck with some phoas trick, which _is_ awful. |
| 07:03:13 | <edwardk> | but in an LF you are usually able to stick in proper hoas. |
| 07:03:33 | <edwardk> | and the benefit is that if you can express what you want using HOAS in LF you can't "fuck up the names" |
| 07:03:36 | <talismanick> | phoas? |
| 07:03:48 | <tomsmeding> | Try doing something like common subexpression elimination on a program represented in hoas form |
| 07:03:51 | <edwardk> | phoas = parametric hoas. adam chlipala has a paper on it |
| 07:03:56 | <edwardk> | tomsmeding: have, it sucks |
| 07:04:03 | <tomsmeding> | :D |
| 07:04:15 | <edwardk> | this is why i've been working towards an LF using egg |
| 07:04:21 | <edwardk> | then i can just get it all by magic for free |
| 07:04:47 | <edwardk> | CSE, optimization rules, whatever |
| 07:05:11 | <tomsmeding> | @hackage egg |
| 07:05:11 | <lambdabot> | https://hackage.haskell.org/package/egg |
| 07:05:14 | <tomsmeding> | 404 |
| 07:05:37 | <ski> | right, to be able to do variables in HOAS, using `tm', you need goal implication and goal universal quantification (which lambdaProlog also has, but Prolog doesn't really .. well, you can code a forall/2 predicate (which technically is implication, not universal quantification, while achieving the effect of both) .. but operationally it behaves differently. enumerating and testing, as opposed to conjuring up |
| 07:05:39 | <edwardk> | if you look at https://github.com/philzook58/egglog0-talk/blob/main/out.pdf and try to do the same transformation from it to a LF that i sketched for prolog/datalog above you get the idea |
| 07:05:39 | <tomsmeding> | Was it something something egraphs? |
| 07:05:43 | <ski> | skolems and assuming clauses) |
| 07:05:46 | <edwardk> | egg is egraphs-good, yeah |
| 07:05:48 | <edwardk> | its in rust |
| 07:06:11 | <edwardk> | spent the weekend trying to make a nice model of egraphs in haskell and generally failing |
| 07:06:23 | <edwardk> | (i want a _nice_ API) |
| 07:07:13 | <edwardk> | ski: my end-goal with an LF is to get to one that works in a more guanxi/kanren like fashion for the search than a traditional LF, so i can program usefully with those relations |
| 07:07:37 | <edwardk> | twelf uses a prolog'ish, depth-first search |
| 07:07:55 | <edwardk> | and so you find yourself with the usual limitations you'd expect from an untabled prolog |
| 07:07:57 | × | dsrt quits (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 272 seconds) |
| 07:08:13 | <edwardk> | easily bottoming out, needing but not having the equivalent of cut, etc. |
| 07:09:41 | → | coot joins (~coot@213.134.190.95) |
| 07:09:52 | <edwardk> | for the record, i'm rather aggressively hiring on the egg/e-graph side of things at groq. |
| 07:10:19 | <ski> | edwardk : hm, what's the specific guanxi/kanren part ? (haven't looked in detail at these) |
| 07:10:23 | <edwardk> | the LFish bits above are more my own personal project though |
| 07:10:35 | <ski> | being able to externally customize search in some way ? |
| 07:10:40 | <edwardk> | kanren does a logict style search (it was why LogicT was invented) |
| 07:10:58 | <edwardk> | logict has the benefit of offering a 'fairer' interleaving of goals. |
| 07:11:03 | <edwardk> | the WAM is depth first |
| 07:11:48 | <edwardk> | you can think of logict as offering a sort of 'divergence by halves'. if you give half of your attention to the first goal, and half of what remains to the next, and half of what remains to the next.. you get a sort of geometric series. so instead of diverging you just slow by 2x |
| 07:12:04 | <edwardk> | so if there's a match to be found you'll still find it rather than bottom out hard |
| 07:12:15 | <ski> | re cut, perhaps it could borrow some ideas from Mercury there (switch disjunctions, committed-choice nondeterminism) ? |
| 07:12:19 | <edwardk> | guanxi is partially about refining that to distributions that don't look like strict powers of 2 |
| 07:12:47 | <edwardk> | committed-choice is very much like cut in that it is a non-compositional reasoning tool. |
| 07:13:05 | <edwardk> | i want thing that feel like programming with relations, where i glue two relations together and don't have to care about their guts |
| 07:13:19 | <edwardk> | that is kanren's strength (and biggest weakness) |
| 07:13:37 | <edwardk> | kanren doesn't do enough to cut the exponent in the search space down |
| 07:13:43 | <edwardk> | that is why i went off and worked on guanxi |
| 07:13:52 | <talismanick> | edwardk: akin to how power sets being of 2^n cardinality can be considered as a consequence of n binary probabilistic experiments? (set inclusion or exclusion) |
| 07:14:53 | → | benin0 joins (~benin@183.82.29.162) |
| 07:15:05 | <Axman6> | Damn, I've missed a Kmettflood on cool stuff |
| 07:15:07 | <ski> | well, committed-choice nondeterminism in Mercury is declarative. it's used when a goal has no output instantiations (e.g. because of existential quantification). in that case, the inner goal is called in a way to compute at most one solution |
| 07:15:12 | <edwardk> | talismanick: well, it has implementation consequences in the WAM you can actually change variables mutably to point to their current bindings, and backtrack on the way out. but when you have, multiple logical threads being tracked, you need to carry the environment has an explicit substitution and pay for that in performance (this is how kanren works) |
| 07:17:22 | <talismanick> | for the WAM (with which I am somewhat familiar with on a surface level), I've never understood why "tagging lvars with more info" (many-sorted logic) and partitioning search with that extra info couldn't be used to encapsulate and prune search spaces for more "usable" programming |
| 07:17:27 | <ski> | (you can also use it to explicitly ask for just one solution, out of many possible, for `main'. and you can `promise' that a committed-choice nondet goal, at that point, has one / at most one solution, upto duplicates (which can involve nontrivially equivalent structures, in case of user-defined equality, iow quotients)) |
| 07:17:56 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:18:05 | <talismanick> | (we reason in terms of types anyways, in programming and even in normal math - no one does stuff from FOL or ZFC - so why not in Prolog, too?) |
| 07:18:34 | <edwardk> | talismanick: that is basically the guanxi approach. tracking propagators between variables, to reduce the exponent in the search space, then using a more kanren style search to avoid spuriously bottoming out, but adding (abstract) conflict-directed clause learning so it can learn about other worlds rather than brute force everything |
| 07:18:59 | → | Cajun joins (~Cajun@user/cajun) |
| 07:19:18 | <edwardk> | ski: i don't hate the notion of a committed choice when the alternatives are indistinguishable |
| 07:19:19 | <talismanick> | fascinating. Does it bear relation to categorical logic? Of all topics, that sounds like an obviously rich combo, but I'm a ways off from being ready to read about it |
| 07:19:27 | <edwardk> | distinguishable committed choices are more concerning to me |
| 07:20:10 | <talismanick> | (I imagine categorical logic deals in facts "hidden" behind products lifted into objects) |
| 07:20:16 | <edwardk> | https://www.youtube.com/watch?v=D7rlJWc3474 is an intro to the ideas behind the guanxi project. though i got pulled away from it when i left MIRI |
| 07:20:29 | <ski> | edwardk : i think pbone worked on sharing logic / "dataflow" variables between multiple threads of execution (both kinds of AND-parallelism, iirc) |
| 07:20:37 | <edwardk> | the first video in that sequence is pretty self-contained. the other 3 get progressively more workshop like |
| 07:21:48 | <edwardk> | talismanick: there's a lot of category theory involved in talking about the different adjunctions between various abstract interpretation domains, but no categorical logic per se |
| 07:21:48 | × | yauhsien quits (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 07:22:45 | <edwardk> | my goal with this was to use it as an intermediate form for manipulating the half-compiled guts of a higher level language |
| 07:22:58 | <edwardk> | e.g. i didn't want to write a full coda compiler in haskell, then have to bootstrap |
| 07:23:02 | <ski> | ("and backtrack on the way out" -- reminds me of a simple prototype i did, which enabled "backtracking backtracking" (in arbitrary many steps), wrt having goal implications (better behaving than the forall/2 (or foreach/2) Prolog ones) .. of the generate&test rather than the conjure&assume variant. also involved flipping interpretation between skolems and logic variables) |
| 07:23:13 | → | MajorBiscuit joins (~MajorBisc@wlan-145-94-167-213.wlan.tudelft.nl) |
| 07:23:37 | <edwardk> | i;d rather write a fancy logical framework in haskell, then compile down to the LF from the high level language, then just have to port the LF to the new language |
| 07:24:12 | <ski> | talismanick : "lvars" as in "logic variables", or as in `lvish' ? |
| 07:24:19 | <ski> | @hackage lvish |
| 07:24:19 | <lambdabot> | https://hackage.haskell.org/package/lvish |
| 07:24:53 | <edwardk> | ski: my approach is a little "cute" in that what i do is turn fair coinflips into arbitrary distributions using an arithmetic decoder. but then track the bitstrings i used. |
| 07:25:20 | <edwardk> | the key is that when you backtrack and learn there's no solution in a space you need to mark off the space of bits that would encode to the same solution |
| 07:25:22 | → | `2jt joins (~jtomas@141.red-88-17-65.dynamicip.rima-tde.net) |
| 07:25:35 | <ski> | edwardk : "distinguishable committed choices are more concerning to me" -- agreed |
| 07:25:48 | × | JimL quits (~quassel@89-162-2-132.fiber.signal.no) (Ping timeout: 260 seconds) |
| 07:25:51 | → | chomwitt joins (~chomwitt@2a02:587:dc0d:4a00:cff7:1232:6084:40) |
| 07:25:53 | <ski> | (when i mention "comitted choice", i usually mean the latter) |
| 07:26:12 | <edwardk> | the idea is then that if you go off and try things for a while, you get a tree of bits that collapses as you learn more, and if it collapses all the way you exhausted the space |
| 07:26:19 | <ski> | (er, by latter i meant "when the alternatives are indistinguishable", sorry) |
| 07:26:30 | <edwardk> | and you can go back to the start and start flipping coins again as a form of restarts |
| 07:27:09 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 07:27:17 | <edwardk> | the arithmetic decoder turns coinflips into arbitrary distributions so you aren't stuck with paying some KL-divergence driven overhead relative to assuming the distribution looks like (0.5,0.25,0.125...) |
| 07:27:48 | <edwardk> | which since that divergence is affecting the POWER in an exponential, is insane |
| 07:27:51 | <talismanick> | ski: logic variables, because I needed to go to the bathroom :) |
| 07:28:39 | <talismanick> | (barely enough time to type that out) |
| 07:29:16 | <talismanick> | Now that I think about it, this whole discussion has me positively drained digging about my mind for relevant references |
| 07:29:23 | <ski> | edwardk : hm, "collapse" here meaning ? |
| 07:29:28 | <edwardk> | in any event you can basically just give an implementation a luby-style restart timer, where it tries random probes into the space that are single shot interleaved with ones that have exponentially longer and longer runtime, and that system above will find everything if the system is exhaustible, and by tracking and ruling out any place you've been before its not _that_ bad. |
| 07:29:40 | × | lbseale quits (~quassel@user/ep1ctetus) (Ping timeout: 244 seconds) |
| 07:29:42 | <talismanick> | time for bed, I suppose |
| 07:30:05 | <ski> | ("KL" ?) |
| 07:30:09 | <edwardk> | consider if i flip and get 1 for the first bit, then try 10, and fail, and backtrack and try 11 and fail, then i can rule out all bitstrings that start with 1. |
| 07:30:24 | <edwardk> | i don't need to store all the suffixes i tried |
| 07:30:28 | <edwardk> | just that everything after 1* is dead |
| 07:30:39 | <edwardk> | if i get down to * is dead i'm done, no solution exists |
| 07:31:24 | → | yauhsien joins (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) |
| 07:31:39 | <edwardk> | but now consider if instead of choices that are binary i have something like a solution 0 that i want to give 90% of the time, and 1 that i want to try 10% of the time. the arithmetic code for that has lots of things that lead to trying 0 |
| 07:31:41 | <ski> | i see .. what i thought, but wanted confirmation |
| 07:32:06 | × | NaturalNumber quits (~monadam@137.229.82.64) (Quit: Leaving) |
| 07:32:36 | <ski> | (i'm reminded of one of Brouwer's three inference steps (i forget the name), wrt bar induction) |
| 07:32:50 | <edwardk> | 0, 10, 110 all try the "0" solution, so we need to encode the fact that when i try any one of them that the entire interval of bitstrings that would yield 0 is masked off (lazily) in the bit tree. |
| 07:33:23 | <edwardk> | er i should have had ... in there on the candidates for selecting 0 in the arithmetic decoder |
| 07:33:39 | <edwardk> | or chosen something that did evenly break into binary =) |
| 07:33:54 | Axman6 | is wondering how long until Ed starts designing a CPU with support for propagators in Clash |
| 07:33:58 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 07:34:22 | <edwardk> | Axman6: i'm busy designing chips with support for ridiculous SIMD parallelism |
| 07:34:34 | <edwardk> | propagators can sit on top of that =P |
| 07:35:09 | <edwardk> | propagators don't seem to need any real hardware support from my view |
| 07:35:13 | <Axman6> | need a SIMP processor |
| 07:35:19 | <edwardk> | =P |
| 07:35:41 | <Axman6> | Groq needs better duckduckgo SEO |
| 07:35:52 | × | dostoevsky quits (~5c42c5384@user/dostoevsky) (Quit: Ping timeout (120 seconds)) |
| 07:36:05 | <edwardk> | http://pkamath.com/publications/papers/tsp-isca20.pdf <- is the best summary of the v1 chip's architecture |
| 07:36:11 | <Axman6> | It's a shame your jobs are all US based, I'd be interested |
| 07:36:23 | → | dostoevsky joins (~5c42c5384@user/dostoevsky) |
| 07:36:27 | × | yauhsien quits (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) (Ping timeout: 272 seconds) |
| 07:36:27 | × | chomwitt quits (~chomwitt@2a02:587:dc0d:4a00:cff7:1232:6084:40) (Ping timeout: 272 seconds) |
| 07:37:34 | <ski> | edwardk : if every path through the (possibly infinite) tree, via the `00' branch from the root, and via the `10' branch, can be detected to be barred, then every path through `0' can be detected to be barred |
| 07:37:47 | <edwardk> | https://www.youtube.com/watch?v=upljocX5mrk and https://www.youtube.com/watch?v=kPUxl00xys4 cover the way we compile and the way we do determinstic networking to turn lots of fully deterministic chips into a big deterministic cluster |
| 07:37:53 | <ski> | (iiuc your bit indexing correctly) |
| 07:38:05 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 07:38:15 | ski | tried finding a source listing the inference rules to check, failed for the moment |
| 07:38:42 | <Axman6> | edwardk: I just promised my psychologist that I'd stop staying up late watching YouTube videos, thanks for ruining that for me :P |
| 07:38:55 | <edwardk> | Axman6: we have some folks in the UK and a _lot_ in canada, but aussie timezones are a bit of a stretch for us logistically |
| 07:39:06 | <ski> | "Groq" ? |
| 07:39:14 | <Axman6> | Can;t handle people too far in the future, I understand that |
| 07:39:16 | <edwardk> | tell them some crazy guy on the internet made you do it |
| 07:39:56 | <edwardk> | ski: groq is a company i work for as their head of software, we build AI accelerator chips. |
| 07:40:05 | <Axman6> | edwardk: only vaugely relatedm but are you familliar with the Mill CPU work? |
| 07:40:22 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:40:25 | <Axman6> | Groq is a Google (Alphabet?) thing right/ |
| 07:40:27 | <Axman6> | ?* |
| 07:40:27 | <lambdabot> | Maybe you meant: v @ ? . |
| 07:40:30 | <edwardk> | if you are familiar at all with Google's TPUs, the guy who designed those (in BlueSpec, a dialect of haskell no less!) is Jonathan Ross, now the CEO of Groq. |
| 07:41:07 | <edwardk> | groq is not alphabet related. its more part of the google diaspora of folks who left and decided to do things while keeping a sort of googlish culture. |
| 07:41:28 | <edwardk> | i'm familiar with the pain and mess that is mill ;) |
| 07:41:32 | <Axman6> | Right, fair enough - is there a similar company making Google's hardware? |
| 07:41:42 | <edwardk> | yeah, its called google. |
| 07:42:04 | <Axman6> | Hmm, I thought they had a spinout, but maybe I was just thinking of Groq |
| 07:43:18 | × | dsp quits (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Ping timeout: 260 seconds) |
| 07:44:16 | <edwardk> | TPUs still exist. Groq's notion is basically just to double down on what makes them good. When Jonathan originally proposed the TPU project and Jeff Dean accepted, he somehow overpromised that he'd use like 70% of the theoretical efficiency of the LUTs and DSPs on the FPGAs he was using at the time, 35% is generally what folks expect. |
| 07:44:32 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 07:45:07 | <edwardk> | he managed to deliver it by using lots of crazy bluespec-like chicanery. then they brought in traditional hardware folks, because it was becoming the next big thing at google and they wanted in... and it dropped right back down to the 'expected' result |
| 07:45:51 | <edwardk> | so sometime after TPUs went from an FPGA project to a bit more than half of all the cycles spent by all of google, he left to form groq. that was a bit over 5 years ago. |
| 07:46:51 | <edwardk> | i'm here because i happen to strongly believe that i want a large SIMD-like execution core for many problems of interest to me. and Groq is the only chip in the AI accelerator space taking the massive single core SIMD strategy. |
| 07:47:17 | <Axman6> | So when you say SIMD, how wide are we talking? |
| 07:47:46 | <Axman6> | (I'm watching your first video at the same time, and just got to the "what it actually looks like" but) |
| 07:48:20 | <edwardk> | we use a 320 _byte_ wide SIMD unit, and can pipeline and retire 4 320x320 matrix-vector multiplies, every clock. |
| 07:48:31 | <edwardk> | per chip |
| 07:48:45 | <Axman6> | that's... quite a lot |
| 07:48:56 | <edwardk> | the v1 chip was the first single core chip to do a petaflop |
| 07:48:58 | <Axman6> | what's the latency? |
| 07:49:02 | <tomsmeding> | uint8 matrices? |
| 07:49:06 | <Axman6> | wow, ok then |
| 07:49:09 | <edwardk> | (technically we're a bit lower than a petaflop in practice) |
| 07:49:20 | <edwardk> | like 750 TFLOPs for the parts we typically sell |
| 07:49:37 | <edwardk> | tomsmeding: yeah, we can do a bit lower fp16 with "truepoint" |
| 07:49:50 | <edwardk> | but int8 (on v1) is our workhorse |
| 07:50:01 | <tomsmeding> | Just like the tpus |
| 07:50:13 | <tomsmeding> | edwardk: is the egg paper a good read? |
| 07:50:41 | <edwardk> | truepoint is a bit differentiated with respect to TPUs, basically we do FP16 but with _no_ intermediate rounding error. |
| 07:51:19 | <edwardk> | tomsmeding: i think the egg writeup is good, but i think it is better if you've watched the old equality saturation talk from ross tate first, which is very short and is a compelling intro to the problem |
| 07:51:24 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 07:51:47 | <Axman6> | in ML, is int8 really just a fixed point type? or used to represent valued between zero and one? |
| 07:51:51 | <edwardk> | https://www.youtube.com/watch?v=hL2MARuBCzw |
| 07:52:07 | → | machinedgod joins (~machinedg@d172-219-86-154.abhsia.telus.net) |
| 07:52:51 | <edwardk> | Axman6: typically what you'd do in ML is train with bigger floats, then take your model and quantize it down to int8 by doing a scaling pass before the layers using post-training quantization or quantization-aware training to get your accuracy back |
| 07:53:37 | <edwardk> | there's a pretty healthy ecosystem around int8 training today because its the workhorse for both the tpu side and the nvidia side |
| 07:53:43 | <tomsmeding> | edwardk: I've read this blog post first https://blog.sigplan.org/2021/04/06/equality-saturation-with-egg/ |
| 07:54:11 | → | yauhsien joins (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) |
| 07:54:18 | <tomsmeding> | But thanks! |
| 07:54:44 | <edwardk> | tomsmeding: basically i've been a huge proponent of equality saturation since tate's original presentation. (i used to use RETE to pull it off), egg changed the asymptotics around in a practical way that made it _way_ easier to implement |
| 07:55:02 | <edwardk> | and practically improved it from a theoretical toy to a day-to-day workhorse |
| 07:55:22 | <tomsmeding> | I know very little about this space, so I'm interested |
| 07:55:35 | <tomsmeding> | Will look at the paper a bit |
| 07:55:36 | <edwardk> | one of my goals over the next year or so it to start using it much more aggressively inside of groq |
| 07:55:57 | <edwardk> | we use it today for post-training quantization and quantization-aware training, rewriting ONNX models into better models |
| 07:56:02 | <tomsmeding> | Your problems making a nice haskell interface were around internal mutation, I expect? |
| 07:56:05 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 07:56:17 | <edwardk> | ddarius implemented that stuff for us in a shockingly compact amount of rust, like 200 lines. |
| 07:56:37 | <edwardk> | yeah. i want e-nodes to be a nice haskell type with hashconsing and i can have that. |
| 07:56:40 | → | kuribas joins (~user@silversquare.silversquare.eu) |
| 07:57:08 | <edwardk> | but the egg notion of rebuilding the egraph would morally change the hash codes of all the e-nodes in the graph, because each e-class gets the hash code of its root e-node |
| 07:57:44 | <edwardk> | so i have to choose between doing evil mutable things (and breaking), not having expressive enough types, having too much memory utilization, or having a hard to use api |
| 07:57:55 | <edwardk> | and i'm trying to thread the needle between all those different concerns |
| 07:59:07 | <edwardk> | what i'd like is that the user inserts things into the graph by just working with syntax-tree like constructions, asserts them into the graph, and then i give them some template-haskell like splices to describe the matching behaviors |
| 07:59:31 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 07:59:55 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 08:00:25 | <edwardk> | basically i'd like to have the hash-consing behavior handled by something like the Merkle construction i give in https://github.com/ekmett/keep |
| 08:00:33 | <edwardk> | but without the redis weirdness |
| 08:02:37 | <edwardk> | my current approach involves building up a big messy hash table full of heterogeneous types for hash consing, using finalizers to strip things out from user-facing roots so that hash consing cleans itself up, but then needing to migrate from one cache to another to rebuild, and having the ability to ask if an AST node is present in a given egraph and/or assert it into the egraph getting a new node out |
| 08:03:20 | <edwardk> | since i use stablenames as the identities in the egraph it comes down to inserting it into one hashtable by structural hashconsing key and another by stablename |
| 08:04:18 | <edwardk> | and when you go to look for a key in the egraph, you check if the stablename is present and if so you're done, otherwise recurse into the syntactic subterms, until you find something that is present and built up from there asserting as you go |
| 08:04:32 | <edwardk> | that way i can keep most of the subterm sharing across egraphs |
| 08:04:56 | <edwardk> | and even keep the larger stablenames since the stablename for the term would remain er.. stable |
| 08:05:20 | → | hsman joins (~hsman@80.95.197.227) |
| 08:05:28 | <edwardk> | so when i migrate from one egraph to the rebuilt one, only terms that actually had their contents changed would actually change and have to be rebuilt |
| 08:05:39 | <edwardk> | the others would port over as the existing object |
| 08:05:52 | <edwardk> | not sure how articulate that was |
| 08:07:50 | <edwardk> | the thing i'm really trying to figure out is the right way to manipulate these from generation to generation, it feels like there's two options, one is you can just assert things into the egraph, and that does lots of unions on union-find structures for each match you find, just dump more data in, then fix up congruence closure on the backswing, which is the egg story. another story involves staging all that up front, which is |
| 08:07:50 | <edwardk> | objectively worse. |
| 08:08:07 | <edwardk> | where what you do is gather all the changes you want to make, then make them all at once. |
| 08:08:36 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 08:08:54 | <edwardk> | the egg-like "mutably change things in place in ways that are visible to subsequent matches but congruence closure isn't yet satisified until you rebuild" story matches onto something like gauss-seidel iteration for me. you can see part way into the current step. |
| 08:09:44 | <tomsmeding> | I don't know enough of egraphs yet to say something useful about the tradeoffs involved |
| 08:09:59 | <tomsmeding> | But yeah this sounds non-trivial, in api design |
| 08:10:06 | <edwardk> | and in practice Gauss-Seidel is faster than a more deterministic Jacobi method for iteratively solving constraints, even if the result is a lot more dependent on the order of constraints |
| 08:10:11 | <turlando> | Noob question (I guess): I have the following function «exponential g lambda = (\x -> - log x / lambda) <$> (uniformFloatPositive01M g)» with signature «exponential :: StatefulGen g m => g -> Float -> m Float». From the REPL I do «g = mkStdGen 23» and then «exponential g 0.1», but I get «No instance for (StatefulGen System.Random.Internal.StdGen m0) arising from a use of ‘it’». What am I missing? |
| 08:10:12 | × | hsman quits (~hsman@80.95.197.227) (Ping timeout: 252 seconds) |
| 08:10:47 | <edwardk> | here ideally your matches are deterministic in that if you iterate this process to a fixed point you get the same graph, but that is an emergent phenomenon of how you _use_ egg, rather than a property of egg itself. |
| 08:11:19 | <tomsmeding> | edwardk: there is no theoretical guarantee that you do end up in a fixpoint, right? |
| 08:11:41 | <tomsmeding> | turlando: what would you expect that m to be instantiated to? |
| 08:11:44 | → | chele joins (~chele@user/chele) |
| 08:12:27 | <edwardk> | tomsmeding: well, this comes down to whether your rewrite rules are 'nice' in some sense. you can come up with lots of classes of them that will hit that guarantee, lots of sufficient conditions, few descriptions of necessary ones |
| 08:12:28 | <turlando> | tomsmeding: Not sure actually. I guess it should be the context of the RNG? |
| 08:12:44 | <tomsmeding> | edwardk: I see, makes sense |
| 08:12:58 | <tomsmeding> | turlando: if you don't know, how is ghc supposed to know? :P |
| 08:13:04 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 08:13:11 | <turlando> | Good point |
| 08:13:16 | <tomsmeding> | That's the error -- ghc has no clue what to instantiate m with |
| 08:13:35 | <edwardk> | usually you'd use some kind of runFoo function to pick the right m. |
| 08:13:43 | <turlando> | Maybe I don't need an m at all? It's the first time I'm using System.Random |
| 08:14:52 | <tomsmeding> | turlando: I suggest you use System.Random first, before going to System.Random.Stateful |
| 08:15:29 | <turlando> | I will, thanks for the suggestion |
| 08:15:31 | <edwardk> | there's a bunch of monad transformers in there for different ways to plumb around the StdGen |
| 08:16:05 | <edwardk> | carrying it in a shared atomic, in a ReaderT style IORef, etc. |
| 08:16:10 | <turlando> | I still feel pretty unfomfortable when moving into the monad transformer territory |
| 08:16:24 | <edwardk> | StateGenM, AtomicGenM, IOGenM, STGenM and TGenM |
| 08:16:49 | <tomsmeding> | turlando: just put the StdGen in a state monad or however you want to pass it around, and use the uniform* family of functions |
| 08:16:56 | <tomsmeding> | Works fine, no monad transformers required |
| 08:17:08 | <edwardk> | then i'd go down to the basic System.Random machinery for now and ignore the monad transformers that exposes |
| 08:17:12 | <tomsmeding> | You can always decide later to go to the stateful version |
| 08:17:17 | <edwardk> | +1 |
| 08:18:25 | <turlando> | Thanks again for the suggestions, I will try |
| 08:19:25 | → | ccntrq joins (~Thunderbi@2a01:c23:8c77:3a00:6188:64f1:5d2d:a884) |
| 08:23:46 | → | Tuplanolla joins (~Tuplanoll@91-159-69-97.elisa-laajakaista.fi) |
| 08:26:51 | → | Pickchea joins (~private@user/pickchea) |
| 08:27:04 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 08:27:55 | <edwardk> | i do want to say one nice thing about the hashconsing story is that you can really quickly compute catamorphisms over them. just build the memotable of the hashes you've seen so far, since everything is well-founded this terminates and gets to use a nice memoization scheme |
| 08:28:14 | <edwardk> | and you can keep the memotable for subsequent invocations later on |
| 08:28:32 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 08:28:53 | → | hsman joins (~hsman@80.95.197.227) |
| 08:29:39 | <edwardk> | this is basically the e-analysis pass for egg, or the same kind of idea as is used by lean to perform folds over hashconsed trees |
| 08:30:02 | <edwardk> | but holy hell is it a booster shot in the arm for performance for a lot of passes |
| 08:31:25 | <edwardk> | i'd like to get to where i can use it with something like https://www.schoolofhaskell.com/user/edwardk/conquering-folds |
| 08:38:10 | <schweers> | I have a problem with Conduit and the types () and Void. When I try to pass a value of type ConduitT () () IO () to runConduit (which has type Monad m => ConduitT () Void m r -> m r) I get an error about () and Data.Void.Void not matching. Am I missing something obvious? |
| 08:45:11 | <[exa]> | schweers: how did you create the value of type ConduitT () () IO () ? |
| 08:46:11 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 08:47:04 | → | vglfr joins (~vglfr@88.155.25.62) |
| 08:47:06 | → | Vajb joins (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) |
| 08:47:32 | <schweers> | I used yield and chained the result with other ConduitT values. I also tried using something different, but it seems no matter what I do, it always comes back to this same problem. |
| 08:48:13 | <schweers> | The weird thing is that I use runConduit somewhere else and that works just fine. There the last part of the pipeline is sinkHandle. |
| 08:48:14 | × | Vajb quits (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) (Read error: Connection reset by peer) |
| 08:48:39 | → | Vajb joins (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) |
| 08:53:13 | <schweers> | To give some more details: the function I’m working on takes (among other arguments) a value of type ConduitT () T.Text IO (). This is then chained with a function from the csv-conduit package and a ConduitT of my own to insert csv rows into a database. Said last ConduitT is of type ConduitT (Row T.Text) () IO (). |
| 08:53:19 | <schweers> | [exa]: ^ |
| 08:53:44 | × | doomfume[m] quits (~doomfumeh@2001:470:69fc:105::2:2a62) (Quit: You have been kicked for being idle) |
| 08:53:44 | × | doomfume[m]1 quits (~doomfumem@2001:470:69fc:105::2:2a64) (Quit: You have been kicked for being idle) |
| 08:57:43 | → | gurkenglas joins (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) |
| 09:02:09 | <[exa]> | schweers: I only used that thing once but it looks like it requires you to explicitly say there's a sink at the end of the pipeline |
| 09:02:15 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:06:29 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 09:06:45 | → | img joins (~img@user/img) |
| 09:09:38 | <[exa]> | schweers: yeah it seems like your type should not specify the output (), instead allow anything in there (just like the type of sinkHandle) |
| 09:09:58 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 09:10:37 | × | Cajun quits (~Cajun@user/cajun) (Quit: Client closed) |
| 09:12:17 | <schweers> | [exa]: hmm, that might be the case. Thanks for the pointer, I’ll see what I can find. |
| 09:13:44 | → | maroloccio joins (~marolocci@151.73.134.175) |
| 09:13:55 | <[exa]> | what's the last thing in the problematic conduit here? |
| 09:14:22 | × | hsman quits (~hsman@80.95.197.227) (Ping timeout: 252 seconds) |
| 09:16:04 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 09:20:28 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 09:23:05 | <schweers> | The last is one I’ve written myself. The goal is to consume the first element of its input stream to create a table in a database, then consume each following element and issue insert statements. As I’m not at all experienced with Conduit I might as well made some mistakes there. |
| 09:24:08 | × | shriekingnoise_ quits (~shrieking@201.212.175.181) (Quit: Quit) |
| 09:24:36 | <schweers> | https://pastebin.com/qwe8ag93 |
| 09:28:13 | <[exa]> | schweers: what happens if you replace the first () on line 20 with `a` ? |
| 09:28:41 | <[exa]> | I see no output -> no reason to push () |
| 09:29:16 | × | JSharp quits (sid4580@id-4580.lymington.irccloud.com) () |
| 09:29:41 | → | JSharp joins (sid4580@id-4580.lymington.irccloud.com) |
| 09:29:44 | <schweers> | Couldn't match type ‘a1’ with ‘()’ |
| 09:30:03 | <schweers> | and that a1 is a rigid type variable bound by the signature for processRows. |
| 09:30:22 | <schweers> | So I get an additional compiler error |
| 09:31:24 | → | jmorris joins (uid537181@id-537181.uxbridge.irccloud.com) |
| 09:31:48 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 09:35:12 | × | mmhat quits (~mmh@p200300f1c7090723ee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 09:37:08 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 09:43:27 | <[exa]> | ah maybe the `pipeline` shouldn't get () too |
| 09:43:34 | <[exa]> | (line 28) |
| 09:44:22 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 09:46:15 | × | phma quits (phma@2001:5b0:215d:e008:5054:f1a6:ecb8:df53) (Read error: Connection reset by peer) |
| 09:47:11 | → | phma joins (~phma@host-67-44-208-203.hnremote.net) |
| 09:48:38 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 09:49:38 | → | mmhat joins (~mmh@p200300f1c7090757ee086bfffe095315.dip0.t-ipconnect.de) |
| 09:51:17 | <schweers> | [exa]: I’m afraid that doesn’t fix it. I have to leave for now, I’ll hopefully be back in about an hour. Thank you so far for your help! |
| 09:52:41 | → | __monty__ joins (~toonn@user/toonn) |
| 09:59:39 | <kuribas> | edwardk: are you writing a egraph library for haskell? |
| 09:59:58 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 10:01:51 | → | dschrempf joins (~dominik@mobiledyn-62-240-134-33.mrsn.at) |
| 10:02:14 | × | dschrempf quits (~dominik@mobiledyn-62-240-134-33.mrsn.at) (Client Quit) |
| 10:10:28 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 10:15:25 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Ping timeout: 272 seconds) |
| 10:16:15 | <gurkenglas> | *googles egraph* kuribas: why not just store a function from the type on which you wish to define an equivalence relation to the set of equivalence classes? |
| 10:16:53 | → | biberu\ joins (~biberu@user/biberu) |
| 10:17:33 | × | biberu quits (~biberu@user/biberu) (Ping timeout: 256 seconds) |
| 10:18:29 | biberu\ | is now known as biberu |
| 10:18:33 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 276 seconds) |
| 10:19:30 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 240 seconds) |
| 10:20:18 | <gurkenglas> | ...oh i guess because you want a fast preimage operation. though i suspect that in many cases you don't actually need that |
| 10:24:23 | <gurkenglas> | *actually reads wikipedia article* are you hoping to use it for an automated theorem prover or compiler? :) |
| 10:27:48 | × | Guest45 quits (~Guest45@bras-base-okvlon5405w-grc-53-70-30-46-127.dsl.bell.ca) (Quit: Client closed) |
| 10:28:26 | × | Lears quits (~Leary]@122-58-224-198-vdsl.sparkbb.co.nz) (Ping timeout: 255 seconds) |
| 10:28:53 | <gurkenglas> | though i suppose the library also generally deserves to exist - in a sense every time you store a function, the structure of an egraph ought to be in easy reach |
| 10:35:18 | <gurkenglas> | Does an egraph provide *all* the operations one can reasonably provide for a stored function? |
| 10:36:17 | → | PiDelport joins (uid25146@id-25146.lymington.irccloud.com) |
| 10:47:52 | × | wenjie quits (~nut@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Quit: WeeChat 3.5) |
| 10:55:08 | → | CiaoSen joins (~Jura@p200300c9570ffb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 10:58:39 | <radhika> | Hi.. I get error messages like “ No instance for (Num String) arising from use of ‘+’ in expression …. In an equation for … |
| 10:58:57 | <radhika> | What does “instance “ mean in all these messages? |
| 10:59:16 | <radhika> | Also what is “it” refer to? |
| 10:59:19 | → | jgeerds joins (~jgeerds@55d437cf.access.ecotel.net) |
| 10:59:34 | <radhika> | What does “it” refer to?? |
| 11:04:33 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 11:05:47 | × | CiaoSen quits (~Jura@p200300c9570ffb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Quit: CiaoSen) |
| 11:06:22 | → | xff0x joins (~xff0x@2405:6580:b080:900:9e06:cb70:78ee:9dbc) |
| 11:06:57 | <[exa]> | radhika: you probably tried to add a String to something? |
| 11:07:28 | <[exa]> | radhika: "No instance for (Constraint Type) ..." means basically "I don't know how Type can satisfy a Constraint" |
| 11:07:52 | <[exa]> | in your case, the compiler tells you that it doesn't know how to make String a numeric object (in class Num) |
| 11:08:10 | <[exa]> | (btw strings are concatenated with ++, if that helps) |
| 11:09:27 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 11:09:28 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 11:09:31 | allbery_b | is now known as geekosaur |
| 11:13:38 | <[exa]> | and re "instance", instance is a part of the typeclass construction. You declare typeclasses (e.g., Num for all numeric things or Ord for all stuff that can be ordered, i.e. has < ), then you add instances of the types that actually fit into the classes (i.e., you write a Num instance for Int and Float and Complex, and Ord instance for Int and Float and Char), and then you can enjoy the typeclass |
| 11:13:44 | <[exa]> | polymorphism and the nice overloading. |
| 11:15:01 | × | frost quits (~frost@user/frost) (Quit: Client closed) |
| 11:16:44 | → | frost joins (~frost@user/frost) |
| 11:17:53 | → | waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 11:21:49 | × | Philonous_ quits (~Philonous@user/philonous) (Quit: ZNC - https://znc.in) |
| 11:22:19 | → | Philonous joins (~Philonous@user/philonous) |
| 11:23:12 | × | talismanick quits (~talismani@2601:200:c100:3850::dd64) (Ping timeout: 244 seconds) |
| 11:23:14 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 11:23:32 | × | frost quits (~frost@user/frost) (Quit: Client closed) |
| 11:31:31 | × | AlexZenon quits (~alzenon@178.34.160.206) (Quit: ;-) |
| 11:31:56 | × | Alex_test quits (~al_test@178.34.160.206) (Quit: ;-) |
| 11:32:14 | × | AlexNoo quits (~AlexNoo@178.34.160.206) (Quit: Leaving) |
| 11:34:52 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 11:38:22 | <schweers> | [exa]: I’m not sure that it really solves my problem, as my tests fail, but changing runConduit pipeline to runConduit $ pipeline .| sinkNull at least makes the compiler happy. |
| 11:39:34 | → | kjak joins (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) |
| 11:39:54 | <[exa]> | yes, that makes sense. The last thing in your pipeline isn't a proper Sink (it produces ()'s), so it can't be run. |
| 11:40:56 | <[exa]> | what was the error when you fix the type annotations to have `a` in output instead of ()? |
| 11:41:29 | → | bontaq joins (~user@ool-45779fe5.dyn.optonline.net) |
| 11:41:43 | <[exa]> | (also not sure if it wouldn't be better to move them into toplevel definitions -- there may be a very undesirable interplay of typesystem features in local scopes) |
| 11:43:41 | <kuribas> | gurkenglas: I was just exploring the page, I haven't even thought of usecases :) |
| 11:43:50 | <schweers> | You mean changing the type of pipeline to ConduitT a b IO ()? |
| 11:44:04 | <kuribas> | gurkenglas: but the given applications look pretty cool, like improving herbie performance for example. |
| 11:44:11 | <schweers> | That gives me • Couldn't match type ‘a1’ with ‘()’ |
| 11:44:49 | <[exa]> | rather `ConduitT () a IO ()` |
| 11:45:26 | <[exa]> | looks to me like the input is set by the type you get with csvInput |
| 11:47:02 | → | AlexNoo joins (~AlexNoo@178.34.160.206) |
| 11:47:12 | → | AlexZenon joins (~alzenon@178.34.160.206) |
| 11:49:19 | <schweers> | `ConduitT () a IO ()` gives me the same error. |
| 11:50:38 | → | Alex_test joins (~al_test@178.34.160.206) |
| 11:53:54 | <[exa]> | in both changed places? |
| 11:54:08 | × | zxx7529 quits (~Thunderbi@user/zxx7529) (Ping timeout: 260 seconds) |
| 11:54:16 | → | hsman joins (~hsman@80.95.197.227) |
| 11:55:57 | <schweers> | Unless I’m completely missing something, then yes. |
| 11:58:02 | <[exa]> | that's weird because it should be okay-ish in one of the places because the outputs changed together |
| 11:58:20 | × | kimjetwav quits (~user@2607:fea8:2340:fe00:730c:be2f:be5e:3847) (Ping timeout: 244 seconds) |
| 11:58:26 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 255 seconds) |
| 11:59:49 | → | dsp joins (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 12:02:21 | → | [Leary] joins (~Leary]@122-58-224-198-vdsl.sparkbb.co.nz) |
| 12:02:48 | <[exa]> | can you paste your error after changing l20 to `ConduitT (Row T.Text) o IO ()` and l28 to `...::ConduitT () o IO ()` ? (Also, you don't have any extensions like ScopedAnything enabled, right?) |
| 12:06:15 | × | hsman quits (~hsman@80.95.197.227) (Quit: Client closed) |
| 12:08:08 | × | Pickchea quits (~private@user/pickchea) (Ping timeout: 260 seconds) |
| 12:12:38 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 12:17:39 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Ping timeout: 272 seconds) |
| 12:17:52 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 12:26:10 | → | notzmv joins (~zmv@user/notzmv) |
| 12:34:49 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 12:35:06 | <radhika> | [exa]: thanks.. my apologies for the delayed reply.. we had a power outage.. |
| 12:35:42 | × | jgeerds quits (~jgeerds@55d437cf.access.ecotel.net) (Ping timeout: 276 seconds) |
| 12:38:33 | → | hsman joins (~hsman@80.95.197.227) |
| 12:39:20 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 12:40:31 | → | {-d0t-} joins (~q_q@user/-d0t-/x-7915216) |
| 12:40:57 | <{-d0t-}> | hello! What is the easiest way to log both request and reply in a WAI app? |
| 12:44:02 | <[exa]> | radhika: np, take care. :D |
| 12:45:56 | → | Pickchea joins (~private@user/pickchea) |
| 12:46:37 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 12:47:37 | → | dsrt joins (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 12:48:40 | <[exa]> | {-d0t-}: you can log the request simply by showing the input of your Application or Middleware. For logging responses you need to stash something to the parameter of Application. I'd just smash traceShow in there. :] |
| 12:49:40 | <{-d0t-}> | [exa]: the thing is, I want to log them as a single string and send that to Grafana |
| 12:50:32 | <[exa]> | ah so. That might require some slightly more advanced Middleware but I guess it will still be representable as a Middleware |
| 12:50:44 | <{-d0t-}> | [exa]: for requests, Warp accepts a logger parameter via Settings, but it only logs response code and not any other part. |
| 12:51:53 | × | dsp quits (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Ping timeout: 260 seconds) |
| 12:52:21 | <[exa]> | like: withLogs :: Middleware; withLogs app req respond = do { logRequest req; app (\x -> logResponse x >> respond x) } |
| 12:52:34 | <[exa]> | logRequest and logResponse can do IO so you should be able to send it there |
| 12:53:05 | <[exa]> | uh wait you want to catch the response data, which are not in ResponseReceived |
| 12:53:16 | <{-d0t-}> | Yeah, that :( |
| 12:53:40 | <{-d0t-}> | https://hackage.haskell.org/package/wai-log-0.2.0.0/docs/Network-Wai-Log.html |
| 12:53:45 | <[exa]> | that's generally impossible with WAI because response gets streamed out right at the point it's available |
| 12:53:50 | <{-d0t-}> | This seems like something I c)ould use |
| 12:54:09 | <[exa]> | but yeah this seems to connect to the right bits |
| 12:54:17 | <{-d0t-}> | [exa]: what if I force evaluate it to some buffer? |
| 12:54:44 | <{-d0t-}> | This seems like an thing that would be obvious and shouldn't be hard to impelement, hence I'm a bit puzzled |
| 12:55:34 | <[exa]> | ah wait no I confused myself |
| 12:55:47 | <[exa]> | Response is perfectly okay and loggable. :D |
| 12:56:05 | <[exa]> | if you dig into the source in the Log there, they do more or less the same thing as `withLogs` above |
| 12:56:31 | <[exa]> | here https://hackage.haskell.org/package/wai-log-0.2.0.0/docs/src/Network.Wai.Log.Internal.html#logRequestsWith |
| 12:56:51 | × | AlexZenon quits (~alzenon@178.34.160.206) (Quit: ;-) |
| 12:57:12 | <{-d0t-}> | oh cool cool! Then this is about what I need. |
| 12:57:14 | <{-d0t-}> | Thanks! |
| 12:57:14 | × | Alex_test quits (~al_test@178.34.160.206) (Quit: ;-) |
| 12:58:25 | <[exa]> | the "Source" links on hackage are magick |
| 12:59:45 | <{-d0t-}> | indeed they are! |
| 13:00:03 | × | AlexNoo quits (~AlexNoo@178.34.160.206) (Quit: Leaving) |
| 13:00:33 | → | zxx7529 joins (~Thunderbi@user/zxx7529) |
| 13:02:52 | × | dknite quits (~dknite@49.37.45.188) (Read error: Connection reset by peer) |
| 13:05:27 | × | dsrt quits (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 268 seconds) |
| 13:06:12 | → | frost joins (~frost@user/frost) |
| 13:07:00 | → | AlexNoo joins (~AlexNoo@178.34.160.206) |
| 13:07:03 | × | Pickchea quits (~private@user/pickchea) (Ping timeout: 272 seconds) |
| 13:07:03 | → | AlexZenon joins (~alzenon@178.34.160.206) |
| 13:07:37 | <gurkenglas> | kuribas: exploring what page? |
| 13:07:57 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 13:08:06 | <kuribas> | gurkenglas: https://egraphs-good.github.io/ |
| 13:09:25 | → | Alex_test joins (~al_test@178.34.160.206) |
| 13:11:28 | → | dsp joins (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 13:12:27 | → | pmarg joins (~pmarg@2a01:799:159f:9b00:692:26ff:fec4:d342) |
| 13:12:31 | → | Fxmuhrwawz joins (~Fxmuhrwaw@191-214-26-24.user.veloxzone.com.br) |
| 13:13:31 | <gurkenglas> | ...I badly misunderstood e-graphs. I thought it stores an equivalence relation over nodes of the graph. |
| 13:16:20 | × | k60`` quits (~user@94.25.174.91) (Ping timeout: 244 seconds) |
| 13:17:47 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 13:17:53 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 13:18:47 | × | Fxmuhrwawz quits (~Fxmuhrwaw@191-214-26-24.user.veloxzone.com.br) (Remote host closed the connection) |
| 13:19:56 | jpds1 | is now known as jpds |
| 13:22:52 | → | ubert1 joins (~Thunderbi@91.141.39.36.wireless.dyn.drei.com) |
| 13:24:34 | × | ubert quits (~Thunderbi@178.165.177.173.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 13:24:34 | ubert1 | is now known as ubert |
| 13:27:26 | <shapr> | gurkenglas: what does it actually do? |
| 13:28:22 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 13:28:52 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 13:29:55 | <gurkenglas> | Stores an equivalence relation over terms of a language. Which happens to be an equivalence relation over nodes of a graph, but that's not the point. I thought it was just supposed to take an arbitrary equivalence relation on a set, then use a graph to efficiently allow operations you might want to do to such a relation. |
| 13:31:26 | <gurkenglas> | (and "arbitrary equivalent relation on a set" is in a sense another word for "function", which is why that seemed general enough to deserve a library) |
| 13:31:44 | <gurkenglas> | s/equivalent/equivalence/ |
| 13:33:23 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 13:35:14 | shapr | tries to understand the difference |
| 13:35:22 | × | dsp quits (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Ping timeout: 272 seconds) |
| 13:36:02 | shapr | reads the tutorial |
| 13:39:17 | → | dsp joins (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 13:41:55 | <edwardk> | kuribas: i was writing some code that wanted to use egraphs, and was debating about ways to get it to be nice, one way would be to turn it into a library, yes |
| 13:42:32 | <kuribas> | +1 to make it into a library :) |
| 13:42:52 | brettgilio5 | is now known as brettgilio |
| 13:42:59 | kuribas | wonders if you can ffi into rust... |
| 13:43:28 | <shapr> | I thought there was an inline-rust package at some point |
| 13:44:18 | <shapr> | https://github.com/harpocrates/inline-rust ? |
| 13:45:19 | → | dsrt joins (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 13:46:16 | <shapr> | this is an interesting read: https://docs.rs/egg/0.9.0/egg/tutorials/ |
| 13:46:19 | × | {-d0t-} quits (~q_q@user/-d0t-/x-7915216) (Ping timeout: 272 seconds) |
| 13:48:37 | × | acidjnk quits (~acidjnk@p200300d6e7058634bd1cff6d17bc0490.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 13:49:36 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 13:50:25 | → | {-d0t-} joins (~q_q@user/-d0t-/x-7915216) |
| 13:53:22 | <tomsmeding> | shapr: I found this to be a good intro as well https://blog.sigplan.org/2021/04/06/equality-saturation-with-egg/ |
| 13:53:33 | <shapr> | thanks! |
| 13:53:51 | <tomsmeding> | But maybe tutorial part 1 covers that? Not sure, I skipped part 1 after having read the blogpost |
| 13:54:53 | × | motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 260 seconds) |
| 13:57:43 | × | dsrt quits (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 272 seconds) |
| 13:59:21 | × | troydm quits (~troydm@host-176-37-124-197.b025.la.net.ua) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset) |
| 13:59:30 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 14:01:57 | <mrianbloom> | Is it possible to make a type family that is part of a typeclass also injective? |
| 14:04:03 | × | {-d0t-} quits (~q_q@user/-d0t-/x-7915216) (Ping timeout: 272 seconds) |
| 14:04:48 | × | dsp quits (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Ping timeout: 260 seconds) |
| 14:09:04 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 14:09:32 | × | frost quits (~frost@user/frost) (Ping timeout: 252 seconds) |
| 14:11:18 | → | dsrt joins (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 14:17:46 | → | _ht joins (~quassel@231-169-21-31.ftth.glasoperator.nl) |
| 14:19:58 | → | jgeerds joins (~jgeerds@55d437cf.access.ecotel.net) |
| 14:22:50 | × | toluene quits (~toluene@user/toulene) (Ping timeout: 240 seconds) |
| 14:23:08 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:24:28 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 14:24:51 | → | toluene joins (~toluene@user/toulene) |
| 14:30:52 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 14:31:18 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 14:33:47 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 14:37:42 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 14:39:48 | × | dsrt quits (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 268 seconds) |
| 14:41:21 | <ski> | % class Foo a where type Bar a = r | r -> a -- mrianbloom ? |
| 14:41:21 | <yahb2> | <no output> |
| 14:41:36 | → | acidjnk joins (~acidjnk@p200300d6e7058634bd1cff6d17bc0490.dip0.t-ipconnect.de) |
| 14:41:50 | <mrianbloom> | ski: Is wasn't sure if that syntax works? |
| 14:42:08 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 14:43:51 | <mrianbloom> | Ah, I think it does. You just need TypeFamilyDependencies enabled. |
| 14:43:57 | <mrianbloom> | Thank you |
| 14:44:47 | → | indigo_ibs joins (~user@31.124.106.79) |
| 14:45:14 | <ski> | np |
| 14:47:19 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 14:49:39 | × | schweers quits (~user@2001:9e8:be64:4500:aaa1:59ff:fe3f:235c) (Ping timeout: 272 seconds) |
| 14:50:22 | → | shriekingnoise joins (~shrieking@201.212.175.181) |
| 14:51:10 | → | benin09 joins (~benin@156.146.51.131) |
| 14:51:37 | × | jmorris quits (uid537181@id-537181.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 14:52:04 | × | machinedgod quits (~machinedg@d172-219-86-154.abhsia.telus.net) (Remote host closed the connection) |
| 14:52:22 | → | dsrt joins (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 14:52:49 | × | benin0 quits (~benin@183.82.29.162) (Ping timeout: 272 seconds) |
| 14:52:49 | benin09 | is now known as benin0 |
| 14:54:28 | → | machinedgod joins (~machinedg@d172-219-86-154.abhsia.telus.net) |
| 14:55:34 | × | pmarg quits (~pmarg@2a01:799:159f:9b00:692:26ff:fec4:d342) (Remote host closed the connection) |
| 14:59:51 | × | dextaa quits (~DV@user/dextaa) (Read error: Connection reset by peer) |
| 15:01:51 | → | benin09 joins (~benin@183.82.29.162) |
| 15:02:05 | → | dextaa joins (~DV@user/dextaa) |
| 15:02:53 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 15:04:04 | × | dextaa quits (~DV@user/dextaa) (Read error: Connection reset by peer) |
| 15:04:13 | × | benin0 quits (~benin@156.146.51.131) (Ping timeout: 272 seconds) |
| 15:04:13 | benin09 | is now known as benin0 |
| 15:05:58 | → | dextaa joins (~DV@user/dextaa) |
| 15:06:17 | × | dextaa quits (~DV@user/dextaa) (Read error: Connection reset by peer) |
| 15:06:53 | → | talismanick joins (~talismani@2601:200:c100:3850::dd64) |
| 15:08:19 | → | dextaa joins (~DV@user/dextaa) |
| 15:08:42 | × | dextaa quits (~DV@user/dextaa) (Read error: Connection reset by peer) |
| 15:10:48 | → | dextaa joins (~DV@user/dextaa) |
| 15:12:54 | → | pmarg joins (~pmarg@2a01:799:159f:9b00:36a6:c77c:6059:5758) |
| 15:12:59 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:14:04 | → | zebrag joins (~chris@user/zebrag) |
| 15:15:09 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 15:18:09 | × | ski quits (~ski@ext-1-468.eduroam.chalmers.se) (Ping timeout: 272 seconds) |
| 15:20:03 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Ping timeout: 272 seconds) |
| 15:20:13 | × | maroloccio quits (~marolocci@151.73.134.175) (Quit: WeeChat 3.0) |
| 15:20:58 | → | slack1256 joins (~slack1256@191.126.99.206) |
| 15:24:49 | → | econo joins (uid147250@user/econo) |
| 15:27:23 | <edwardk> | kuribas: that was one thought, but i kind of want the nice haskelly version |
| 15:27:45 | <edwardk> | kuribas: i will admit my maximum likelihood scenario at this moment is just going over to write the code i want in rust instead of haskell |
| 15:29:15 | <edwardk> | i do wish injective type families let me say things like: type Foo x y = z | z x -> y -- having PolyKinds makes the crippled current version of injectivity really bad |
| 15:31:03 | × | alexhandy quits (~trace@user/trace) (Read error: Connection reset by peer) |
| 15:31:04 | × | Vajb quits (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) (Read error: Connection reset by peer) |
| 15:31:14 | → | alexhandy joins (~trace@user/trace) |
| 15:31:57 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) |
| 15:32:06 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 15:32:45 | × | dsrt quits (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 244 seconds) |
| 15:34:17 | → | alexhandy2 joins (~trace@user/trace) |
| 15:34:53 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.5) |
| 15:35:37 | → | troydm joins (~troydm@host-176-37-124-197.b025.la.net.ua) |
| 15:35:48 | × | alexhandy quits (~trace@user/trace) (Ping timeout: 260 seconds) |
| 15:36:21 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 15:41:30 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 15:46:17 | → | zmt00 joins (~zmt00@user/zmt00) |
| 15:49:03 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 15:49:49 | × | jgeerds quits (~jgeerds@55d437cf.access.ecotel.net) (Ping timeout: 272 seconds) |
| 15:50:01 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 15:50:10 | <dextaa> | Can someone help me out understanding this compiler error message? https://paste.tomsmeding.com/Wae5P1sR |
| 15:53:01 | <edwardk> | dextaa: guessing buildinEnv is just a value not an m (something)? |
| 15:53:16 | <edwardk> | does |
| 15:53:23 | <edwardk> | initInterpreterState = InterpreterState builtinEnv <$> newIORef Seq.empty |
| 15:53:24 | <edwardk> | work? |
| 15:53:31 | <kuribas> | dextaa: InterpreterState has only one argument? |
| 15:53:43 | × | vglfr quits (~vglfr@88.155.25.62) (Remote host closed the connection) |
| 15:54:02 | <edwardk> | and if not what are the types of builtinEnv and InterpreterState ? |
| 15:54:04 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 15:54:24 | <kuribas> | data InterpreterState = InterpreterState { isEnv :: Env } |
| 15:54:24 | → | vglfr joins (~vglfr@88.155.25.62) |
| 15:54:34 | <kuribas> | initInterpreterState = InterpreterState <$> builtinEnv <*> newIORef Seq.empty |
| 15:55:04 | <edwardk> | oh interpreterState doesn't carry around any IORef at all |
| 15:55:13 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 15:55:24 | <kuribas> | I think he forgot to add it... |
| 15:55:31 | <geekosaur> | yes, this appears very confused |
| 15:55:39 | × | vglfr quits (~vglfr@88.155.25.62) (Remote host closed the connection) |
| 15:55:46 | <edwardk> | builtinEnv :: IO Env; builtinEnv = return Map.empty -- seems pretty heavy, why bother requiring that to be in IO? |
| 15:55:54 | → | vglfr joins (~vglfr@88.155.25.62) |
| 15:56:02 | <edwardk> | it may have had to be when there was some sequence in there and what not |
| 15:56:06 | <edwardk> | but not any more |
| 15:56:08 | <dextaa> | kuribas: right, removed it. I'm very confused indeed. following the crafting interpreters book but the env stuff i'm shopping around tutorials :P |
| 15:56:13 | <edwardk> | guessing this code was partially refactored and never finished |
| 15:56:15 | <dextaa> | from here https://abhinavsarkar.net/posts/implementing-co-2/#running-a-program |
| 15:57:57 | <edwardk> | ExceptT RuntimeExcept (ContT (Either RuntimeExcept ()) (StateT InterpreterState IO)) a -- is quite complex. |
| 15:58:12 | <maerwald[m]> | edwardk: how do you like rust? |
| 15:58:15 | → | emergence joins (emergence@2607:5300:60:5910:dcad:beff:feef:5bc) |
| 15:58:25 | <edwardk> | maerwald[m]: i hate it, i love it, some times both at the same time |
| 15:58:32 | <kuribas> | dextaa: there are some greyed out code lines... |
| 15:59:50 | <maerwald[m]> | edwardk: simple things sometimes need extraordinary ceremony. Like... a for loop :p |
| 16:00:21 | <kuribas> | maerwald[m]: so... like haskell? :-O |
| 16:00:45 | <dextaa> | kuribas: in that blog article? The toy language I am building is different to it, I was just using the blog article as reference for the saving environment state part, but yes It's a bit over complicated for my beginner mind |
| 16:02:26 | <maerwald[m]> | kuribas: i think on average, rust is more verbose than haskell. By a lot |
| 16:02:40 | <kuribas> | maerwald[m]: I don't think haskell is verbose. |
| 16:02:55 | <kuribas> | In my experience it's even less verbose than clojure, with types and all. |
| 16:03:16 | <kuribas> | People just see a lot of types, and think it's verbose. |
| 16:03:42 | × | indigo_ibs quits (~user@31.124.106.79) (Ping timeout: 276 seconds) |
| 16:03:43 | <kuribas> | Because they think the types are redundant, while they aren't. |
| 16:04:29 | <maerwald[m]> | I didn't say Haskell is verbose |
| 16:05:07 | <kuribas> | maerwald[m]: right. |
| 16:05:21 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 16:05:51 | <geekosaur> | that could actually be taken that way, but it'd be distinguished by tone of voice. which doesn't get conveyed over irc (or slack, discord, etc.) well |
| 16:06:08 | <kuribas> | maerwald[m]: someone explained parsers in rust to me, i wasn't impressed :) But then I think the goals of haskell and rust are different. |
| 16:06:24 | <maerwald[m]> | I do think rust is a safer bet business wise or for hiring. I also enjoyed it a couple years ago. But it never quite felt at home |
| 16:06:32 | <geekosaur> | I think rust is trying to be a better C, not a worse Haskell |
| 16:07:00 | <kuribas> | indeed |
| 16:07:31 | <maerwald[m]> | geekosaur: there are certainly competing forces in the rust ecosystem. But maybe less than in Haskell |
| 16:08:01 | <maerwald[m]> | It seems to be more focussed on becoming a serious compiler |
| 16:08:13 | <kuribas> | ocaml, f#, idris? |
| 16:08:26 | <edwardk> | maerwald[m]: i like traits, fun fact, they even consulted me when implementing them, because they wanted feedback based on my old 'typeclasses vs. the world' talk. it sure as hell beats SFINAE and C++'s story which is a ratsnest of problems. i am kind of okay with the borrowing ceremony. its tedious, and it rarely catches problems _for me_ but for a team? i could see it helping a lot pin down contracts. |
| 16:08:47 | <edwardk> | maerwald[m]: i find the macro import and namespacing story horrid. its just a bad design. i really miss C++ variadic templates |
| 16:09:50 | <edwardk> | on the other hand, they have a compiler that gets cross-platform right from day 1. wasm as a first class citizen, so many backends, the best damn thought through graphics pipeline set anywhere |
| 16:10:17 | <edwardk> | when i look at makepad and compare it to what the haskell equivalent would look like, i cry |
| 16:10:48 | <maerwald[m]> | 9.6 is getting wasm |
| 16:10:55 | <dextaa> | isn't rust just using LLVM so they get those backends for free anyway? |
| 16:11:03 | <edwardk> | yeah but at a _tiny_ bit of overhead relative to rust ;) |
| 16:11:22 | <maerwald[m]> | It may be usable in 5 years from now :p |
| 16:12:17 | <edwardk> | dextaa: free is relative. there's been a lot of work put into handling wasm well, handling compiling for spir-v for shaders. |
| 16:12:17 | <kuribas> | I am hoping idris will be a more efficient haskell for some targets, due to being strict.... |
| 16:12:21 | <kuribas> | like javascript. |
| 16:12:32 | <kuribas> | or wasm |
| 16:12:34 | <maerwald[m]> | dextaa: GHC can do that too... the first M1 support release used that trick |
| 16:12:34 | <Rembane> | Purescript is quite good in that regard. |
| 16:12:35 | <edwardk> | ghc can use llvm on the backend for large chunks of itself, but will never run in spir-v |
| 16:13:02 | <dextaa> | edwardk: ah ok |
| 16:13:59 | <edwardk> | i mention spir-v because for makepad it means they write the front end, _and_ all the shaders in rust, making a very unified experience, where doing so in haskell i'd be writing a ton of EDSLs, or maybe using compiling to categories badly |
| 16:14:54 | danso_o | is now known as danso |
| 16:14:56 | × | alexhandy2 quits (~trace@user/trace) (Read error: Connection reset by peer) |
| 16:15:15 | → | alexhandy joins (~trace@user/trace) |
| 16:16:14 | × | ccntrq quits (~Thunderbi@2a01:c23:8c77:3a00:6188:64f1:5d2d:a884) (Remote host closed the connection) |
| 16:17:56 | × | coot quits (~coot@213.134.190.95) (Quit: coot) |
| 16:21:31 | × | mbuf quits (~Shakthi@122.165.55.71) (Quit: Leaving) |
| 16:22:20 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 16:23:12 | → | Guest34 joins (~Guest34@2605:a601:a615:f600:b98b:a0a1:7db6:362) |
| 16:25:40 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 16:26:40 | × | zxx7529 quits (~Thunderbi@user/zxx7529) (Quit: zxx7529) |
| 16:28:22 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:32:32 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:33:02 | × | kuribas quits (~user@silversquare.silversquare.eu) (Quit: ERC (IRC client for Emacs 26.3)) |
| 16:33:25 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 16:34:22 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 16:34:50 | <Guest34> | Can anyone explain to me what is the role of `Functor1` in `Representable` 's `cotraverse1` ? |
| 16:34:50 | <Guest34> | ( `cotraverse1 :: (Representable m, Functor1 w) => (w Identity -> a) -> w m -> m a` ) |
| 16:34:51 | <Guest34> | ( `class Functor1 w where map1 :: (forall a. f a -> g a) -> w f -> w g` ) |
| 16:35:06 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 16:37:18 | × | MajorBiscuit quits (~MajorBisc@wlan-145-94-167-213.wlan.tudelft.nl) (Ping timeout: 240 seconds) |
| 16:37:33 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 16:37:34 | → | Cajun joins (~Cajun@user/cajun) |
| 16:44:38 | × | vglfr quits (~vglfr@88.155.25.62) (Ping timeout: 260 seconds) |
| 16:47:12 | <c_wraith> | Guest34: it's a higher-order version of Functor. |
| 16:48:59 | × | dostoevsky quits (~5c42c5384@user/dostoevsky) (Quit: Ping timeout (120 seconds)) |
| 16:49:28 | → | dostoevsky joins (~5c42c5384@user/dostoevsky) |
| 16:51:37 | <c_wraith> | Functor is a class over types with kind (Type -> Type). Functor1 is class over types with kind (Type -> Type) -> Type |
| 16:53:58 | × | gurkenglas quits (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 16:55:49 | → | waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 16:58:53 | → | kenran joins (~kenran@200116b82b758c00ea3f33dad92dd6ae.dip.versatel-1u1.de) |
| 16:59:44 | <Guest34> | Thanks, that's a good explanation of Functor1. Do you know why it's necessary for defining efficient operations that evaluate a Representable functor at multiple indices? |
| 16:59:48 | × | kenran quits (~kenran@200116b82b758c00ea3f33dad92dd6ae.dip.versatel-1u1.de) (Client Quit) |
| 17:04:13 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 17:05:03 | × | benin0 quits (~benin@183.82.29.162) (Quit: The Lounge - https://thelounge.chat) |
| 17:05:37 | × | jespada quits (~jespada@cpc121022-nmal24-2-0-cust171.19-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com) |
| 17:05:49 | <edwardk> | Guest34: i can maybe speak to that |
| 17:06:02 | × | PiDelport quits (uid25146@id-25146.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:06:11 | <edwardk> | Guest34: i'm not sure which version of Representable you took that from |
| 17:07:18 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) (Ping timeout: 240 seconds) |
| 17:07:18 | <edwardk> | but the short version is, having that notion rather than just tabulate and index allows things like 'Moore' machines to avoid having to walk all the way in and out of the functor. and it allows types where you use the type parameter at multiple 'f's to common up shapes. |
| 17:07:44 | <edwardk> | data Moore a b = Moore b (a -> Moore a b) -- is a representable functor, it is represented by [a] |
| 17:07:58 | → | Vajb joins (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) |
| 17:08:10 | <edwardk> | but if you have to use tabulate and index, it corresponds to giving up and starting over from the original machine feeding it a's until you select out a b. |
| 17:08:19 | <edwardk> | this is asymptotically less efficient than walking down one level at a time |
| 17:08:35 | <edwardk> | which scatter or cotraverse1 or whatever its called in that version does |
| 17:08:43 | <edwardk> | now consider something like |
| 17:09:06 | <edwardk> | newtype Person f = Person { age :: f Int, name :: f String } |
| 17:09:23 | <edwardk> | without that its quite difficult to automatically generate the instance that does the right thing, pulling the 'f's out of Person |
| 17:09:38 | <edwardk> | you want to take Person f -> f (Person ???) where ??? gets filled in with Identity |
| 17:10:11 | <edwardk> | and you can see that as exploiting the fact that 'f' is representable to know it has a common shape for all occurrences, despite what arguments are packed into it |
| 17:10:22 | → | dknite joins (~dknite@49.37.45.188) |
| 17:10:53 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 17:10:57 | <Guest34> | Oh, that's nice. So then you get a structure that can represent the data directly, or a diff, or even a database access, and you can manipulate them all in a consistent way. |
| 17:10:59 | <edwardk> | this is important, because without this Functor1 version of things, you don't get just from the distributive law a canonical implementation of index/tabulate. you have to bolt them on by hand, but _with_ this operation you can define tabulate and index once and for all for all representable functors |
| 17:11:19 | <edwardk> | and you can use it to derive Applicative, the reader-like Monad instance, MonadFix, all the things |
| 17:12:12 | <edwardk> | https://github.com/ekmett/distributive/blob/main/src/Data/Rep/Internal.hs#L156 is my preferred version of this idea |
| 17:12:28 | <edwardk> | the class you gave above is actually pretty bad, because it doesn't work with GeneralizedNewtypeDeriving |
| 17:12:36 | <edwardk> | the version with scatter that i showed does |
| 17:13:21 | <edwardk> | but using the data type i define as Dist f a here: https://github.com/ekmett/distributive/blob/main/src/Data/Rep/Internal.hs#L590 you can derive a crapload of instances for free for any representable functor and they get efficient implementations using scatter. |
| 17:14:06 | <Guest34> | OK, I was looking in your adjunctions repo. This one directly gives a lot more information about the type. |
| 17:14:14 | <edwardk> | https://github.com/ekmett/distributive/blob/main/src/Data/Machine/Moore.hs#L42 |
| 17:14:21 | → | vglfr joins (~vglfr@88.155.25.62) |
| 17:14:26 | <edwardk> | shows a bunch of instances being defined just from Dist using DerivingVia |
| 17:14:49 | <edwardk> | my goal is/was to go through and refactor the entire package hierarchy i have on top of this new version of Distributive |
| 17:15:19 | <edwardk> | because it shows that Distributive built off of Functor1 is powerful enough to replicate Representable |
| 17:16:07 | <edwardk> | and then i go through and use generics to derive nice versions of this that either use simple counters like Fin n to index the type or use generics when there's infinite cases or use whatever you wrote by hand for tabulate and index while still offering a fast generic scatter |
| 17:16:34 | <Guest34> | Very cool. This seems a lot more satisfying. |
| 17:16:57 | <edwardk> | the refactored HKD package offers an F1 data type that lets GHC.Generics define the rest of this stuff |
| 17:17:09 | <edwardk> | https://github.com/ekmett/hkd |
| 17:17:18 | <edwardk> | you'd need to build off repos though |
| 17:17:37 | <edwardk> | as its not on hackage and i'll confess i've yet to refactor the top of my package hierarchy to be compatible |
| 17:17:43 | <edwardk> | i need to take a week or and just code or something |
| 17:18:26 | → | dsp joins (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 17:19:38 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 17:20:53 | <Guest34> | Thanks, I'll take a look and try to understand how it all fits together. |
| 17:21:24 | → | jgeerds joins (~jgeerds@55d437cf.access.ecotel.net) |
| 17:22:51 | <edwardk> | let me know if you have questions. it is a bit of a rube goldberg machine |
| 17:23:09 | <edwardk> | the major selling points are the Record type which lets you generically write |
| 17:23:30 | <edwardk> | Record '[Int,String] f -- and builds a vector backed version of Person above. |
| 17:23:56 | <edwardk> | and the usecases for it for me are mostly around turning row-stores into column stores. because Person f -- for a representable f is a column store, and f (Person Id) is a row store |
| 17:24:24 | <edwardk> | in Person f we have a functor full of ages and one full of names and we have to zip the parts we want |
| 17:24:34 | <edwardk> | in f (Person Id) we're fully zipped with everything, whether we want it or not |
| 17:25:20 | <edwardk> | it does do some evil evil things to get unpackable Fin's and Variants. |
| 17:26:23 | → | dsrt joins (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 17:26:23 | <edwardk> | my intention when i go to finish it is to package up the modified profunctor package, and then rebuild the remaining packages i have on top of the changed over base, the problem is it commutes a _lot_ of my dependencies, so its a big major version bump across the entire ecosystem |
| 17:27:24 | <Guest34> | How much of this applies to representable profunctors? |
| 17:27:32 | <edwardk> | yes |
| 17:27:35 | <edwardk> | =) |
| 17:27:40 | <edwardk> | thats also part of the refactor |
| 17:27:59 | <edwardk> | part of the profunctors package including all the closed stuff move into distributive in the refactor |
| 17:28:39 | <edwardk> | representability for profunctors is a bit trickier though, because the basis 'a' is part of the p type so you don't get to use it much |
| 17:28:52 | <edwardk> | you do get to use it in closed profunctors though |
| 17:29:06 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 17:29:30 | <edwardk> | right now it gives p a b -> p (x -> a) (x -> b) -- but the x -> can be turned into a representable functor with representation x |
| 17:29:35 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 17:29:39 | <edwardk> | then we can look at doing the same trick |
| 17:30:49 | → | abhixec joins (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) |
| 17:30:59 | <edwardk> | e.g. can we turn something like p (u Id) (u Id) -> p (u f) (u f) ? -- for Functor1 u, Representable f? |
| 17:31:04 | <Guest34> | Like the Rep-based Reader? The new type would be `p a b -> m a -. m b` ? |
| 17:31:05 | <edwardk> | afk a bit |
| 17:31:18 | <Guest34> | Got it, thanks again |
| 17:31:48 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 17:33:13 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 17:34:50 | → | gurkenglas joins (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) |
| 17:36:26 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 17:37:29 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 17:38:28 | × | phma quits (~phma@host-67-44-208-203.hnremote.net) (Read error: Connection reset by peer) |
| 17:39:27 | → | phma joins (phma@2001:5b0:211c:eca8:4705:335b:2d2:d9c2) |
| 17:44:43 | × | kjak quits (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) (Ping timeout: 260 seconds) |
| 17:45:00 | → | kjak joins (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) |
| 17:46:28 | × | abhixec quits (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 17:47:20 | → | codaraxis joins (~codaraxis@user/codaraxis) |
| 17:47:43 | → | abhixec joins (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) |
| 17:49:16 | <Profpatsch> | Is a ~ [Int] the only way to “let bind” a type? |
| 17:49:30 | <monochrom> | I think yes. |
| 17:49:50 | <Profpatsch> | I’m thinking about having the return type of a postgresql query *above* the SELECT |
| 17:49:58 | <monochrom> | Haha |
| 17:50:00 | <Profpatsch> | So that it’s obvious what the binding is |
| 17:50:18 | <monochrom> | I don't think of ~ as type-level let binding, but it does have that effect in retrospect. |
| 17:50:20 | <Profpatsch> | But naively binding it against a proxy (my first idea) is not the best |
| 17:50:33 | <monochrom> | People usually write type synonyms instead. |
| 17:51:14 | <Profpatsch> | monochrom: Haskell is a very good functional language with a very questionable relational language tucked to the side of it |
| 17:51:31 | <Bulby[m]> | what is a relational language |
| 17:51:48 | <Profpatsch> | Bulby[m]: prolog for example |
| 17:51:53 | <geekosaur[m]> | Anyone remember Quel? |
| 17:51:59 | <Bulby[m]> | i don't write prolog |
| 17:54:10 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:54:38 | × | gurkenglas quits (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 17:55:26 | <Profpatsch> | but there’s no way if I have a (Proxy a) in hand to “pass” the a to another binding? |
| 17:55:35 | <Profpatsch> | apart from doing the ~ in the function sig |
| 17:55:37 | <heath> | [exa]: re: package definining algebraic structures and how "efficient"... "should be able to deal with matrix dimensions in the 100s or 1000s |
| 17:55:49 | <heath> | "I've started using hmatrix and so far i'm pretty happy with it. Another option i found was the package linear, but it seems like it was aimed at low dimensional (3 or 4) stuff ?" |
| 17:56:49 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:01:02 | <[exa]> | yeah linear is a bit more towards the 3d graphics math |
| 18:01:16 | × | dsp quits (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Quit: Leaving) |
| 18:05:53 | → | gurkenglas joins (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) |
| 18:07:10 | × | elkcl quits (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) (Ping timeout: 240 seconds) |
| 18:07:34 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:07:56 | → | elkcl joins (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) |
| 18:08:35 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 18:11:01 | → | ski joins (~ski@ext-1-468.eduroam.chalmers.se) |
| 18:16:12 | × | dsrt quits (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Remote host closed the connection) |
| 18:17:23 | × | jgeerds quits (~jgeerds@55d437cf.access.ecotel.net) (Ping timeout: 272 seconds) |
| 18:17:32 | → | lottaquestions joins (~nick@S0106a84e3f794893.ca.shawcable.net) |
| 18:25:43 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 18:28:54 | × | talismanick quits (~talismani@2601:200:c100:3850::dd64) (Ping timeout: 264 seconds) |
| 18:29:57 | <amonowy> | Hi! I'm looking for someone to review my first Haskell project. I was learning while working on it. It has 1700 loc and is simple Trello terminal client. If you want to do few iterations with me I'll be happy to pay 50$/h. You can check it here https://gitlab.com/amonowy/haskello/-/tree/cursor-refactor |
| 18:34:07 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:37:13 | <dextaa> | Could someone help out with my (subsequent) compile error? :P https://paste.tomsmeding.com/0MsmLb3t |
| 18:38:50 | <[exa]> | amonowy: looks cool tbh, pretty clean & understandable as far as I click (randomly) |
| 18:39:33 | <geekosaur> | dextaa, your defineVarEnv is in InterpreterEnv, but it needs to be in IO for you to use newIORef |
| 18:39:41 | <ski> | dextaa : `valueRef <- liftIO (newIORef val)' ? |
| 18:40:03 | <[exa]> | amonowy: anything specific for feedback? I noticed you manage the state manually, could be interesting to try out actual monadic State and lenses; it gives much simpler updates :] |
| 18:40:17 | → | enthropy joins (~enthropy@24-246-69-9.cable.teksavvy.com) |
| 18:41:02 | <[exa]> | amonowy: also try running hlint on the source, it has good hints. (e.g. this https://gitlab.com/amonowy/haskello/-/blob/cursor-refactor/src/State/AppState.hs#L92 might be concatMap if I get it right) |
| 18:42:37 | <dextaa> | geekosaur, ski : thanks. Don't see how the code i'm basing mine off compiled without that but oh well ¯\_(ツ)_/¯ |
| 18:43:23 | <geekosaur> | mm, didn't you say earlier you'd taken that part from blog posts? those may simply have been in IO with the state in an IORef or something |
| 18:44:00 | <geekosaur> | which is not a preferred way of writing things, but would work at least if you were going for a more procedural feel |
| 18:44:40 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:46:00 | <dextaa> | Seems the same https://abhinavsarkar.net/code/co-interpreter.html |
| 18:46:01 | <amonowy> | Thanks [exa] ! I tried to use simplest constructs to understand it better. Will give it a try with your suggestions! There is this io func that is crucial to sync with server. I use recursive monadic bind. Wonder if there is typeclas I can use to make it terser https://gitlab.com/amonowy/haskello/-/blob/cursor-refactor/src/Event.hs#L407 |
| 18:46:06 | <[exa]> | amonowy: outright lens sploier: addCards cs = listCards %~ (cs++) |
| 18:46:20 | <[exa]> | hm lemme check |
| 18:47:22 | <[exa]> | yeah you literally have almost State in there already. `Control.Monad.State` represents the `state -> (result,state)` as a convention for you. |
| 18:48:53 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 18:49:29 | <[exa]> | (like, don't get me wrong, this is probably the best way you could do it without jumping to more advanced haskell :] ) |
| 18:49:39 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 18:49:43 | <amonowy> | I was trying to use it but couldn't find how to iterate until hit end condition |
| 18:49:46 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 18:49:58 | <amonowy> | Like monad transformers? |
| 18:51:09 | × | machinedgod quits (~machinedg@d172-219-86-154.abhsia.telus.net) (Ping timeout: 244 seconds) |
| 18:51:17 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 18:51:20 | <[exa]> | yeah transformers combine the monadic stuff, that your type you have there would be equivalent to `StateT AppState IO Bool` |
| 18:51:31 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 18:51:52 | <[exa]> | you know about how functors work? |
| 18:52:56 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 18:53:05 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 18:53:50 | → | gmg joins (~user@user/gehmehgeh) |
| 18:54:57 | <[exa]> | amonowy: btw there's this https://hackage.haskell.org/package/extra-1.7.10/docs/Control-Monad-Extra.html#v:whileM (and a few other helpful combinators-- I guess one of them would fit into your saveStateToServer?) |
| 18:54:58 | × | slack1256 quits (~slack1256@191.126.99.206) (Read error: Connection reset by peer) |
| 18:55:38 | <amonowy> | I think I do although I'm not sure if enough |
| 18:55:42 | → | slack1256 joins (~slack1256@186.11.84.89) |
| 18:55:51 | <Guest34> | It's good to understand state transformers, but sometimes it's more flexible to just use `withFoo` bracketing functions directly, no monads except IO. |
| 18:55:54 | <amonowy> | Thanks will check that as well |
| 18:56:41 | × | pmarg quits (~pmarg@2a01:799:159f:9b00:36a6:c77c:6059:5758) (Remote host closed the connection) |
| 18:56:41 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:56:46 | <[exa]> | amonowy: btw where's the recursion in that funciton? (not sure if I spotted it) |
| 18:58:21 | <amonowy> | Sorry it in function called by saveStateToServer https://gitlab.com/amonowy/haskello/-/blob/cursor-refactor/src/Event.hs#L437 |
| 18:59:23 | × | vglfr quits (~vglfr@88.155.25.62) (Ping timeout: 260 seconds) |
| 19:01:51 | <[exa]> | amonowy: you could probably simplify that a bit -- you're passing it a (trivial) IO action that just returns the SyncedChanges, but I guess there's no reason because it can live just with the data |
| 19:01:55 | <[exa]> | lemme try |
| 19:05:30 | → | nschoe joins (~quassel@2a01:e0a:8e:a190:5f4c:d84e:12c7:8ba) |
| 19:05:37 | <[exa]> | amonowy: https://paste.tomsmeding.com/iV2T83MZ |
| 19:05:53 | <[exa]> | (no guarantees, I just wrote it) |
| 19:06:13 | <[exa]> | (ie right should be Right... :D ) |
| 19:08:41 | → | mikoto-chan joins (~mikoto-ch@dzw9kf47j-sy--ghcbk-4.rev.dnainternet.fi) |
| 19:12:11 | <amonowy> | Awesome, nice one. I like how you get rid of superfluous 'return' calls |
| 19:13:23 | → | Everything joins (~Everythin@37.115.210.35) |
| 19:15:01 | → | coot joins (~coot@213.134.190.95) |
| 19:19:59 | → | seriously joins (~seriously@ool-18bd55d4.dyn.optonline.net) |
| 19:20:09 | <seriously> | hey gentleman... |
| 19:20:39 | <seriously> | Working on histogram problem in cis194 ... |
| 19:21:11 | <seriously> | just about finished... it it possible to use a variable within a list comprehension? |
| 19:21:29 | <seriously> | e.g. [maxOccurs..(-1)] |
| 19:21:57 | <geekosaur> | sure |
| 19:22:12 | → | machinedgod joins (~machinedg@184.68.124.102) |
| 19:22:13 | <geekosaur> | but if you intend that to count down, you have to say that |
| 19:22:23 | ← | Everything parts (~Everythin@37.115.210.35) () |
| 19:22:44 | <geekosaur> | [maxOccurs, maxOccurs - 1 .. -1] |
| 19:22:52 | <geekosaur> | otherwise it counts up |
| 19:23:02 | <seriously> | ok so yeah im trying to countdown from this dynamic variable to -1 |
| 19:23:10 | <ski> | seriously : fwiw, that's an enumeration, not a list comprehension |
| 19:23:26 | <geekosaur> | enumerations expand to normal functions, btw |
| 19:23:26 | <ski> | > [9 .. 0] |
| 19:23:28 | <lambdabot> | [] |
| 19:23:31 | <ski> | > [9,8 .. 0] |
| 19:23:33 | <lambdabot> | [9,8,7,6,5,4,3,2,1,0] |
| 19:23:51 | <geekosaur> | enumFrom, enumFromTo, enumFromThenTo |
| 19:23:51 | <seriously> | yes thats what im seeing now ski geekosaur |
| 19:24:15 | <ski> | `[9,8 .. 0]' is desugared to `enumFromThenTo 9 8 0' |
| 19:24:57 | <ski> | (there's also `enumFromThen') |
| 19:24:57 | <seriously> | that worked! thx |
| 19:25:20 | <ski> | @src Enum |
| 19:25:20 | <lambdabot> | class Enum a where |
| 19:25:20 | <lambdabot> | succ, pred :: a -> a |
| 19:25:20 | <lambdabot> | toEnum :: Int -> a |
| 19:25:20 | <lambdabot> | fromEnum :: a -> Int |
| 19:25:20 | <lambdabot> | enumFrom :: a -> [a] |
| 19:25:22 | <lambdabot> | enumFromThen, enumFromTo :: a -> a -> [a] |
| 19:25:24 | <lambdabot> | enumFromThenTo :: a -> a -> a -> [a] |
| 19:27:30 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 19:29:45 | × | coot quits (~coot@213.134.190.95) (Quit: coot) |
| 19:30:07 | <EvanR> | Enum. how quaint |
| 19:30:19 | × | EsoAlgo quits (~EsoAlgo@129.146.136.145) (Quit: The Lounge - https://thelounge.chat) |
| 19:30:31 | <EvanR> | and they said a -> a was impossible! |
| 19:30:42 | <tomsmeding> | :t id |
| 19:30:43 | <EvanR> | oops that was a -> b |
| 19:30:43 | <lambdabot> | a -> a |
| 19:31:08 | <tomsmeding> | :t fix id :: a -> b |
| 19:31:09 | <lambdabot> | a -> b |
| 19:31:14 | <EvanR> | that's cheating |
| 19:31:25 | tomsmeding | whistles innocently |
| 19:32:00 | <tomsmeding> | % import Data.Coerce |
| 19:32:00 | <yahb2> | <no output> |
| 19:32:07 | <tomsmeding> | % :info Coercible |
| 19:32:07 | <yahb2> | {- ; Coercible is a special constraint with custom solving rules. ; It is not a class. ; Please see section `The Coercible constraint` ; of the user's guide for details. ; -} ; type role Coercible ... |
| 19:32:13 | <int-e> | :t Unsafe.Coerce.unsafeCoerce |
| 19:32:14 | <tomsmeding> | Sad |
| 19:32:15 | <lambdabot> | a -> b |
| 19:32:37 | <int-e> | :t Data.Coerce.coerce |
| 19:32:38 | <lambdabot> | Coercible a b => a -> b |
| 19:33:19 | → | EsoAlgo joins (~EsoAlgo@129.146.136.145) |
| 19:35:47 | <ski> | @type cast |
| 19:35:48 | <lambdabot> | (Typeable a, Typeable b) => a -> Maybe b |
| 19:37:07 | <Guest34> | > let foo _ = Nothing |
| 19:37:09 | <lambdabot> | <no location info>: error: not an expression: ‘let foo _ = Nothing’ |
| 19:37:22 | <Guest34> | :t const Nothing |
| 19:37:24 | <lambdabot> | b -> Maybe a |
| 19:43:08 | → | pavonia joins (~user@user/siracusa) |
| 19:45:46 | × | EsoAlgo quits (~EsoAlgo@129.146.136.145) (Quit: The Lounge - https://thelounge.chat) |
| 19:47:06 | → | acidjnk_new joins (~acidjnk@p200300d6e7058634ccce5b583b17b980.dip0.t-ipconnect.de) |
| 19:47:17 | → | chomwitt joins (~chomwitt@2a02:587:dc0d:4a00:ae09:5cbc:3a9a:5a89) |
| 19:47:47 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:48:28 | → | EsoAlgo joins (~EsoAlgo@129.146.136.145) |
| 19:48:35 | × | acidjnk quits (~acidjnk@p200300d6e7058634bd1cff6d17bc0490.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 19:49:18 | × | christiansen quits (~christian@83-95-137-75-dynamic.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 19:50:14 | → | Pickchea joins (~private@user/pickchea) |
| 19:50:34 | → | jgeerds joins (~jgeerds@55d437cf.access.ecotel.net) |
| 19:51:06 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:52:22 | <ski> | > let foo _ = Nothing in foo "Guest34" |
| 19:52:23 | <lambdabot> | Nothing |
| 19:54:15 | × | EsoAlgo quits (~EsoAlgo@129.146.136.145) (Quit: The Lounge - https://thelounge.chat) |
| 19:56:58 | → | EsoAlgo joins (~EsoAlgo@129.146.136.145) |
| 19:59:21 | × | machinedgod quits (~machinedg@184.68.124.102) (Ping timeout: 272 seconds) |
| 19:59:33 | → | vglfr joins (~vglfr@46.96.135.38) |
| 20:00:20 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 20:01:24 | → | slac35555 joins (~slack1256@191.125.99.206) |
| 20:03:33 | × | slack1256 quits (~slack1256@186.11.84.89) (Ping timeout: 260 seconds) |
| 20:03:40 | → | coot joins (~coot@213.134.190.95) |
| 20:03:58 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 20:06:16 | <dextaa> | Could someone help me with this subsequent (subsequent) build error https://paste.tomsmeding.com/oA8Vs0B2 ? |
| 20:06:32 | × | _ht quits (~quassel@231-169-21-31.ftth.glasoperator.nl) (Remote host closed the connection) |
| 20:08:07 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 20:08:44 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:08:58 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 20:09:02 | <ski> | i'd call that a type error, not a build error |
| 20:09:13 | <ski> | dextaa : and the solution, again, is `liftIO' |
| 20:09:19 | <geekosaur> | that's going to be the same issue as with the earlier readIORef, namely … that |
| 20:10:21 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 20:10:22 | <ski> | .. >>= liftIO . flip writeIORef value |
| 20:10:41 | → | talismanick joins (~talismani@campus-117-212.ucdavis.edu) |
| 20:10:47 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 20:10:58 | <dextaa> | ah thanks |
| 20:11:10 | <dextaa> | I was trying to use liftIO but in the wrong places apparently :P |
| 20:11:38 | <ski> | not writing in pointless style, at least to begin with, might help there |
| 20:11:49 | × | Cajun quits (~Cajun@user/cajun) (Quit: Client closed) |
| 20:12:03 | <dextaa> | true |
| 20:18:00 | → | Topsi joins (~Topsi@host-88-217-154-179.customer.m-online.net) |
| 20:18:07 | × | Topsi quits (~Topsi@host-88-217-154-179.customer.m-online.net) (Client Quit) |
| 20:20:07 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:20:53 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 272 seconds) |
| 20:21:38 | → | Sgeo_ joins (~Sgeo@user/sgeo) |
| 20:21:42 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 20:21:58 | → | codaraxis__ joins (~codaraxis@user/codaraxis) |
| 20:22:17 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 20:22:17 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 20:22:19 | → | mncheckm joins (~mncheck@193.224.205.254) |
| 20:22:20 | allbery_b | is now known as geekosaur |
| 20:22:27 | × | abhixec quits (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) (Quit: leaving) |
| 20:22:47 | → | sayola joins (~sayola@dslb-088-078-152-210.088.078.pools.vodafone-ip.de) |
| 20:23:11 | → | bontaq` joins (~user@ool-45779fe5.dyn.optonline.net) |
| 20:23:11 | → | EsoAlgo9 joins (~EsoAlgo@129.146.136.145) |
| 20:23:23 | → | elkcl_ joins (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) |
| 20:23:45 | → | sloorush joins (~sloorush@52.187.184.81) |
| 20:24:04 | → | sndr joins (~sander@user/sander) |
| 20:25:00 | → | lottaquestions_ joins (~nick@S0106a84e3f794893.ca.shawcable.net) |
| 20:25:59 | → | cosimone` joins (~user@2001:b07:ae5:db26:57c7:21a5:6e1c:6b81) |
| 20:26:04 | → | triteraf1ops joins (~triterafl@user/triteraflops) |
| 20:26:30 | → | gurkengl1s joins (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) |
| 20:26:33 | → | pretty_d1 joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 20:26:36 | → | dextaa8 joins (~DV@user/dextaa) |
| 20:26:49 | → | kritzefitz_ joins (~kritzefit@debian/kritzefitz) |
| 20:28:31 | → | kritzefitz__ joins (~kritzefit@212.86.56.80) |
| 20:28:35 | ← | kritzefitz__ parts (~kritzefit@212.86.56.80) () |
| 20:28:44 | → | Alex_test_ joins (~al_test@178.34.160.206) |
| 20:29:50 | × | kritzefitz quits (~kritzefit@debian/kritzefitz) (Killed (NickServ (GHOST command used by kritzefitz_))) |
| 20:29:57 | kritzefitz_ | is now known as kritzefitz |
| 20:30:16 | × | Guest34 quits (~Guest34@2605:a601:a615:f600:b98b:a0a1:7db6:362) (Quit: Client closed) |
| 20:30:31 | → | elkcl__ joins (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) |
| 20:30:51 | × | elkcl_ quits (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) (Ping timeout: 276 seconds) |
| 20:31:00 | × | alexhandy quits (~trace@user/trace) (Read error: Connection reset by peer) |
| 20:31:14 | × | seriously quits (~seriously@ool-18bd55d4.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 20:31:15 | × | EsoAlgo quits (~EsoAlgo@129.146.136.145) (*.net *.split) |
| 20:31:15 | × | lottaquestions quits (~nick@S0106a84e3f794893.ca.shawcable.net) (*.net *.split) |
| 20:31:15 | × | elkcl quits (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) (*.net *.split) |
| 20:31:15 | × | gurkenglas quits (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) (*.net *.split) |
| 20:31:15 | × | codaraxis quits (~codaraxis@user/codaraxis) (*.net *.split) |
| 20:31:15 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (*.net *.split) |
| 20:31:15 | × | troydm quits (~troydm@host-176-37-124-197.b025.la.net.ua) (*.net *.split) |
| 20:31:15 | × | dextaa quits (~DV@user/dextaa) (*.net *.split) |
| 20:31:15 | × | shriekingnoise quits (~shrieking@201.212.175.181) (*.net *.split) |
| 20:31:15 | × | Sgeo quits (~Sgeo@user/sgeo) (*.net *.split) |
| 20:31:15 | × | Alex_test quits (~al_test@178.34.160.206) (*.net *.split) |
| 20:31:15 | × | bontaq quits (~user@ool-45779fe5.dyn.optonline.net) (*.net *.split) |
| 20:31:15 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (*.net *.split) |
| 20:31:15 | × | Tuplanolla quits (~Tuplanoll@91-159-69-97.elisa-laajakaista.fi) (*.net *.split) |
| 20:31:15 | × | `2jt quits (~jtomas@141.red-88-17-65.dynamicip.rima-tde.net) (*.net *.split) |
| 20:31:15 | × | hiredman quits (~hiredman@frontier1.downey.family) (*.net *.split) |
| 20:31:15 | × | triteraflops quits (~triterafl@user/triteraflops) (*.net *.split) |
| 20:31:15 | × | wagle quits (~wagle@quassel.wagle.io) (*.net *.split) |
| 20:31:16 | × | mzan quits (~quassel@mail.asterisell.com) (*.net *.split) |
| 20:31:16 | × | brettgilio quits (~brettgili@c9yh.net) (*.net *.split) |
| 20:31:16 | × | In0perable quits (~PLAYER_1@fancydata.science) (*.net *.split) |
| 20:31:16 | × | rush quits (~sloorush@52.187.184.81) (*.net *.split) |
| 20:31:16 | × | sander quits (~sander@user/sander) (*.net *.split) |
| 20:31:16 | × | neightchan quits (~nate@98.45.169.16) (*.net *.split) |
| 20:31:16 | × | zaquest quits (~notzaques@5.130.79.72) (*.net *.split) |
| 20:31:16 | × | sayola1 quits (~sayola@dslb-088-078-152-210.088.078.pools.vodafone-ip.de) (*.net *.split) |
| 20:31:16 | × | cosimone quits (~user@93-44-186-171.ip98.fastwebnet.it) (*.net *.split) |
| 20:31:16 | × | sagax quits (~sagax_nb@user/sagax) (*.net *.split) |
| 20:31:16 | × | mjs2600 quits (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) (*.net *.split) |
| 20:31:16 | × | foul_owl quits (~kerry@23.82.194.109) (*.net *.split) |
| 20:31:16 | × | mncheck quits (~mncheck@193.224.205.254) (*.net *.split) |
| 20:31:16 | EsoAlgo9 | is now known as EsoAlgo |
| 20:31:16 | sndr | is now known as sander |
| 20:31:17 | elkcl__ | is now known as elkcl |
| 20:32:14 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 20:32:15 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 20:32:34 | → | califax joins (~califax@user/califx) |
| 20:33:04 | → | machinedgod joins (~machinedg@d172-219-86-154.abhsia.telus.net) |
| 20:34:54 | → | rustisafungus joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 20:34:54 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 20:34:54 | → | troydm joins (~troydm@host-176-37-124-197.b025.la.net.ua) |
| 20:34:54 | → | shriekingnoise joins (~shrieking@201.212.175.181) |
| 20:34:54 | → | `2jt joins (~jtomas@141.red-88-17-65.dynamicip.rima-tde.net) |
| 20:34:54 | → | In0perable joins (~PLAYER_1@fancydata.science) |
| 20:34:54 | → | hiredman joins (~hiredman@frontier1.downey.family) |
| 20:34:54 | → | wagle joins (~wagle@quassel.wagle.io) |
| 20:34:54 | → | mzan joins (~quassel@mail.asterisell.com) |
| 20:34:54 | → | brettgilio joins (~brettgili@c9yh.net) |
| 20:34:54 | → | neightchan joins (~nate@98.45.169.16) |
| 20:34:54 | → | mjs2600 joins (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) |
| 20:35:07 | × | In0perable quits (~PLAYER_1@fancydata.science) (Max SendQ exceeded) |
| 20:35:59 | → | wenjie joins (~nut@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 20:36:04 | × | mikoto-chan quits (~mikoto-ch@dzw9kf47j-sy--ghcbk-4.rev.dnainternet.fi) (Read error: Connection reset by peer) |
| 20:36:18 | <wenjie> | anyone familiar with brick tui library? anyway to make a txt widget scrollable? |
| 20:36:23 | → | Inoperable joins (~PLAYER_1@fancydata.science) |
| 20:36:40 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 20:36:50 | → | zaquest joins (~notzaques@5.130.79.72) |
| 20:37:36 | → | Katarushisu joins (~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net) |
| 20:37:44 | × | vglfr quits (~vglfr@46.96.135.38) (Ping timeout: 255 seconds) |
| 20:38:00 | × | nschoe quits (~quassel@2a01:e0a:8e:a190:5f4c:d84e:12c7:8ba) (Ping timeout: 276 seconds) |
| 20:39:54 | → | Qudit joins (~user@user/Qudit) |
| 20:40:21 | → | foul_owl joins (~kerry@23.82.194.109) |
| 20:40:28 | → | Tuplanolla joins (~Tuplanoll@91-159-69-97.elisa-laajakaista.fi) |
| 20:41:09 | × | biberu quits (~biberu@user/biberu) (Ping timeout: 272 seconds) |
| 20:43:24 | → | Guest|38 joins (~Guest|38@89.253.138.59) |
| 20:44:35 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 20:45:22 | → | pmarg joins (~pmarg@2a01:799:159f:9b00:64d8:8354:ad7c:2411) |
| 20:48:12 | → | biberu joins (~biberu@user/biberu) |
| 20:49:15 | → | sagax joins (~sagax_nb@213.138.71.146) |
| 20:50:14 | → | alexhandy joins (~trace@user/trace) |
| 20:51:56 | × | Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 20:51:59 | → | econo joins (uid147250@user/econo) |
| 20:52:19 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 20:52:23 | → | mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 20:53:14 | → | geschwindingskei joins (~John_Ivan@user/john-ivan/x-1515935) |
| 20:54:53 | <geschwindingskei> | hello haskell community. I'm looking for the equivalent of objects/structs/classes in haskell for describing a model. there's a few concepts here I came across.... Records, DataTypes and Type Classes. I presume these aren't what I'm looking for? |
| 20:55:25 | <Rembane> | geschwindingskei: They are, tell us more about what you're trying to model. |
| 20:55:49 | <Rembane> | geschwindingskei: Having functions that take records as arguments and produce more records is a quite useful set of tools. |
| 20:56:35 | × | talismanick quits (~talismani@campus-117-212.ucdavis.edu) (Ping timeout: 268 seconds) |
| 20:56:38 | × | mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 255 seconds) |
| 20:56:40 | <geschwindingskei> | Rembane, well, since I'm comparing with models in imperative, I guess I'll start simple. A class Car containing various fields, say Colour and Size, of type "string" and "int". And a function to drive(); |
| 20:56:52 | <geschwindingskei> | is what I'm trying to see the equivalent of in Haskell |
| 20:58:43 | → | mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 20:59:38 | × | lottaquestions_ quits (~nick@S0106a84e3f794893.ca.shawcable.net) (Ping timeout: 240 seconds) |
| 20:59:39 | <Guest|38> | Hi guys I ran powershell command in GHCup the page, but it seems not to add stack or ghcup to path |
| 21:00:02 | <Rembane> | geschwindingskei: Something like this: data Car = Car String Int; |
| 21:00:06 | <Rembane> | geschwindingskei: How would you drive that car? |
| 21:00:21 | <Rembane> | geschwindingskei: It has no notion of position, velocity or acceleration. |
| 21:00:26 | → | nosewings joins (~ngpc@cpe-76-186-194-45.tx.res.rr.com) |
| 21:01:05 | <geschwindingskei> | Rembane, just the association of the model/class' function as a private or public member for the function drive(). implementation is not important or any of the sort. I'm just trying to do some comparison. |
| 21:01:33 | <geschwindingskei> | Rembane, is that a record? |
| 21:01:48 | × | coot quits (~coot@213.134.190.95) (Quit: coot) |
| 21:02:14 | <Rembane> | geschwindingskei: Fair enough. We can use my new (patent pending) function: shrink :: Car -> Car; shrink (Car c size) = Car c (div size 2) |
| 21:02:57 | <Rembane> | geschwindingskei: That's not a record, I took a shortcut and made it a datatype without accessor functions. Here's an example of the same thing as a record: data Car = Car { colour :: String, size :: Int } |
| 21:04:31 | <geschwindingskei> | Rembane, reading. I'll ask questions in a moment, trying to figure thing sout. |
| 21:04:34 | <geschwindingskei> | thank you. |
| 21:05:42 | <Rembane> | geschwindingskei: No worries. :) |
| 21:05:47 | Alex_test_ | is now known as Alex_test |
| 21:06:39 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 21:07:30 | <geschwindingskei> | Rembane, what kind of assignment is that under the datatype? |
| 21:08:24 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:10:59 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 21:12:14 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 21:12:16 | <Rembane> | geschwindingskei: It's the syntax for creating a datatype, it's slightly strange but quite useful. |
| 21:16:19 | <geschwindingskei> | Rembane, I see. so, ```Car = Car String Int``` - where and how would one define a constructor for this? |
| 21:16:31 | <Rembane> | geschwindingskei: Somewhere in a module. |
| 21:16:55 | <geschwindingskei> | So this would be more of a structure than a class. |
| 21:17:10 | × | cosimone` quits (~user@2001:b07:ae5:db26:57c7:21a5:6e1c:6b81) (Ping timeout: 260 seconds) |
| 21:18:25 | <Rembane> | geschwindingskei: What's the difference between a structure and a class? |
| 21:18:49 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 21:19:12 | <geschwindingskei> | Rembane, accessors, mutators, methods, constructors/destructors and inheritance/oop paradigms. |
| 21:19:22 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 21:19:23 | <geschwindingskei> | structures are merely blobs of data. |
| 21:19:30 | <geschwindingskei> | classes are more complex. |
| 21:19:39 | → | lottaquestions_ joins (~nick@S0106a84e3f794893.ca.shawcable.net) |
| 21:19:57 | <darkling> | And the accessors, mutators, methods, contructors and destructors are just functions that take a structure as a parameter. |
| 21:19:58 | × | rustisafungus quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 21:20:01 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:20:05 | × | fserucas quits (~fserucas@12.64.114.89.rev.vodafone.pt) (Quit: Leaving) |
| 21:20:16 | <geschwindingskei> | darkling, the "self" you mean? |
| 21:20:41 | <darkling> | Exactly. |
| 21:21:00 | <Rembane> | geschwindingskei: Okay, so how would you implement my shrink function in an OOP language? |
| 21:21:03 | × | chomwitt quits (~chomwitt@2a02:587:dc0d:4a00:ae09:5cbc:3a9a:5a89) (Ping timeout: 272 seconds) |
| 21:21:37 | <geschwindingskei> | but there's no sugar syntax to keep/show that this structure strictly has methods associated with it. |
| 21:21:53 | <geschwindingskei> | in other words, I'm asking if there's some sort of "." dot operator to access a class' associated data. |
| 21:21:55 | <geschwindingskei> | \methods |
| 21:22:04 | <geschwindingskei> | is this correct? |
| 21:22:26 | <Rembane> | None at all. |
| 21:22:53 | <geschwindingskei> | right. so let me guess. I would have to append "Car" as the first parameter in all my associated functions |
| 21:23:03 | <geschwindingskei> | ok. got it. |
| 21:23:14 | <darkling> | You've got type declarations on the functions that will tell you if it works on objects of the structure, of course. |
| 21:23:59 | <Rembane> | geschwindingskei: Yes, all functions that should do something with a Car needs to take Car as a parameter. |
| 21:24:00 | <darkling> | You wouldn't necessarily use the first parameter in all cases -- sometimes it makes sense to put a different parameter first (because of currying and partial application of functions) |
| 21:24:25 | <geschwindingskei> | I understood. |
| 21:24:48 | <geschwindingskei> | Okay, and in respect to Records - what kind of assignment is that? I recall there being a particular name for it. |
| 21:24:57 | <geschwindingskei> | Something to do with order of declaration defining parametrization. |
| 21:25:38 | → | talismanick joins (~talismani@2601:200:c100:3850::dd64) |
| 21:26:20 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 21:27:10 | <Rembane> | There's something about it here: https://wiki.haskell.org/Parameter_order |
| 21:28:21 | → | indigo_ibs joins (~user@31.124.106.79) |
| 21:29:55 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 21:30:00 | × | dtman34 quits (~dtman34@c-73-62-246-247.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 21:32:15 | → | dtman34 joins (~dtman34@2601:446:4400:2ad9:50de:fed7:560f:d711) |
| 21:34:11 | <geschwindingskei> | Rembane, not what I'm looking for. I'll post the link here once I come across it. |
| 21:34:55 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:37:54 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 21:39:30 | × | Guest|38 quits (~Guest|38@89.253.138.59) (Ping timeout: 240 seconds) |
| 21:39:59 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 21:40:03 | × | hpc quits (~juzz@ip98-169-32-242.dc.dc.cox.net) (Ping timeout: 272 seconds) |
| 21:41:04 | × | mmhat quits (~mmh@p200300f1c7090757ee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 3.5) |
| 21:41:10 | <geschwindingskei> | Rembane, https://en.wikipedia.org/wiki/Structural_type_system |
| 21:41:12 | <geschwindingskei> | found it. |
| 21:41:18 | → | Guest|38 joins (~Guest|38@89.253.138.59) |
| 21:41:24 | <geschwindingskei> | I suppose this applies more to OCaml than Haskell though. I think. |
| 21:41:43 | × | Guest|38 quits (~Guest|38@89.253.138.59) (Client Quit) |
| 21:42:10 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 21:45:25 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 21:46:18 | × | indigo_ibs quits (~user@31.124.106.79) (Ping timeout: 244 seconds) |
| 21:50:15 | <Rembane> | geschwindingskei: Haskell has a structural type system |
| 21:50:46 | <geschwindingskei> | Rembane, I see. Then that answers a lot about that datatype's definition. |
| 21:50:56 | <geschwindingskei> | Car that is. |
| 21:51:20 | <Rembane> | geschwindingskei: Yes. |
| 21:51:30 | <geschwindingskei> | Then I can take it from here. |
| 21:51:31 | <geschwindingskei> | thanks. |
| 21:52:31 | <Rembane> | No worries. Good luck! :) |
| 21:52:49 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 21:52:55 | × | hsman quits (~hsman@80.95.197.227) (Quit: Client closed) |
| 21:55:02 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 21:55:07 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:56:23 | × | sagax quits (~sagax_nb@213.138.71.146) (Read error: Connection reset by peer) |
| 21:57:47 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Ping timeout: 272 seconds) |
| 21:58:38 | × | shapr quits (~user@2600:4040:2d31:7100:101e:d56a:4512:22d5) (Ping timeout: 240 seconds) |
| 21:59:38 | × | segfaultfizzbuzz quits (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 255 seconds) |
| 21:59:41 | × | enthropy quits (~enthropy@24-246-69-9.cable.teksavvy.com) (Quit: Client closed) |
| 22:00:28 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 22:06:38 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 22:06:39 | × | acidjnk_new quits (~acidjnk@p200300d6e7058634ccce5b583b17b980.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 22:07:07 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:07:31 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 268 seconds) |
| 22:09:49 | × | kjak quits (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) (Ping timeout: 272 seconds) |
| 22:10:35 | × | jgeerds quits (~jgeerds@55d437cf.access.ecotel.net) (Ping timeout: 268 seconds) |
| 22:10:45 | → | kjak joins (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) |
| 22:26:17 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 22:28:36 | → | segfaultfizzbuzz joins (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 22:30:43 | × | ubert quits (~Thunderbi@91.141.39.36.wireless.dyn.drei.com) (Ping timeout: 272 seconds) |
| 22:30:55 | ← | geschwindingskei parts (~John_Ivan@user/john-ivan/x-1515935) (Leaving) |
| 22:34:26 | → | cosimone joins (~user@2001:b07:ae5:db26:57c7:21a5:6e1c:6b81) |
| 22:43:02 | × | pmarg quits (~pmarg@2a01:799:159f:9b00:64d8:8354:ad7c:2411) (Remote host closed the connection) |
| 22:47:54 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 22:48:08 | → | slack1256 joins (~slack1256@191.125.99.212) |
| 22:49:48 | → | slack6215 joins (~slack1256@186.11.84.89) |
| 22:50:13 | × | slack1256 quits (~slack1256@191.125.99.212) (Read error: Connection reset by peer) |
| 22:50:48 | × | slac35555 quits (~slack1256@191.125.99.206) (Ping timeout: 272 seconds) |
| 22:51:43 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 22:51:47 | × | nosewings quits (~ngpc@cpe-76-186-194-45.tx.res.rr.com) (Remote host closed the connection) |
| 22:52:53 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 272 seconds) |
| 22:57:04 | × | `2jt quits (~jtomas@141.red-88-17-65.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 22:57:22 | → | `2jt joins (~jtomas@141.red-88-17-65.dynamicip.rima-tde.net) |
| 23:00:42 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 23:04:19 | × | kjak quits (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) (Remote host closed the connection) |
| 23:04:32 | → | kjak joins (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) |
| 23:08:54 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 23:10:55 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 23:24:15 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 23:28:21 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 272 seconds) |
| 23:30:15 | × | Alex_test quits (~al_test@178.34.160.206) (Ping timeout: 272 seconds) |
| 23:30:15 | × | AlexZenon quits (~alzenon@178.34.160.206) (Ping timeout: 272 seconds) |
| 23:33:04 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 23:33:48 | → | Alex_test joins (~al_test@178.34.160.206) |
| 23:33:48 | → | AlexZenon joins (~alzenon@178.34.160.206) |
| 23:33:52 | → | geschwindig joins (~John_Ivan@user/john-ivan/x-1515935) |
| 23:34:15 | <geschwindig> | Rembane, hello again. I wish to ask - how do you explicitly give function parameters a label? |
| 23:34:47 | <geschwindig> | theFunction :: Int -> IO -- this lacks parameter labels/naming. |
| 23:34:58 | <Rembane> | geschwindig: At the next line usually |
| 23:35:16 | <Rembane> | geschwindig: thefunction someInt = print someInt |
| 23:36:12 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 23:36:17 | <geschwindig> | Rembane, any other syntactic sugar way? |
| 23:36:33 | <geschwindig> | seems a little messy to do that, especially if the function is lengthy. |
| 23:36:43 | <Rembane> | geschwindig: None that I can think of |
| 23:36:50 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds) |
| 23:36:54 | <geschwindig> | Oof |
| 23:37:29 | Lord_of_Life_ | is now known as Lord_of_Life |
| 23:41:12 | <geekosaur> | some people use a record for the parameters and record update syntax to specify them |
| 23:41:27 | → | ph88 joins (~ph88@ip5f5af71f.dynamic.kabel-deutschland.de) |
| 23:41:33 | <geekosaur> | this can go well with Default (but can also lead to that being overused and losing type safety) |
| 23:42:16 | <geekosaur> | instance Default MyParameters where def = … {- … -} foo def {thing = "what"} |
| 23:42:42 | × | Igloo quits (~ian@matrix.chaos.earth.li) (Quit: BIAW) |
| 23:42:48 | <geekosaur> | I dislike Default but can see how it would be attractive |
| 23:43:04 | <geschwindig> | I.... see. thank you. |
| 23:43:33 | <geekosaur> | it also lets you prepackage combinations of parameters (replacing `def`) |
| 23:44:22 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Write error: Connection reset by peer) |
| 23:44:22 | × | califax quits (~califax@user/califx) (Write error: Connection reset by peer) |
| 23:44:22 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Read error: Connection reset by peer) |
| 23:44:22 | × | noteness quits (~noteness@user/noteness) (Read error: Connection reset by peer) |
| 23:44:22 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 23:44:22 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Read error: Connection reset by peer) |
| 23:44:43 | → | noteness joins (~noteness@user/noteness) |
| 23:44:49 | × | pretty_d1 quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 23:44:55 | <geschwindig> | geekosaur, you ever played skyrim? |
| 23:45:03 | <geekosaur> | nope |
| 23:45:13 | × | AlexZenon quits (~alzenon@178.34.160.206) (Ping timeout: 260 seconds) |
| 23:45:17 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 23:45:29 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 23:45:39 | × | lottaquestions_ quits (~nick@S0106a84e3f794893.ca.shawcable.net) (Quit: Konversation terminated!) |
| 23:45:51 | → | califax joins (~califax@user/califx) |
| 23:45:54 | × | AlexNoo quits (~AlexNoo@178.34.160.206) (Ping timeout: 272 seconds) |
| 23:46:05 | × | Alex_test quits (~al_test@178.34.160.206) (Ping timeout: 272 seconds) |
| 23:46:07 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 23:46:21 | <geschwindig> | geekosaur, then here's my reaction to all of your comments in this 30 second video. in particular at 0:10 - https://www.youtube.com/watch?v=pFhCGMW8pPo |
| 23:46:23 | <geschwindig> | :P |
| 23:46:48 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 23:47:09 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 23:49:39 | × | Tuplanolla quits (~Tuplanoll@91-159-69-97.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:49:43 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 23:50:15 | → | AlexNoo joins (~AlexNoo@178.34.160.206) |
| 23:50:17 | → | AlexZenon joins (~alzenon@178.34.160.206) |
| 23:50:24 | × | gurkengl1s quits (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) (Ping timeout: 276 seconds) |
| 23:50:30 | → | Alex_test joins (~al_test@178.34.160.206) |
| 23:55:43 | × | noteness quits (~noteness@user/noteness) (Remote host closed the connection) |
| 23:56:01 | → | noteness joins (~noteness@user/noteness) |
| 23:59:04 | × | zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection) |
All times are in UTC on 2022-07-12.