Logs on 2021-05-31 (liberachat/#haskell)
| 00:00:59 | × | myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 252 seconds) |
| 00:05:47 | → | ku joins (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) |
| 00:06:17 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 00:07:35 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 00:08:16 | <hyiltiz> | hello haskell@libera |
| 00:08:47 | <hyiltiz> | noticed I got banned/kicked from tons of channels from freenode or channels just got silent |
| 00:09:02 | <hyiltiz> | Guess I was behind the pace of the world |
| 00:09:15 | hyiltiz | is now known as YourNick |
| 00:09:53 | <shapr> | hello |
| 00:09:54 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 00:10:08 | <shapr> | yeah, freenode imploded, too bad |
| 00:10:16 | YourNick | is now known as hyiltiz |
| 00:10:43 | → | moet joins (~moet@172.58.35.191) |
| 00:12:17 | <hyiltiz> | now gotta register here I guess |
| 00:14:49 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 00:16:07 | × | hyiltiz quits (~quassel@31.220.5.250) (Quit: hyiltiz) |
| 00:16:55 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 00:18:27 | <sm[m]> | welcome hyiltiz |
| 00:20:10 | → | lavaman joins (~lavaman@98.38.249.169) |
| 00:22:05 | × | sajith quits (~sajith@user/sajith) (Quit: Gone) |
| 00:22:05 | × | nonzen quits (~nonzen@user/nonzen) (Quit: Gone) |
| 00:22:20 | → | nonzen joins (~nonzen@user/nonzen) |
| 00:22:52 | × | Deide quits (~Deide@user/deide) (Quit: Seeee yaaaa) |
| 00:22:52 | → | sajith joins (~sajith@user/sajith) |
| 00:22:55 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 00:24:01 | <chisui> | Is there a good writeup of what actually went down? I only read bits and peaces. |
| 00:24:43 | <sm[m]> | chisui: search for freenode in recent hacker news stories |
| 00:24:56 | <pavonia> | chisui: https://gist.github.com/joepie91/df80d8d36cd9d1bde46ba018af497409 though this doesn't include the "offcial" view |
| 00:29:19 | <chisui> | Thanks. What a clusterfuck |
| 00:30:54 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 00:34:23 | × | dhil quits (~dhil@195.213.192.85) (Ping timeout: 268 seconds) |
| 00:34:46 | × | satai quits (~satai@static-84-42-172-253.net.upcbroadband.cz) (Read error: Connection reset by peer) |
| 00:37:22 | × | moet quits (~moet@172.58.35.191) (Quit: leaving) |
| 00:38:14 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:f131:7ff:d61f:7340) |
| 00:40:46 | × | nonzen quits (~nonzen@user/nonzen) (Quit: Gone) |
| 00:40:46 | × | sajith quits (~sajith@user/sajith) (Quit: Gone) |
| 00:41:00 | → | nonzen joins (~nonzen@user/nonzen) |
| 00:41:33 | → | sajith joins (~sajith@user/sajith) |
| 00:42:10 | × | Athas quits (athas@sigkill.dk) (Ping timeout: 264 seconds) |
| 00:42:22 | → | Athas joins (athas@2a01:7c8:aaac:1cf:885f:6d75:b55f:82a8) |
| 00:48:03 | × | shapr quits (~user@2607:fb90:a90e:1723:1429:b6ec:2d1d:b192) (Remote host closed the connection) |
| 00:48:20 | → | shapr joins (~user@2607:fb90:a90e:1723:c496:c7fd:8ebe:11ee) |
| 00:51:01 | × | bfrk quits (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) (Ping timeout: 268 seconds) |
| 00:52:13 | → | arson joins (~arson@pool-100-36-47-118.washdc.fios.verizon.net) |
| 00:53:01 | <arson> | hello everyone :) first time on irc - would this be a place to ask some questions about if a function I have is similar or related in any way to something that already exists? |
| 00:54:23 | <pavonia> | Welcome! If it is about a Haskell function, sure |
| 00:55:58 | × | shapr quits (~user@2607:fb90:a90e:1723:c496:c7fd:8ebe:11ee) (Ping timeout: 268 seconds) |
| 00:59:08 | → | hmmmas joins (~chenqisu1@183.217.202.217) |
| 01:00:04 | <arson> | Thanks! I have this function, called `tw` for treewalk, which has the basic behavior of allowing you to recurse down a tree (such as an AST), but the caller also passes a function which looks at every node in the tree and can either have `tw` continue processing it, or do it's own processing and return a new node to use in place. This is further |
| 01:00:05 | <arson> | complicated by the fact that the function tw takes in, takes in a callback which is equal to `tw <the function argument>`, to allow for further recursion once it's made it's own new node. I know that makes zero sense, so there's two examples of how you would use the `tw` function at the bottom for manipulating ASTs. For sake of example I have a |
| 01:00:05 | <arson> | couple different ways of implementing this function. code: https://paste.tomsmeding.com/tYODlusU |
| 01:00:34 | <arson> | I'm looking for information about a similar function or concept, or even just a similar typeclass to `TWable` that's used in some way already. |
| 01:02:23 | × | ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Read error: Connection reset by peer) |
| 01:03:21 | × | renzhi quits (~xp@2607:fa49:6500:bc00::e7b) (Ping timeout: 268 seconds) |
| 01:04:28 | → | ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) |
| 01:06:39 | <davean> | arson: Look at recursion schemes |
| 01:07:03 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 272 seconds) |
| 01:07:14 | <pavonia> | It somewhat reminds me of what the uniplate package does |
| 01:07:24 | <davean> | I mean it should because uniplate is based on ... |
| 01:08:05 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 252 seconds) |
| 01:08:17 | × | Guest417 quits (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) (Ping timeout: 268 seconds) |
| 01:09:05 | <pavonia> | Based on what? |
| 01:09:43 | × | fosskers quits (~colin@S0106f0f249642f53.vn.shawcable.net) (Remote host closed the connection) |
| 01:09:47 | <arson> | funny how uniplate also has simple asts as their main example |
| 01:12:37 | <davean> | pavonia: the thing I'd said |
| 01:13:03 | <davean> | https://github.com/passy/awesome-recursion-schemes for a bunch of links |
| 01:13:30 | → | wagle joins (~wagle@quassel.wagle.io) |
| 01:14:17 | <arson> | heh, guess it's not haskell if you don't `{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TemplateHaskell, TypeFamilies #-}` |
| 01:16:03 | × | pbrisbin quits (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) (Ping timeout: 265 seconds) |
| 01:16:04 | <pavonia> | Hhm, I'd say the whole language is more or less based on recursion schemes :p |
| 01:16:28 | <davean> | That seems an odd way to think about it, but you do you |
| 01:19:16 | <davean> | Yah, pretty sure i can't even stretch that to be true |
| 01:23:43 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 268 seconds) |
| 01:25:11 | → | wagle joins (~wagle@quassel.wagle.io) |
| 01:27:35 | × | bontaq quits (~user@ool-18e47f8d.dyn.optonline.net) (Remote host closed the connection) |
| 01:28:56 | → | fosskers joins (~colin@S0106f0f249642f53.vn.shawcable.net) |
| 01:30:12 | → | hylisper joins (~yaaic@111.119.208.67) |
| 01:33:27 | × | sh9 quits (~sh9@softbank060116136158.bbtec.net) (Read error: Connection reset by peer) |
| 01:37:17 | × | xff0x quits (~xff0x@2001:1a81:5252:9d00:f476:7d38:9d5:54c9) (Ping timeout: 268 seconds) |
| 01:38:30 | → | xff0x joins (~xff0x@2001:1a81:528f:3900:ab23:5f87:bcb1:2783) |
| 01:43:28 | → | Guest417 joins (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) |
| 01:46:25 | → | wei2912 joins (~wei2912@112.199.250.21) |
| 01:46:30 | → | sh9 joins (~sh9@softbank060116136158.bbtec.net) |
| 01:48:50 | → | myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net) |
| 01:49:11 | → | renzhi joins (~xp@2607:fa49:6500:bc00::e7b) |
| 02:00:30 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 02:01:50 | × | arson quits (~arson@pool-100-36-47-118.washdc.fios.verizon.net) (Quit: Client closed) |
| 02:03:07 | × | egoist quits (~egoist@186.235.82.52) (Quit: WeeChat 3.1) |
| 02:05:24 | → | hydroxonium joins (uid500654@id-500654.stonehaven.irccloud.com) |
| 02:08:16 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 02:12:09 | → | gbd_628 joins (~gbd_628@c-73-160-244-80.hsd1.nj.comcast.net) |
| 02:15:50 | <gbd_628> | Hi all, I'm getting an odd error when I try to build the latest version of `glib` from Hackage: "Lexical error! The character '#' does not fit here." Full error message: https://paste.tomsmeding.com/EcjZdm60. |
| 02:16:06 | <gbd_628> | I get the same problem with the `cairo` package. Googling led to the recommendation that I try compiling with LANG=C in the shell environment, but that didn't change anything for me. |
| 02:16:46 | <gbd_628> | (Sorry if this isn't really a Haskell question, but I'm not sure what's causing the problem so I don't know where else to ask) |
| 02:17:05 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 264 seconds) |
| 02:17:30 | <davean> | With no particular knowlege I'd bet thats something like a c2hs issue |
| 02:17:40 | <davean> | check if your c2hs is old maybe? |
| 02:18:51 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:19:50 | × | machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 268 seconds) |
| 02:21:33 | <gbd_628> | Sorry, what's c2hs? I have a program called `hsc2hs` as part of my ghc distribution; is that the same thing? It's on version 0.68.7 |
| 02:22:38 | <gbd_628> | Which is the most recent version of it on hackage. I don't have any program called c2hs as part of my haskell installation, it doesn't look liek |
| 02:23:30 | × | chisui quits (~chisui@200116b86647790081989979d16794a1.dip.versatel-1u1.de) (Ping timeout: 250 seconds) |
| 02:29:25 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 02:29:56 | <geekosaur> | that's a c2hs error but the real problem is too new a gcc |
| 02:30:56 | <geekosaur> | https://github.com/haskell/c2hs/issues/268 |
| 02:32:41 | <geekosaur> | and the gtk stuff comes with its own fork of c2hs (gtk2hsc2hs) which it uses to build API descriptions from gtk/glib include files |
| 02:32:47 | × | td_ quits (~td@94.134.91.12) (Ping timeout: 252 seconds) |
| 02:34:33 | → | td_ joins (~td@muedsl-82-207-238-238.citykom.de) |
| 02:35:22 | <gbd_628> | Hmm, okay, I'll downgrade to version 10.x of gcc, hopefully that'll work. Thanks! |
| 02:37:43 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 02:41:00 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Quit: /ragequit) |
| 02:41:07 | × | forell quits (~forell@host-178-216-90-220.sta.tvknaszapraca.pl) (Ping timeout: 265 seconds) |
| 02:41:20 | → | forell joins (~forell@host-178-216-90-220.sta.tvknaszapraca.pl) |
| 02:42:02 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Ping timeout: 268 seconds) |
| 02:42:39 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 268 seconds) |
| 02:45:07 | × | Guest417 quits (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) (Ping timeout: 268 seconds) |
| 02:47:32 | × | sheepduck quits (~sheepduck@2607:fea8:2a60:b700::5d55) (Read error: Connection reset by peer) |
| 02:49:37 | <Axman6> | davean: That recursion schemes link... the first link got me |
| 02:49:45 | → | sheepduck joins (~sheepduck@2607:fea8:2a60:b700::5d55) |
| 02:50:18 | <davean> | Axman6: :) stuck in a loop? |
| 02:51:08 | <Axman6> | I cannot get out D: |
| 02:51:20 | <Axman6> | I just keep learning about recursion schemes! |
| 02:52:04 | <int-e> | to learn about recursion schemes you first have to lear about recusion schemes? |
| 02:52:29 | int-e | keeps dropping letters recently, meh. |
| 02:53:02 | <dy> | Axman6: from a Scala library but this chart is language agnostic and neat |
| 02:53:04 | <dy> | https://github.com/precog/matryoshka/blob/master/resources/recursion-schemes.pdf |
| 02:53:53 | <dy> | Stolen from one of edwardk's blog posts |
| 02:55:04 | × | AgentM quits (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) (Quit: Leaving.) |
| 03:00:32 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 268 seconds) |
| 03:02:39 | <arahael> | Is there an easy way for me to list all the licenses that my project uses? |
| 03:02:41 | → | lbseale joins (~lbseale@ip72-194-54-201.sb.sd.cox.net) |
| 03:02:55 | <arahael> | Including transitively. |
| 03:03:42 | <Axman6> | There are definitely ways to do that... there's a package for command line args and configuration handling which does it automatically, I'll find it |
| 03:06:20 | ← | justsomeguy parts (~justsomeg@user/justsomeguy) (WeeChat 3.0.1) |
| 03:08:06 | × | myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Remote host closed the connection) |
| 03:08:17 | <davean> | Axman6: yes, cabal license check |
| 03:08:24 | → | myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net) |
| 03:09:24 | <arahael> | davean: That's not a recognised command. |
| 03:09:26 | → | Guest417 joins (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) |
| 03:10:20 | <Axman6> | https://hackage.haskell.org/package/configuration-tools is what I've used in the past, it's much more than just alicense check, but you could just use it for that |
| 03:11:08 | <Axman6> | if you scroll to the bottom you can see the output it gives |
| 03:11:31 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 03:12:18 | → | doyougnu joins (~user@c-67-168-253-231.hsd1.or.comcast.net) |
| 03:12:56 | × | vicfred quits (~vicfred@user/vicfred) (Quit: Leaving) |
| 03:16:33 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 268 seconds) |
| 03:18:17 | → | otto_s_ joins (~user@p5de2fbac.dip0.t-ipconnect.de) |
| 03:18:32 | → | ru0mad joins (~ruomad@176.164.105.224) |
| 03:18:59 | × | lbseale quits (~lbseale@ip72-194-54-201.sb.sd.cox.net) (Read error: Connection reset by peer) |
| 03:19:36 | × | ru0mad quits (~ruomad@176.164.105.224) (Client Quit) |
| 03:20:04 | → | ru0mad joins (~ruomad@176.164.105.224) |
| 03:20:18 | → | ikex joins (~ash@user/ikex) |
| 03:21:21 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 03:21:43 | × | otto_s quits (~user@p5de2f103.dip0.t-ipconnect.de) (Ping timeout: 265 seconds) |
| 03:21:45 | → | dyeplexer joins (~dyeplexer@user/dyeplexer) |
| 03:23:57 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 03:24:11 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 03:25:15 | Lord_of_Life_ | is now known as Lord_of_Life |
| 03:28:34 | × | smitop quits (uid328768@user/smitop) (Quit: Connection closed for inactivity) |
| 03:31:21 | × | Erutuon quits (~Erutuon@71-34-10-193.mpls.qwest.net) (Ping timeout: 268 seconds) |
| 03:31:25 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Quit: /ragequit) |
| 03:32:28 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 03:33:34 | → | a6a45081-2b83 joins (~aditya@106.212.79.20) |
| 03:37:46 | → | bilegeek joins (~bilegeek@2600:1008:b06d:65ed:93d7:e6a:a06d:9e4) |
| 03:39:50 | × | mnrmnaugh quits (~mnrmnaugh@pool-96-252-87-182.bstnma.fios.verizon.net) (Ping timeout: 264 seconds) |
| 03:40:30 | → | hexology joins (~hexology@user/hexology) |
| 03:41:00 | → | Erutuon joins (~Erutuon@71-34-10-193.mpls.qwest.net) |
| 03:42:18 | × | radw quits (~radw@user/radw) (Ping timeout: 264 seconds) |
| 03:44:05 | × | ru0mad quits (~ruomad@176.164.105.224) (Ping timeout: 264 seconds) |
| 03:45:03 | → | ru0mad joins (~ruomad@176.164.105.224) |
| 03:48:31 | <edwardk> | dy: is it just me or is the fact that that chart substitutes things with arrows in themon the left hand side of the arrow without respect for precedence disturbing? the algebras are all things that in that position would be pairs but are shown as arrows. (f a -> a) -> (f ~> f) -- etc. |
| 03:49:37 | → | radw joins (~radw@user/radw) |
| 03:52:23 | × | alx741 quits (~alx741@186.178.108.160) (Quit: alx741) |
| 03:52:39 | × | ru0mad quits (~ruomad@176.164.105.224) (Ping timeout: 265 seconds) |
| 03:54:52 | → | BosonCollider joins (~olofs@90-227-86-119-no542.tbcn.telia.com) |
| 03:56:25 | <dy> | edwardk: not just you haha |
| 03:56:38 | × | renzhi quits (~xp@2607:fa49:6500:bc00::e7b) (Ping timeout: 268 seconds) |
| 03:56:41 | <dy> | But it's Scala what do you expect :^p |
| 04:02:19 | × | zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 04:02:38 | × | hendursaga quits (~weechat@user/hendursaga) (Remote host closed the connection) |
| 04:03:05 | → | hendursaga joins (~weechat@user/hendursaga) |
| 04:06:59 | <arahael> | Axman6: Thanks for that. |
| 04:07:34 | <arahael> | Axman6: Unfortunately a bit raw, I think I'll do it by hand this time. (It's just a quick weekend script, effectively) |
| 04:07:54 | → | rk04 joins (~rk04@user/rajk) |
| 04:08:56 | → | ru0mad joins (~ruomad@176.164.105.224) |
| 04:09:35 | <hololeap> | I think you know that you're in the weeds when you start making type-level rose trees and type families that can map over them |
| 04:10:02 | × | BosonCollider quits (~olofs@90-227-86-119-no542.tbcn.telia.com) (Read error: Connection reset by peer) |
| 04:13:57 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 04:20:13 | × | noddy quits (~user@user/noddy) (Quit: WeeChat 3.1) |
| 04:20:32 | → | noddy joins (~user@user/noddy) |
| 04:25:00 | × | ru0mad quits (~ruomad@176.164.105.224) (Ping timeout: 268 seconds) |
| 04:25:48 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 04:31:35 | × | ryantrinkle quits (~ryan@24.229.199.25.res-cmts.sm.ptd.net) (Ping timeout: 252 seconds) |
| 04:31:39 | → | ru0mad joins (~ruomad@176.164.105.224) |
| 04:33:02 | × | ikex quits (~ash@user/ikex) (Ping timeout: 268 seconds) |
| 04:33:35 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 04:36:32 | × | ru0mad quits (~ruomad@176.164.105.224) (Ping timeout: 252 seconds) |
| 04:36:43 | → | lu joins (~lu@user/lu) |
| 04:39:21 | nerdy | is now known as np |
| 04:39:33 | → | vicfred joins (~vicfred@user/vicfred) |
| 04:40:07 | × | ddellacosta quits (~ddellacos@86.106.121.222) (Remote host closed the connection) |
| 04:42:30 | × | rk04 quits (~rk04@user/rajk) (Quit: Client closed) |
| 04:42:47 | <hololeap> | I'm trying to make a class function `toFieldTree :: Data.Tree.Tree (n -> s -> Brick.Forms.FormFieldState s e n)` |
| 04:42:51 | → | rk04 joins (~rk04@user/rajk) |
| 04:43:03 | <hololeap> | the problem is that the `s` and `n` type variables are unique in each node of the tree, but need to compose with their parents |
| 04:43:13 | <hololeap> | the only way that I can see to do this is to have a heterogeneous Tree which carries type-level Trees for both `s` and `n`. this way each node has its own `s` and `n` and also knows that of its children, etc. |
| 04:43:56 | × | xkapastel quits (uid17782@id-17782.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 04:44:48 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 04:45:05 | × | siraben quits (~siraben@user/siraben) (Quit: node-irc says goodbye) |
| 04:45:25 | → | siraben joins (~siraben@user/siraben) |
| 04:45:53 | × | hmmmas quits (~chenqisu1@183.217.202.217) (Quit: Leaving.) |
| 04:46:25 | × | fosskers quits (~colin@S0106f0f249642f53.vn.shawcable.net) (Remote host closed the connection) |
| 04:51:45 | → | leeb joins (~leeb@KD111239155018.au-net.ne.jp) |
| 04:56:28 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 268 seconds) |
| 04:57:06 | × | ornxka quits (~ornxka@user/ornxka) (Quit: ornxka) |
| 04:57:21 | → | favonia_ joins (~favonia@user/favonia) |
| 05:04:16 | → | petersen joins (~juhp@bb219-75-40-154.singnet.com.sg) |
| 05:05:17 | × | hexology quits (~hexology@user/hexology) (Quit: hex on you ...) |
| 05:05:55 | → | hexology joins (~hexology@user/hexology) |
| 05:08:47 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 05:09:51 | → | ru0mad joins (~ruomad@176.164.105.224) |
| 05:11:00 | × | ru0mad quits (~ruomad@176.164.105.224) (Client Quit) |
| 05:11:26 | → | ru0mad joins (~ruomad@176.164.105.224) |
| 05:16:08 | → | ddellacosta joins (~ddellacos@86.106.143.209) |
| 05:17:13 | → | mnrmnaugh joins (~mnrmnaugh@pool-96-252-87-182.bstnma.fios.verizon.net) |
| 05:18:40 | × | favonia_ quits (~favonia@user/favonia) (Ping timeout: 268 seconds) |
| 05:18:46 | × | ru0mad quits (~ruomad@176.164.105.224) (Ping timeout: 264 seconds) |
| 05:19:05 | → | favonia_ joins (~favonia@user/favonia) |
| 05:19:17 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 05:19:46 | × | rk04 quits (~rk04@user/rajk) (Quit: Client closed) |
| 05:20:17 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 05:20:34 | × | ddellacosta quits (~ddellacos@86.106.143.209) (Ping timeout: 264 seconds) |
| 05:22:32 | × | favonia_ quits (~favonia@user/favonia) (Client Quit) |
| 05:23:50 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 252 seconds) |
| 05:24:49 | × | hylisper quits (~yaaic@111.119.208.67) (Ping timeout: 268 seconds) |
| 05:28:00 | → | favonia_ joins (~favonia@user/favonia) |
| 05:28:19 | × | favonia_ quits (~favonia@user/favonia) (Client Quit) |
| 05:29:06 | → | favonia_ joins (~favonia@user/favonia) |
| 05:30:22 | → | Bartosz joins (~textual@24.35.90.211) |
| 05:31:21 | → | hylisper joins (~yaaic@2409:4040:e89:1bc::94b:8209) |
| 05:31:29 | × | bilegeek quits (~bilegeek@2600:1008:b06d:65ed:93d7:e6a:a06d:9e4) (Quit: Leaving) |
| 05:32:06 | × | favonia_ quits (~favonia@user/favonia) (Client Quit) |
| 05:32:16 | → | favonia_ joins (~favonia@user/favonia) |
| 05:32:35 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 05:35:58 | × | lu quits (~lu@user/lu) (Remote host closed the connection) |
| 05:37:27 | × | a6a45081-2b83 quits (~aditya@106.212.79.20) (Remote host closed the connection) |
| 05:41:07 | → | chomwitt joins (~Pitsikoko@2a02:587:dc02:b00:b16c:5166:feb8:97d5) |
| 05:43:05 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 252 seconds) |
| 05:44:19 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 05:44:34 | → | dut joins (~dut@user/dut) |
| 05:50:54 | × | doyougnu quits (~user@c-67-168-253-231.hsd1.or.comcast.net) (Remote host closed the connection) |
| 05:54:27 | → | arrowd joins (~arr@2.94.203.147) |
| 05:55:02 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 05:55:24 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 05:55:34 | <siraben> | What happens if you join #haskell on Freenode? Is it now closed? |
| 05:55:47 | <arrowd> | edwardk: Hello. I'm OP of #haskell-freebsd on Freenode and I want to migrate the channel to Libera. I need OP for #haskell-freebsd there, but someont already created the channel. |
| 05:55:56 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 05:56:15 | → | ddellacosta joins (~ddellacos@86.106.121.222) |
| 05:58:15 | → | ikex joins (~ash@user/ikex) |
| 05:59:22 | → | Guest64 joins (~Guest64@2601:140:8a00:2230:d9be:6461:1c65:81f0) |
| 05:59:46 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 05:59:59 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 268 seconds) |
| 06:00:54 | × | ddellacosta quits (~ddellacos@86.106.121.222) (Ping timeout: 264 seconds) |
| 06:06:55 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 06:08:17 | × | favonia_ quits (~favonia@user/favonia) (Quit: Leaving) |
| 06:08:18 | × | pe200012 quits (~pe200012@119.131.208.84) (Read error: Connection reset by peer) |
| 06:08:44 | → | pe200012 joins (~pe200012@218.107.17.245) |
| 06:09:07 | → | hmmmas joins (~chenqisu1@183.217.202.217) |
| 06:10:16 | <glguy> | arrowd, could you ask in #haskell-ops please? one of the #haskell group contacts can help |
| 06:11:16 | × | Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 06:12:13 | → | Bartosz joins (~textual@24.35.90.211) |
| 06:12:51 | <arrowd> | I'll try, thanks. |
| 06:12:58 | <dy> | Bartosz: I have a question regarding the Functorio post |
| 06:13:10 | → | hylisper2 joins (~yaaic@111.119.208.67) |
| 06:13:12 | <dy> | Are you happy with what you've done :^p? |
| 06:13:39 | <dy> | It's only a matter of time until someone does actually add proper functors to Factorio now. |
| 06:13:57 | <dy> | And before you know it we'll have conveyer built systems producing abstract proofs of proportions rather than any concrete good. |
| 06:14:12 | → | ornxka joins (~ornxka@user/ornxka) |
| 06:14:54 | <dy> | More pressingly: how do we visualize higher order functorial belts? (e.g. Belt Belt Belt Belt ... at |
| 06:15:01 | <dy> | Belt Belt Belt Belt ... T* |
| 06:15:18 | <dy> | Is this probably equivalent to higher dimensional belt systems? |
| 06:15:22 | <hmmmas> | williang123# |
| 06:15:22 | <dy> | provably* |
| 06:17:52 | × | hylisper quits (~yaaic@2409:4040:e89:1bc::94b:8209) (Ping timeout: 268 seconds) |
| 06:23:10 | × | aforemny quits (~aforemny@static.248.158.34.188.clients.your-server.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 06:23:31 | → | aforemny joins (~aforemny@static.248.158.34.188.clients.your-server.de) |
| 06:25:26 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 252 seconds) |
| 06:25:35 | → | prite joins (~pritam@user/pritambaral) |
| 06:26:13 | → | kosmikus[m] joins (~andresloe@2001:470:69fc:105::95d) |
| 06:29:52 | × | aforemny quits (~aforemny@static.248.158.34.188.clients.your-server.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 06:30:13 | → | aforemny joins (~aforemny@static.248.158.34.188.clients.your-server.de) |
| 06:30:14 | → | ddellacosta joins (~ddellacos@89.46.62.183) |
| 06:30:53 | × | Guest64 quits (~Guest64@2601:140:8a00:2230:d9be:6461:1c65:81f0) (Quit: Client closed) |
| 06:33:15 | → | coot joins (~coot@37.30.49.19.nat.umts.dynamic.t-mobile.pl) |
| 06:33:20 | × | dut quits (~dut@user/dut) (Quit: Leaving) |
| 06:34:57 | → | sondre joins (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) |
| 06:35:07 | × | ddellacosta quits (~ddellacos@89.46.62.183) (Ping timeout: 272 seconds) |
| 06:35:54 | → | favonia joins (~favonia@38.54.72.34.bc.googleusercontent.com) |
| 06:36:09 | × | favonia quits (~favonia@38.54.72.34.bc.googleusercontent.com) (Client Quit) |
| 06:36:28 | <koishi_> | hi, i'm trying to use lazy IO to get a stream of lines, which works as expected (code: https://pastebin.com/L0GmUPSd) |
| 06:36:46 | <koishi_> | but what is not expected is the constant memory usage! |
| 06:37:13 | <koishi_> | i'm curious how ghc does that? |
| 06:37:33 | → | favonia joins (~favonia@user/favonia) |
| 06:37:46 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 06:37:50 | → | wonko joins (~wjc@62.115.229.50) |
| 06:38:02 | <koishi_> | (this code keeps a list of 100 most recent lines) |
| 06:38:13 | × | wonko quits (~wjc@62.115.229.50) (Changing host) |
| 06:38:13 | → | wonko joins (~wjc@user/wonko) |
| 06:39:36 | → | favonia joins (~favonia@user/favonia) |
| 06:40:41 | → | mib_lfiwfw joins (a0ee4bcb@ircip1.mibbit.com) |
| 06:41:20 | → | michalz joins (~user@185.246.204.55) |
| 06:41:34 | → | enzotib joins (~enzotib@user/enzotib) |
| 06:42:52 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 06:43:46 | <mib_lfiwfw> | https://paste.tomsmeding.com/wC5mbV9Q is this correct syntax and program. I got no clue what is happening |
| 06:44:27 | <dibblego> | what does the compiler say? |
| 06:44:47 | × | Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 06:44:50 | <mib_lfiwfw> | dibblego: not using it I got it from a video |
| 06:45:07 | <dminuoso> | mib_lfiwfw: Yeah, so this is a cute (but inefficient) way of expressing quicksort. |
| 06:45:07 | <dibblego> | compile it |
| 06:45:30 | <mib_lfiwfw> | dminuoso: ineeficient as in performance? |
| 06:45:58 | <mib_lfiwfw> | dibblego: I will do later slowly |
| 06:46:00 | <dminuoso> | mib_lfiwfw: Yeah, this is not in place. |
| 06:46:14 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 268 seconds) |
| 06:46:21 | <dminuoso> | I used to think this was a good example, but Im slowly changing my mind on this. |
| 06:47:21 | → | favonia joins (~favonia@user/favonia) |
| 06:47:36 | <mib_lfiwfw> | dminuoso: hmm |
| 06:47:45 | <dminuoso> | mib_lfiwfw: One could think of a sorted list as one where each element is placed in between the lower sorted elements and the greater sorted elements. |
| 06:48:04 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:c68c:4252:bd9f:2d01) |
| 06:48:04 | → | favonia_ joins (~favonia@user/favonia) |
| 06:48:06 | <dminuoso> | With that view, you can think this of declarative programming |
| 06:48:10 | × | favonia_ quits (~favonia@user/favonia) (Client Quit) |
| 06:48:48 | <mib_lfiwfw> | dminuoso: I am curious how you would write quicksort in haskell |
| 06:48:55 | <mib_lfiwfw> | just to compare |
| 06:49:01 | <dminuoso> | I wouldn't to begin with. :p |
| 06:49:03 | × | vicfred quits (~vicfred@user/vicfred) (Quit: Leaving) |
| 06:49:06 | <dminuoso> | There's better sorts |
| 06:49:12 | → | cfricke joins (~cfricke@user/cfricke) |
| 06:49:15 | <koishi_> | hoare's trick is indeed ingenious, but perhaps it's not what makes it quicksort |
| 06:49:35 | <mib_lfiwfw> | dminuoso: ok |
| 06:49:36 | <koishi_> | there are parallel quicksort algorithms, and they are not in-place |
| 06:49:36 | <dminuoso> | But roughly the same you'd write it in any language (except the mutation is hidden away with ST) |
| 06:50:53 | <dminuoso> | But with inplace partitioning inside ST, the code doesn't look cute and pretty anymore.. so nobody shows you that. |
| 06:51:15 | → | the-coot[m] joins (~the-cootm@2001:470:69fc:105::95f) |
| 06:51:16 | <dminuoso> | Which is why I think this is a terrible example, at worst it might suggest to users that Haskell cant implement efficient quicksort. |
| 06:51:37 | <mib_lfiwfw> | dminuoso: Igot that snippet form some haskell intro video |
| 06:51:53 | <mib_lfiwfw> | I liked its syntax and style |
| 06:53:18 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Remote host closed the connection) |
| 06:53:46 | → | holy_ joins (~h01y_b4z0@103.244.176.36) |
| 06:54:42 | → | anandprabhu joins (~anandprab@87.201.97.214) |
| 06:54:54 | o | is now known as niko |
| 06:56:04 | × | solomon quits (~solomon@165.227.48.175) (Ping timeout: 250 seconds) |
| 07:00:06 | × | slowButPresent quits (~slowButPr@user/slowbutpresent) (Quit: leaving) |
| 07:00:16 | → | Cubic joins (~hannesste@ip5f5be453.dynamic.kabel-deutschland.de) |
| 07:01:02 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 07:01:27 | → | chaosite joins (~chaosite@user/chaosite) |
| 07:04:13 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:04:25 | × | mib_lfiwfw quits (a0ee4bcb@ircip1.mibbit.com) (Quit: https://mibbit.com Online IRC Client) |
| 07:04:59 | → | ddellacosta joins (~ddellacos@89.45.224.118) |
| 07:05:10 | <phma> | Is there a way to set up an out-of-source build in Cabal? |
| 07:06:46 | × | chaosite quits (~chaosite@user/chaosite) (Ping timeout: 264 seconds) |
| 07:07:52 | <sclv> | what means out of source |
| 07:08:23 | <dminuoso> | "out-of-source" refers to keeping build artifacts separate from source code |
| 07:08:33 | <dminuoso> | e.g. intermediate object files, final artifacts |
| 07:08:55 | <dminuoso> | At least that's the terminology used in the C/C++ world |
| 07:09:20 | <sclv> | cabal does that by default |
| 07:09:44 | <sclv> | all its artifacts go in dist-newstyle |
| 07:09:46 | × | ddellacosta quits (~ddellacos@89.45.224.118) (Ping timeout: 264 seconds) |
| 07:09:47 | <phma> | I have the source in ~/src/foo/. I'd like the built binary to be in ~/build/foo/, where I keep data files I run the program on. |
| 07:10:06 | <phma> | but dist-newstyle is inside the source directory |
| 07:10:51 | <sclv> | you can cabal install the package and pass the —install-dir flag |
| 07:11:23 | <sclv> | and it symlinks (or copies depending on flag) the exe to the target |
| 07:11:46 | <phma> | I'm not installing it yet, I'm still working on it |
| 07:12:11 | <sclv> | install just copies or symlinks the product to the specified dir |
| 07:12:38 | <sclv> | if its an executable that is |
| 07:13:06 | × | ell quits (~ellie@user/ellie) (Quit: The Lounge - https://thelounge.chat) |
| 07:13:59 | <phma> | in my C++ projects I have ~/build/foo/grel, ~/build/foo/cdbg, etc. according to which compiler I use and whether it's a release, install, debug, or fuzzing build |
| 07:14:36 | <phma> | and the binary goes in that file, with build artifacts in subdirectories of it |
| 07:14:59 | <sclv> | ok thats dist-newstyle for cabal |
| 07:15:19 | <sclv> | it just so happens to be in the project dir |
| 07:15:43 | <phma> | but the dist-newstyle directory is inside the source directory, not the build directory |
| 07:15:49 | <phma> | and I don't see the binary |
| 07:17:10 | → | chaosite joins (~chaosite@user/chaosite) |
| 07:17:43 | <sclv> | the binary is hidden in it |
| 07:18:42 | <sclv> | https://cabal.readthedocs.io/en/3.4/nix-local-build.html#where-are-my-build-products |
| 07:19:27 | <phma> | is there a way to tell cabal to put the binary in the build directory? and I'm not installing it because I'm still working on it |
| 07:20:08 | <sclv> | install is that command. that’s literally all it does. If you don’t like the name... sorry |
| 07:22:10 | <phma> | is there a way to run cabal in the build directory and tell it where the source directory is? that's how cmake works |
| 07:22:25 | → | Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 07:22:37 | × | chaosite quits (~chaosite@user/chaosite) (Ping timeout: 268 seconds) |
| 07:22:53 | <sclv> | not that i know of. its a different tool, it has different flags and conventions. *shrug* |
| 07:25:42 | × | arrowd quits (~arr@2.94.203.147) () |
| 07:25:51 | <phma> | what does "nix-style" mean? |
| 07:25:58 | × | riatre quits (~quassel@2001:310:6000:f::5198:1) (Ping timeout: 264 seconds) |
| 07:26:45 | <phma> | where can I submit a feature request for cabal? |
| 07:26:46 | → | riatre joins (~quassel@h203-145-233-111.ablenetvps.ne.jp) |
| 07:26:57 | → | dpl joins (~dpl@77-121-78-163.chn.volia.net) |
| 07:27:24 | <sclv> | ok first please explain why you want this |
| 07:27:33 | <sclv> | other than “cmake does it” |
| 07:27:43 | <sclv> | but also just go to the github |
| 07:33:05 | × | holy_ quits (~h01y_b4z0@103.244.176.36) (Ping timeout: 268 seconds) |
| 07:33:23 | <tomsmeding> | sclv: install does more, it also does a clean rebuild, right? |
| 07:33:50 | <sclv> | yes, i was simplifying a bit |
| 07:34:38 | <tomsmeding> | phma: nix-style means that it automatically builds and caches dependencies in the user-wide store in ~/.cabal when you mention them in the dependency list in your .cabal file |
| 07:35:11 | → | mc47 joins (~yecinem@89.246.239.190) |
| 07:35:31 | <tomsmeding> | nix is a tool that did this for other applications, and is somewhat used/known in the haskell world, and people chose this name to distinguish the behaviour from what cabal previously did |
| 07:35:38 | <sclv> | this is all explained in The Fine Manual i linked |
| 07:36:05 | <dminuoso> | 09:19:27 phma | is there a way to tell cabal to put the binary in the build directory? and I'm not installing it because I'm still working on it |
| 07:36:21 | <dminuoso> | phma: There's a plumbing command in cabal 3.4.0.0 called `list-bin` |
| 07:36:37 | <dminuoso> | For older versions, you can use `cabal-plan`. With those you can extract the build artifact with something like |
| 07:36:48 | tomsmeding | is delighted |
| 07:36:56 | <dminuoso> | $ cp $(cabal -v0 list-bin <target>) ./ |
| 07:37:22 | → | cheater1__ joins (~Username@user/cheater) |
| 07:37:24 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 07:37:34 | cheater1__ | is now known as cheater |
| 07:39:15 | → | ddellacosta joins (~ddellacos@86.106.121.235) |
| 07:40:11 | <dminuoso> | phma: If you want a different directory for dist-newstyle, you can pass one of: --builddir, --distdir, --distpref DIR |
| 07:42:43 | → | cheater1__ joins (~Username@user/cheater) |
| 07:42:57 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 07:44:11 | × | ddellacosta quits (~ddellacos@86.106.121.235) (Ping timeout: 268 seconds) |
| 07:45:09 | → | bilegeek joins (~bilegeek@2600:1008:b06d:65ed:93d7:e6a:a06d:9e4) |
| 07:45:30 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 07:47:23 | → | beka joins (~beka@104.193.170-254.PUBLIC.monkeybrains.net) |
| 07:47:33 | × | cheater1__ quits (~Username@user/cheater) (Ping timeout: 265 seconds) |
| 07:49:22 | <phma> | can I tell it --sourcedir? |
| 07:52:08 | <dminuoso> | What are you trying to do exactly? |
| 07:56:32 | × | jjhoo quits (jahakala@dsl-trebng21-58c18f-56.dhcp.inet.fi) (Ping timeout: 268 seconds) |
| 07:57:24 | <phma> | I put data files in the build directory, and I'd like to run "cabal new-run" or the like in the build directory. I don't want my data files in the repo, so I put them in the build directory. |
| 07:58:16 | → | jjhoo joins (jahakala@dsl-trebng21-58c18f-56.dhcp.inet.fi) |
| 07:59:11 | <phma> | So cabal has to know where the source is. Also if I load the program in ghci, and I want to do this in the build directory so that I can run it on the datafiles, ghci has to know where the source is. |
| 07:59:48 | <phma> | So it may need to be an option not just for cabal. |
| 08:02:05 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 268 seconds) |
| 08:03:18 | → | dhouthoo joins (~dhouthoo@178-117-36-167.access.telenet.be) |
| 08:08:54 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:08:59 | <sclv> | sounds like you should just put (or symlink) the datafiles in the project directory and use a .gitignore to exclude them from the repo. or just teach your lib or executable to take a flag specifying the data file directory |
| 08:09:17 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 08:09:40 | × | hendursaga quits (~weechat@user/hendursaga) (Ping timeout: 252 seconds) |
| 08:10:20 | → | kuribas joins (~user@ptr-25vy0i7o5gw6tky01tr.18120a2.ip6.access.telenet.be) |
| 08:10:28 | → | cheater joins (~Username@user/cheater) |
| 08:11:35 | <phma> | I found the repo on github and am thinking about how to word the feature request. |
| 08:12:06 | <kuribas> | I read on an article how some database libraries aren't good because they don't prove their correctness in the type system. That makes me wonder, don't they test the code they write? I always test any code I write, even just quickly in the REPL. |
| 08:12:14 | <phma> | It doesn't make sense to put data files in .gitignore, because if other people work on the same project, they'll have different data files. |
| 08:12:29 | <c_wraith> | kuribas: I'm not sure that's a good argument |
| 08:12:51 | <kuribas> | c_wraith: mine or his? :-) |
| 08:12:59 | × | Sgeo quits (~Sgeo@user/sgeo) (Quit: Leaving) |
| 08:13:09 | → | ddellacosta joins (~ddellacos@86.106.143.209) |
| 08:13:37 | <c_wraith> | The one to which you are responding. (You can't really express a lot of what SQL can do in a way that's easy to use in Haskell) |
| 08:14:05 | <kuribas> | the article seemed to favor opaleye |
| 08:14:28 | → | rahguzar joins (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) |
| 08:14:40 | <kuribas> | personally, I'd prefer a library to be close to SQL, rather than another abstraction to learn on top. |
| 08:14:51 | <nitrix> | kuribas, A static type system can catch bugs earlier in the development phase, but it's not perfect. Even if you were to encode all your invariants, you could still accidently get the requirements wrong. |
| 08:14:55 | <c_wraith> | Opaleye doesn't even verify that the database schema matches the queries. :P |
| 08:15:22 | <kuribas> | c_wraith: heh :) |
| 08:15:39 | <kuribas> | My library does :) |
| 08:15:43 | <c_wraith> | terrible that it leaves so many bugs for runtime! |
| 08:15:59 | <nitrix> | kuribas, Tests get you a little further, but only so much. When people talk about proof and correctness, it's a lot more rigorous than that and often impossible for an application of a moderate size. |
| 08:16:23 | <kuribas> | nitrix: true, and I don't think a lot of haskell code is really "proven" correct. |
| 08:16:50 | → | hendursaga joins (~weechat@user/hendursaga) |
| 08:17:41 | × | ddellacosta quits (~ddellacos@86.106.143.209) (Ping timeout: 264 seconds) |
| 08:17:49 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 08:17:58 | <kuribas> | c_wraith: I am more interested in having a library checking for mismatched columns rather than checking if the SQL is semantically sound SQL. |
| 08:18:13 | <kuribas> | c_wraith: because that will help in refactoring database tables. |
| 08:18:22 | <kuribas> | and adding new functionality. |
| 08:18:45 | <kuribas> | assuming I know how to write SQL, and possibly test it in the SQL REPL first. |
| 08:20:05 | <nitrix> | One way that people have been doing this, back in the 70s, is with metaprogramming/macros. You connect to the database and generate code for the application, knowing that they will fully correspond (assuming no bad manipulation in production). |
| 08:20:38 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 264 seconds) |
| 08:20:49 | <kuribas> | There are two options: 1. a library which just translates to SQL, and doesn't try to be much in the way. 2. a library which implements it's own sound model on top of SQL, but it will also limit the possible queries (persistent). |
| 08:20:53 | × | tomboy64 quits (~tomboy64@2a02:2454:416:db00:ba27:ebff:fe58:73c2) (Read error: Connection reset by peer) |
| 08:21:10 | → | xkb joins (~xkb@a80-100-6-16.adsl.xs4all.nl) |
| 08:21:12 | <kuribas> | nitrix: that's nice until you want to compose your queries. |
| 08:21:25 | <kuribas> | nitrix: add sort keys, cursors, etc... |
| 08:21:42 | <nitrix> | I don't see the issue. |
| 08:22:01 | <kuribas> | nitrix: how would you compose the query if the macro is predefined? |
| 08:22:45 | <nitrix> | The metaprogram is just translating the databases and tables into equivalent types. You then worth with those types to make your queries like you normally would. |
| 08:22:53 | <nitrix> | s/worth/work |
| 08:24:54 | <nitrix> | You can have any sort of ORM around this, it's completely orthogonal. |
| 08:25:13 | <unyu> | Presumably the metaprogram runs at compile-time, so every time you want to add a new query, you need to recompile the thing, even if the actual tables have not changed. |
| 08:25:18 | <xkb> | Hi all, I'm trying to solve a hackerRank exercise called minimum swaps. Challenge is to determine the minmum nr of swaps needed to sort an array. I've written a (naive) Haskell solution using a graph cycle algorithm, Code is here: https://paste.tomsmeding.com/azzuoitj This solves the problem for the first 4 sample cases + 1 other but fails on |
| 08:25:19 | <xkb> | others. I probably made some really stupid mistake but can't see it, so would appreciate some eyes at the code. Next to this I need to optimise it, probably by fixing the hasCycle function so I don't repeatedly sort.. Just to be clear: this is not a work assessment or anything, it's one of the practice exercises from HackerRank. |
| 08:26:02 | <nitrix> | unyu, Not every time you add a new query, just every time you change the database structure (new tables, new columns, etc). |
| 08:26:02 | <xkb> | `Minimum Swaps 2` to be exact |
| 08:26:27 | <unyu> | Oh, then that is good. |
| 08:26:28 | <kuribas> | nitrix: that's what my library does, it reads the information schema and outputs template haskell with corresponding types. |
| 08:26:40 | <nitrix> | kuribas, Then you're set :) |
| 08:29:21 | → | Topsi joins (~Tobias@dyndsl-095-033-095-132.ewe-ip-backbone.de) |
| 08:31:11 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 08:31:42 | → | z0k joins (~z0k@101.50.108.132) |
| 08:31:51 | → | feliix42 joins (~felix@gibbs.uberspace.de) |
| 08:39:21 | → | chaosite joins (~chaosite@user/chaosite) |
| 08:40:21 | → | bfrk joins (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) |
| 08:41:30 | → | dhil joins (~dhil@195.213.192.85) |
| 08:41:48 | ← | bfrk parts (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) () |
| 08:41:48 | × | z0k quits (~z0k@101.50.108.132) (Quit: WeeChat 3.0) |
| 08:42:30 | × | charukiewicz quits (~quassel@irouteince04.i.subnet.rcn.com) (Remote host closed the connection) |
| 08:43:40 | → | charukiewicz joins (~quassel@irouteince04.i.subnet.rcn.com) |
| 08:46:50 | → | fendor joins (~fendor@178.115.56.93.wireless.dyn.drei.com) |
| 08:49:33 | × | Guest417 quits (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) (Ping timeout: 268 seconds) |
| 08:54:02 | → | comerijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 08:54:29 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 08:55:10 | <arahael> | I'm trying to get 'newEnv' from Network.AWS.Env, which should be in https://github.com/brendanhay/amazonka/blob/a266fc686cdddb48ac791261b73798c2ed8a6097/amazonka/src/Network/AWS/Env.hs |
| 08:55:35 | <arahael> | However... when I compile, I get a 'Could not find module ‘Network.AWS.Env’', what must I be doing wrong? It's in amazonka-core, right? |
| 08:56:46 | × | hnOsmium0001 quits (uid453710@id-453710.stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:58:21 | <fendor> | arahael, looks like it is in amazonka |
| 08:58:24 | <fendor> | https://hackage.haskell.org/package/amazonka |
| 08:59:17 | → | Guest58 joins (~Guest58@125-227-78-46.HINET-IP.hinet.net) |
| 08:59:25 | <arahael> | fendor: Oh, so I have to get the whole thing? I can't just build-depends amazonka-core or something? |
| 08:59:47 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 08:59:49 | <fendor> | arahael, to me it looks like amazonka-core does not expose that module. |
| 08:59:58 | × | xprlgjf quits (~gavin@60.27.93.209.dyn.plus.net) (Remote host closed the connection) |
| 09:00:07 | <fendor> | so maybe? Don't know about amazonka otherwise |
| 09:00:09 | <arahael> | Hmm... Very curious. |
| 09:00:33 | <arahael> | So I'm now build-depending amazonka, amazonka-core, and amazonka-s3, lets see if that works... |
| 09:00:39 | × | beka quits (~beka@104.193.170-254.PUBLIC.monkeybrains.net) (Ping timeout: 268 seconds) |
| 09:01:10 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:f131:7ff:d61f:7340) (Remote host closed the connection) |
| 09:01:39 | <dhouthoo> | arahael: i just depend on amazonka and amazonka-s3 |
| 09:01:43 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) |
| 09:01:48 | × | fendor quits (~fendor@178.115.56.93.wireless.dyn.drei.com) (Remote host closed the connection) |
| 09:02:05 | <arahael> | dhouthoo: Thanks for the tip. |
| 09:02:17 | <arahael> | For my learning, how do you guys figure that out? |
| 09:02:48 | <dhouthoo> | browsing hackage |
| 09:02:51 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 09:03:59 | <arahael> | Ahd observing that the amazonka package does contain a Network.AWS.Env and that that does contain a newEnv, ok that works. :) |
| 09:04:04 | → | berberman_ joins (~berberman@user/berberman) |
| 09:04:29 | → | shiraeeshi joins (~shiraeesh@109.166.58.176) |
| 09:04:48 | → | tremon joins (~tremon@217-63-61-89.cable.dynamic.v4.ziggo.nl) |
| 09:04:59 | × | berberman quits (~berberman@user/berberman) (Ping timeout: 268 seconds) |
| 09:05:06 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.1) |
| 09:05:37 | → | Guest417 joins (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) |
| 09:06:49 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) (Ping timeout: 268 seconds) |
| 09:07:54 | <arahael> | Thanks :) |
| 09:08:44 | → | xprlgjf joins (~gavin@60.27.93.209.dyn.plus.net) |
| 09:09:54 | × | ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Ping timeout: 268 seconds) |
| 09:10:14 | → | ubikium joins (~ubikium@2400:2200:4f2:4b71:94bf:c634:be62:7c0d) |
| 09:12:23 | × | xprlgjf quits (~gavin@60.27.93.209.dyn.plus.net) (Remote host closed the connection) |
| 09:13:19 | → | xprlgjf joins (~gavin@60.27.93.209.dyn.plus.net) |
| 09:14:31 | × | ubikium quits (~ubikium@2400:2200:4f2:4b71:94bf:c634:be62:7c0d) (Read error: Connection reset by peer) |
| 09:14:45 | → | ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) |
| 09:20:13 | × | Topsi quits (~Tobias@dyndsl-095-033-095-132.ewe-ip-backbone.de) (Quit: Leaving.) |
| 09:20:26 | → | Topsi joins (~Tobias@dyndsl-095-033-095-132.ewe-ip-backbone.de) |
| 09:21:42 | → | guest0123 joins (~aaron@2601:602:a080:fa0:21da:7ddc:2cc6:a10c) |
| 09:22:52 | × | Erutuon quits (~Erutuon@71-34-10-193.mpls.qwest.net) (Ping timeout: 268 seconds) |
| 09:24:26 | × | xprlgjf quits (~gavin@60.27.93.209.dyn.plus.net) (Remote host closed the connection) |
| 09:27:13 | × | Lycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 09:27:46 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 264 seconds) |
| 09:28:38 | → | tomboy64 joins (~tomboy64@2a02:2454:416:db00:ba27:ebff:fe58:73c2) |
| 09:29:23 | → | xprlgjf joins (~gavin@60.27.93.209.dyn.plus.net) |
| 09:31:11 | → | fendor joins (~fendor@178.115.56.93.wireless.dyn.drei.com) |
| 09:31:29 | × | shiraeeshi quits (~shiraeesh@109.166.58.176) (Ping timeout: 264 seconds) |
| 09:31:29 | × | rahguzar quits (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Ping timeout: 264 seconds) |
| 09:33:59 | × | xkb quits (~xkb@a80-100-6-16.adsl.xs4all.nl) (Quit: Ping timeout (120 seconds)) |
| 09:34:30 | × | jonathanclarke quits (~jonathanc@202.51.76.55) (Ping timeout: 264 seconds) |
| 09:34:47 | → | guest531 joins (~user@49.5.6.87) |
| 09:36:28 | → | disconsis joins (~disconsis@103.212.147.213) |
| 09:36:42 | <disconsis> | hi guys |
| 09:36:50 | <disconsis> | i'm trying to solve a sorta simple problem |
| 09:37:12 | <tdammers> | sorta simple problems are the worst |
| 09:37:21 | <disconsis> | I have an AstF type: |
| 09:37:24 | <disconsis> | data AstF a b |
| 09:37:26 | <disconsis> | = Assign { var :: Text, value :: ArithExpr, label :: a } |
| 09:37:28 | <disconsis> | ... |
| 09:37:57 | <disconsis> | I would assume that (Assign{ label :: a}) :: forall b . AstF a b |
| 09:38:59 | <opqdonut> | I think the record update syntax might be monomorphic |
| 09:39:49 | <disconsis> | I was trying to indicate that label has type 'a' |
| 09:40:02 | <disconsis> | Sorry, that's not actual code |
| 09:40:06 | <disconsis> | I'm trying to do this: |
| 09:40:07 | → | shiraeeshi joins (~shiraeesh@109.166.58.176) |
| 09:40:08 | <disconsis> | apply :: (i -> a -> (i, b)) -> i -> AstF a (Ast b) -> (i, AstF b (Ast b)) |
| 09:40:10 | <disconsis> | apply f i ast = |
| 09:40:12 | <disconsis> | let (i', label') = f i (label ast) |
| 09:40:14 | <disconsis> | in (i', ast {label = label'}) |
| 09:40:16 | <disconsis> | recurse :: (i -> a -> (i, b)) -> i -> Ast a -> (i, Ast b) |
| 09:40:18 | <disconsis> | recurse f i = \case |
| 09:40:20 | <disconsis> | Ast ast@Assign {..} -> apply f i ast |
| 09:40:28 | <opqdonut> | oh nevermind I was reading the code all wrong anyway |
| 09:40:43 | <disconsis> | Oh shit this is also relevat |
| 09:40:45 | <disconsis> | newtype Ast a = Ast (AstF a (Ast a)) |
| 09:40:46 | × | tomboy64 quits (~tomboy64@2a02:2454:416:db00:ba27:ebff:fe58:73c2) (Changing host) |
| 09:40:46 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 09:41:02 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:41:15 | <disconsis> | Sorry this looks a bit complicated, but the basic problem is that in 'recurse', ast :: AstF a (Ast a) |
| 09:41:30 | <disconsis> | But I'm trying to use it as a value of type AstF a (Ast b) |
| 09:41:44 | <disconsis> | I feel like I should be able to do that, since the Assign constructor doesn't use 'b' |
| 09:42:55 | <disconsis> | (there's a mistake here, it should really be `Ast ast@Assign {..} -> second Ast $ apply f i ast` in 'recurse') |
| 09:43:09 | × | tomboy64 quits (~tomboy64@user/tomboy64) (Quit: Off to see the wizard.) |
| 09:43:33 | <disconsis> | However, if I do ast' = ast { label = label } then I can use ast' as a value of type AstF a (Ast b) |
| 09:43:35 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 09:44:00 | <disconsis> | This feels unneccessary to me. any way to fix this? |
| 09:44:31 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:c68c:4252:bd9f:2d01) (Ping timeout: 265 seconds) |
| 09:44:42 | × | xprlgjf quits (~gavin@60.27.93.209.dyn.plus.net) (Remote host closed the connection) |
| 09:45:02 | → | madnight joins (~madnight@static.59.103.201.195.clients.your-server.de) |
| 09:45:10 | → | Dusk[m] joins (~bb010gmat@2001:470:69fc:105::9a5) |
| 09:45:16 | Dusk[m] | is now known as bb010g |
| 09:45:17 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 09:46:20 | <disconsis> | In all, this is the code: |
| 09:46:22 | <disconsis> | data AstF a b |
| 09:46:24 | <disconsis> | = Assign { var :: Text, value :: ArithExpr, label :: a } |
| 09:46:26 | <disconsis> | newtype Ast a = Ast (AstF a (Ast a)) |
| 09:46:28 | <disconsis> | apply :: (i -> a -> (i, b)) -> i -> AstF a (Ast b) -> (i, AstF b (Ast b)) |
| 09:46:30 | <disconsis> | apply f i ast = |
| 09:46:32 | <disconsis> | let (i', label') = f i (label ast) |
| 09:46:34 | <disconsis> | in (i', ast {label = label'}) |
| 09:46:36 | <disconsis> | recurse :: (i -> a -> (i, b)) -> i -> Ast a -> (i, Ast b) |
| 09:46:38 | <disconsis> | recurse f i = \case |
| 09:46:38 | × | tomboy64 quits (~tomboy64@user/tomboy64) (Client Quit) |
| 09:46:40 | <disconsis> | Ast ast@Assign {..} -> |
| 09:46:42 | <disconsis> | -- second Ast $ apply f i ast -- doesn't work |
| 09:46:44 | <disconsis> | second Ast $ apply f i (ast { var = var }) -- does work |
| 09:46:53 | × | bilegeek quits (~bilegeek@2600:1008:b06d:65ed:93d7:e6a:a06d:9e4) (Quit: Leaving) |
| 09:47:38 | <disconsis> | i'm not explaining this amazingly well, but please feel free to ask for any clarifications :P |
| 09:48:38 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Remote host closed the connection) |
| 09:49:07 | × | leeb quits (~leeb@KD111239155018.au-net.ne.jp) (Quit: WeeChat 3.1) |
| 09:52:10 | <opqdonut> | disconsis: the problem is that since `ast` came out of an `Ast a`, it has type `AstF a (Ast a)` |
| 09:53:18 | <disconsis> | opqdonut: any idea how i can get the same value to be of type `AstF a (Ast b)` without doing the hacky `ast { var = var}`? |
| 09:54:18 | × | fabfianda quits (~fabfianda@net-93-148-125-174.cust.dsl.teletu.it) (Ping timeout: 268 seconds) |
| 09:54:26 | <opqdonut> | no, not really, unless you can change the definition of Ast |
| 09:54:41 | → | fabfianda joins (~fabfianda@mob-5-90-246-225.net.vodafone.it) |
| 09:54:49 | <opqdonut> | you can of course give a nice name to the function `AstF a b -> AstF a c` |
| 09:56:25 | <disconsis> | Hmm.. |
| 09:56:43 | <disconsis> | One problem is that AstF contains more constructors, of which some do use the 'b' |
| 09:56:52 | <opqdonut> | of course |
| 09:56:57 | <disconsis> | So it's not possible to white `AstF a b -> AstF a c` in general |
| 09:56:59 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 09:57:09 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 272 seconds) |
| 09:57:14 | <opqdonut> | yeah I think you should just stick with the {} hack |
| 09:57:19 | <disconsis> | I guess I'll just pattern match and create a new value |
| 09:57:32 | <opqdonut> | I'd probably prefer fully destructuring the input Assign, and constructing a new Assign explicitly |
| 09:57:36 | <opqdonut> | yeah |
| 09:57:40 | <disconsis> | Yeah that's what I'm going with |
| 09:57:42 | <disconsis> | thanks! |
| 09:57:51 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 09:58:20 | <opqdonut> | I wonder if you could get further with GADTs |
| 09:59:07 | <opqdonut> | data AstF a b where Assign :: Text -> ArithExpr -> a -> AstF a b, SomethingElse :: Text -> a -> b -> AstF a b |
| 09:59:30 | <opqdonut> | no, probably not, even they don't let you generalize an input that has been given a narrower type |
| 10:01:24 | <disconsis> | yeah, the problem really comes from the function signature |
| 10:01:35 | <disconsis> | but this is an okay solution |
| 10:01:43 | × | chomwitt quits (~Pitsikoko@2a02:587:dc02:b00:b16c:5166:feb8:97d5) (Ping timeout: 268 seconds) |
| 10:01:48 | <disconsis> | it's pretty unexpected though |
| 10:01:58 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 264 seconds) |
| 10:02:15 | <opqdonut> | https://gitlab.haskell.org/ghc/ghc/-/issues/7658 <-- related |
| 10:02:18 | <disconsis> | i feel like i've worked with other functional langs that let you do this, but i can't remember them |
| 10:04:33 | × | fabfianda quits (~fabfianda@mob-5-90-246-225.net.vodafone.it) (Ping timeout: 272 seconds) |
| 10:04:40 | <disconsis> | ah interesting |
| 10:04:44 | → | fabfianda joins (~fabfianda@net-93-148-125-174.cust.vodafonedsl.it) |
| 10:04:55 | <disconsis> | 'phantom types' is exactly what I was trying to think of |
| 10:07:11 | → | igghibu joins (~igghibu@37.120.201.126) |
| 10:07:59 | → | lavaman joins (~lavaman@98.38.249.169) |
| 10:08:56 | <tdammers> | I was going to say, the fact that the foralled "b" does not appear anywhere in the actual type can be problematic |
| 10:09:53 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 264 seconds) |
| 10:12:35 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 252 seconds) |
| 10:13:11 | → | sondre joins (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) |
| 10:14:48 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 10:15:16 | × | involans quits (~alex@cpc92718-cmbg20-2-0-cust157.5-4.cable.virginm.net) (Ping timeout: 268 seconds) |
| 10:16:09 | × | Guest417 quits (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) (Quit: WeeChat 3.1) |
| 10:18:03 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 272 seconds) |
| 10:18:07 | × | Guest58 quits (~Guest58@125-227-78-46.HINET-IP.hinet.net) (Quit: Client closed) |
| 10:21:42 | → | rahguzar joins (~rahguzar@212.189.140.214) |
| 10:24:02 | → | ru0mad joins (~ruomad@176.164.105.224) |
| 10:26:21 | → | sondre joins (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) |
| 10:26:26 | × | ru0mad quits (~ruomad@176.164.105.224) (Client Quit) |
| 10:26:55 | → | ru0mad joins (~ruomad@176.164.105.224) |
| 10:28:29 | → | orhan89 joins (~orhan89@151.91.188.35.bc.googleusercontent.com) |
| 10:31:18 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 268 seconds) |
| 10:31:29 | × | ru0mad quits (~ruomad@176.164.105.224) (Client Quit) |
| 10:31:47 | × | kawzeg_ quits (kawzeg@2a01:7e01::f03c:92ff:fee2:ec34) (Quit: WeeChat 3.1) |
| 10:31:58 | → | kawzeg joins (kawzeg@2a01:7e01::f03c:92ff:fee2:ec34) |
| 10:32:35 | × | ruomad quits (~ruomad@82-64-17-144.subs.proxad.net) (Quit: leaving) |
| 10:32:59 | → | atwm joins (~andrew@178.197.235.239) |
| 10:34:03 | → | ru0mad joins (~ru0mad@82-64-17-144.subs.proxad.net) |
| 10:34:46 | × | wei2912 quits (~wei2912@112.199.250.21) (Quit: Lost terminal) |
| 10:36:27 | × | ukari quits (~ukari@user/ukari) (Remote host closed the connection) |
| 10:37:29 | × | shiraeeshi quits (~shiraeesh@109.166.58.176) (Ping timeout: 272 seconds) |
| 10:38:04 | × | ru0mad quits (~ru0mad@82-64-17-144.subs.proxad.net) (Client Quit) |
| 10:38:05 | × | xff0x quits (~xff0x@2001:1a81:528f:3900:ab23:5f87:bcb1:2783) (Ping timeout: 268 seconds) |
| 10:38:40 | → | xff0x joins (~xff0x@2001:1a81:528f:3900:63a6:c05a:b177:6450) |
| 10:38:44 | → | ru0mad joins (~ru0mad@82-64-17-144.subs.proxad.net) |
| 10:39:00 | × | aforemny quits (~aforemny@static.248.158.34.188.clients.your-server.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 10:39:20 | → | aforemny joins (~aforemny@static.248.158.34.188.clients.your-server.de) |
| 10:39:59 | → | sondre joins (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) |
| 10:40:06 | → | shiraeeshi joins (~shiraeesh@109.166.58.176) |
| 10:41:43 | ← | ru0mad parts (~ru0mad@82-64-17-144.subs.proxad.net) () |
| 10:42:43 | → | ru0mad joins (~ru0mad@82-64-17-144.subs.proxad.net) |
| 10:43:14 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:44:50 | × | ru0mad quits (~ru0mad@82-64-17-144.subs.proxad.net) (Client Quit) |
| 10:44:51 | → | francesco_ joins (~francesco@host-80-180-196-134.pool80180.interbusiness.it) |
| 10:44:59 | × | Techcable quits (~Techcable@168.235.93.147) (Quit: ZNC - https://znc.in) |
| 10:45:18 | × | shiraeeshi quits (~shiraeesh@109.166.58.176) (Ping timeout: 264 seconds) |
| 10:45:33 | × | francesco_ quits (~francesco@host-80-180-196-134.pool80180.interbusiness.it) (Client Quit) |
| 10:47:43 | → | ru0mad joins (~ru0mad@82-64-17-144.subs.proxad.net) |
| 10:48:02 | → | Techcable joins (~Techcable@168.235.93.147) |
| 10:48:34 | → | ru0mad[m] joins (~ru0madmat@2001:470:69fc:105::9b2) |
| 10:48:46 | → | zeenk joins (~zeenk@2a02:2f04:a310:b600:b098:bf18:df4d:4c41) |
| 10:53:19 | ← | tcard parts (~tcard@p2307053-ipngn17101hodogaya.kanagawa.ocn.ne.jp) (Leaving) |
| 10:54:10 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:7d39:eb90:ba7d:df66) |
| 10:54:38 | × | ru0mad quits (~ru0mad@82-64-17-144.subs.proxad.net) (Quit: leaving) |
| 10:55:58 | × | hmmmas quits (~chenqisu1@183.217.202.217) (Quit: Leaving.) |
| 10:55:59 | × | comerijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 10:56:35 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:56:49 | → | tcard joins (~tcard@p2307053-ipngn17101hodogaya.kanagawa.ocn.ne.jp) |
| 10:57:01 | × | disconsis quits (~disconsis@103.212.147.213) (Quit: Disconnected by BOFL) |
| 10:57:49 | × | atwm quits (~andrew@178.197.235.239) (Ping timeout: 268 seconds) |
| 11:00:02 | × | favonia quits (~favonia@user/favonia) (Quit: The Lounge - https://thelounge.chat) |
| 11:01:26 | × | mc47 quits (~yecinem@89.246.239.190) (Quit: Leaving) |
| 11:01:32 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 11:01:37 | × | curiousgay quits (~quassel@178.217.208.8) (Read error: Connection reset by peer) |
| 11:01:46 | → | curiousgay joins (~quassel@178.217.208.8) |
| 11:02:20 | × | xsperry quits (~as@user/xsperry) (Ping timeout: 265 seconds) |
| 11:02:29 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:03:07 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) |
| 11:03:40 | → | mc47 joins (~yecinem@89.246.239.190) |
| 11:03:46 | → | danidiaz joins (~ESDPC@148.3.54.112) |
| 11:05:47 | → | whez joins (sid470288@id-470288.tooting.irccloud.com) |
| 11:07:42 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) (Ping timeout: 268 seconds) |
| 11:08:44 | → | argento joins (~argent0@168.227.96.53) |
| 11:08:50 | × | guest531 quits (~user@49.5.6.87) (Read error: Connection reset by peer) |
| 11:09:09 | → | sciencentistguy joins (~sciencent@194.110.13.3) |
| 11:10:47 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 268 seconds) |
| 11:12:05 | × | rahguzar quits (~rahguzar@212.189.140.214) (Quit: Connection closed) |
| 11:12:28 | → | rahguzar joins (~rahguzar@212.189.140.214) |
| 11:12:52 | → | favonia joins (~favonia@user/favonia) |
| 11:12:53 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 11:13:45 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:16:56 | → | smitop joins (uid328768@user/smitop) |
| 11:21:38 | → | neceve joins (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130) |
| 11:22:18 | → | ruomad joins (~ruomad@176.164.105.224) |
| 11:22:58 | × | ruomad quits (~ruomad@176.164.105.224) (Client Quit) |
| 11:24:04 | → | Topsi1 joins (~Tobias@dyndsl-095-033-095-132.ewe-ip-backbone.de) |
| 11:24:21 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 11:24:35 | → | hmmmas joins (~chenqisu1@183.217.202.217) |
| 11:24:42 | → | ru0mad joins (~ru0mad@176.164.105.224) |
| 11:24:57 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:26:12 | × | Topsi quits (~Tobias@dyndsl-095-033-095-132.ewe-ip-backbone.de) (Ping timeout: 268 seconds) |
| 11:26:34 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 252 seconds) |
| 11:26:37 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 11:28:48 | → | Guest31 joins (~textual@cpc146410-hari22-2-0-cust124.20-2.cable.virginm.net) |
| 11:29:52 | × | ru0mad quits (~ru0mad@176.164.105.224) (Quit: Sayonara) |
| 11:29:53 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 11:30:08 | → | cheater joins (~Username@user/cheater) |
| 11:30:10 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 11:30:12 | → | ru0mad joins (~ru0mad@82-64-17-144.subs.proxad.net) |
| 11:30:29 | × | ru0mad quits (~ru0mad@82-64-17-144.subs.proxad.net) (Client Quit) |
| 11:30:30 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:30:46 | → | atwm joins (~andrew@178.197.235.239) |
| 11:31:41 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 11:32:08 | → | Topsi joins (~Tobias@dyndsl-095-033-095-132.ewe-ip-backbone.de) |
| 11:33:16 | × | GIANTWORLDKEEPER quits (~pjetcetal@2.95.204.25) (Ping timeout: 265 seconds) |
| 11:34:56 | → | ru0mad joins (~ru0mad@82-64-17-144.subs.proxad.net) |
| 11:35:19 | × | Topsi1 quits (~Tobias@dyndsl-095-033-095-132.ewe-ip-backbone.de) (Ping timeout: 272 seconds) |
| 11:35:34 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 11:35:34 | × | hmmmas quits (~chenqisu1@183.217.202.217) (Quit: Leaving.) |
| 11:36:03 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:36:12 | × | ru0mad quits (~ru0mad@82-64-17-144.subs.proxad.net) (Client Quit) |
| 11:37:18 | × | atwm quits (~andrew@178.197.235.239) (Ping timeout: 268 seconds) |
| 11:37:21 | → | ru0mad joins (~ru0mad@82-64-17-144.subs.proxad.net) |
| 11:37:37 | × | ru0mad quits (~ru0mad@82-64-17-144.subs.proxad.net) (Client Quit) |
| 11:39:26 | → | xsperry joins (~as@user/xsperry) |
| 11:47:22 | <arahael> | When I run 'cabal run', I often get the error 'Warning: Couldn't figure out C compiler information! Make sure you're using GNU gcc, or clang' on macos. Is there anything I can do to fix that? |
| 11:49:55 | <arahael> | Hmm, I have to get to bed - I'll ask another time. |
| 11:50:14 | <arahael> | tdammers: Oh, managed to catch you! Before I go, wanted to think you for Ginger. :) Using it for a small personal site that isn't online yet. :) |
| 11:50:45 | → | zebrag joins (~chris@user/zebrag) |
| 11:50:50 | → | Dynom joins (~niels@80-114-12-206.cable.dynamic.v4.ziggo.nl) |
| 11:51:14 | → | atwm joins (~andrew@178.197.235.239) |
| 11:56:07 | → | chisui joins (~chisui@200116b86662dd0045dcdbf42fb73e43.dip.versatel-1u1.de) |
| 11:56:13 | <xerox> | arahael: I wonder what's that about as well |
| 11:57:02 | × | atwm quits (~andrew@178.197.235.239) (Ping timeout: 268 seconds) |
| 11:57:05 | jpds1 | is now known as jpds |
| 11:57:12 | <arahael> | xerox: Not just me, then? Sweet. I'll have to get back in and ask about it again another day. |
| 11:57:22 | <xerox> | arahael: which version are you using? |
| 11:58:00 | <arahael> | xerox: Seems to be 8.8.4, using cabal-install 3.2.0.0 |
| 11:58:06 | <arahael> | xerox: On an M1. |
| 11:58:19 | <xerox> | me 8.10.4 on an m1 |
| 11:58:28 | <arahael> | I probably should upgrade - another time. |
| 12:02:34 | × | benin quits (~benin@183.82.177.19) (Ping timeout: 268 seconds) |
| 12:06:13 | → | benin joins (~benin@183.82.177.19) |
| 12:07:30 | × | gbd_628 quits (~gbd_628@c-73-160-244-80.hsd1.nj.comcast.net) (Quit: Client closed) |
| 12:07:30 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 264 seconds) |
| 12:07:33 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 12:09:21 | → | lavaman joins (~lavaman@98.38.249.169) |
| 12:09:43 | <merijn> | arahael, xerox: The C compiler is handled by GHC's configure script |
| 12:09:47 | <merijn> | but it's hacky as fuck |
| 12:09:56 | <merijn> | It breaks a lot |
| 12:10:50 | <merijn> | Things that have broke it for me: Having a stupid ancient clang that gets identified as gcc (and then breaks, because it considers clang 3.4 to have a bug that applies to gcc sub 4.4) |
| 12:11:08 | <merijn> | Having CUDA's nvcc installed changes clang's output on macOS, which also breaks it |
| 12:14:18 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 268 seconds) |
| 12:15:47 | → | bfrk1 joins (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) |
| 12:16:05 | → | sondre joins (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) |
| 12:18:00 | × | ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Ping timeout: 268 seconds) |
| 12:18:08 | bfrk1 | is now known as bfrk |
| 12:18:28 | → | ubikium joins (~ubikium@2400:2200:4f2:4b71:94bf:c634:be62:7c0d) |
| 12:18:30 | → | schuelermine joins (~schuelerm@2a02:3032:403:c9bf:a3eb:b0ef:ce:fa31) |
| 12:19:52 | × | ubikium quits (~ubikium@2400:2200:4f2:4b71:94bf:c634:be62:7c0d) (Read error: Connection reset by peer) |
| 12:20:06 | → | ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) |
| 12:21:45 | → | xprlgjf joins (~gavin@60.27.93.209.dyn.plus.net) |
| 12:22:52 | → | AgentM joins (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) |
| 12:24:43 | × | ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Ping timeout: 272 seconds) |
| 12:25:10 | → | ubikium joins (~ubikium@2400:2200:4f2:4b71:94bf:c634:be62:7c0d) |
| 12:30:37 | → | lavaman joins (~lavaman@98.38.249.169) |
| 12:31:58 | <schuelermine> | Hello |
| 12:32:32 | <schuelermine> | Does anybody know if GHC have any plans to add full dependent typing? |
| 12:33:07 | <schuelermine> | It’s kinda sad that most Optics need Template Haskell… |
| 12:33:59 | <maerwald> | schuelermine: https://github.com/ghc-proposals/ghc-proposals/pull/378 was accepted, but that isn't full dependent types |
| 12:34:08 | <maerwald> | and I hope we don't get it |
| 12:34:16 | <merijn> | Yeah |
| 12:34:24 | <merijn> | Dependent Haskell is a terrible idea, imo |
| 12:34:42 | <merijn> | I'm not super optimistic about Linear Haskell either |
| 12:35:38 | <schuelermine> | Isn’t linear Haskell basically implemented? |
| 12:35:50 | <kuribas> | merijn: better have a good compiler for idris then? |
| 12:35:58 | <schuelermine> | 8.10 has -XLinearTypes (or similar) |
| 12:36:08 | <opqdonut> | kuribas: that's my opinion, at least |
| 12:36:18 | <opqdonut> | I'd also rather have a haskell2020 standard than yet more experiments |
| 12:36:25 | <opqdonut> | oh well |
| 12:36:30 | × | benin quits (~benin@183.82.177.19) (Ping timeout: 268 seconds) |
| 12:36:34 | <schuelermine> | Also, why do you think dependent Haskell is a bad idea? |
| 12:36:44 | <maerwald> | a language that's designed from the ground up with dependent types in mind sounds like a better idea |
| 12:36:52 | <schuelermine> | true |
| 12:36:59 | <opqdonut> | yeah, that's pretty much it |
| 12:37:04 | <maerwald> | ppl are just turning haskell into C++ |
| 12:37:24 | <schuelermine> | Agda’s mixfix is fun |
| 12:38:39 | <maerwald> | also, why not have a language that compiles to haskell and has dependent types? Do you really want all of the features in one language? What's wrong with inter-operability? |
| 12:38:40 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 12:39:34 | <maerwald> | intellectual complexity is also a concern... I don't want to think about dependent types most of the time, unless I'm doing something rather odd and complicated |
| 12:39:40 | <merijn> | schuelermine: Haskell as-is isn't designed for dependent times and I expect retrofitting will make the user interface considerably worse |
| 12:39:54 | <merijn> | s/times/types |
| 12:39:55 | <beaky> | nice i like agda |
| 12:40:05 | <beaky> | agda is implemented in haskell i think |
| 12:40:10 | <merijn> | And big libraries moving to -XKitchenSink will force it on the entire ecosystem |
| 12:40:17 | <maerwald> | yes |
| 12:40:19 | <schuelermine> | hm |
| 12:40:27 | <maerwald> | ecosystem effects aren't considered in that proposal at all |
| 12:40:32 | → | brandonh joins (~brandonh@151.38.202.252) |
| 12:40:43 | <the-coot[m]> | maerwald: Agda can be compiled to Haskell; the problem is that in some way you loose control over the low level code (Haskell in this case). |
| 12:40:48 | <merijn> | schuelermine: I *like* dependent typs, I just don't like the as ad hoc, backwards incompatible change bolted onto a language not designed for it |
| 12:41:14 | <beaky> | i think agda has a ghc backend too that lets you compile agda as executables or libraries and use between haskell modules |
| 12:41:31 | <maerwald> | so, why don't we explore that, instead of mudding up Haskell |
| 12:41:48 | <merijn> | schuelermine: The appeal of, say, Idris and Agda is that there is only one syntax for type and value level that's identical |
| 12:41:55 | × | igghibu quits (~igghibu@37.120.201.126) (Quit: Textual IRC Client: www.textualapp.com) |
| 12:42:05 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 12:42:14 | <schuelermine> | I actually feel bolting it in ad hoc could help make it more discoverable |
| 12:42:17 | → | ksqsf joins (~textual@67.209.186.120.16clouds.com) |
| 12:42:19 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 12:42:19 | × | ksqsf quits (~textual@67.209.186.120.16clouds.com) (Client Quit) |
| 12:42:30 | <schuelermine> | excuse me |
| 12:42:32 | <merijn> | Haskell pretty explicitly has *different* type and value level syntax, and mixing them now is confusion where some things are correct, some aren't and some mean something different from what you expect |
| 12:42:43 | <schuelermine> | yeah |
| 12:43:04 | <merijn> | schuelermine: Have you looked at something like Idris before? Type level programming in Idris is *much* easier to learn/understand than Hasochism, imo |
| 12:43:17 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 268 seconds) |
| 12:43:25 | <schuelermine> | Is Idris better than Agda? |
| 12:44:37 | <schuelermine> | actually no wait |
| 12:44:37 | <schuelermine> | Does Idris have the same provable productiveness or termination restriction as Agda? |
| 12:45:12 | <beaky> | yes idris is more designed to be 'pacman complete' as edwin brady would say while also haveing the nice depdnendent types like agda (although it uses a different theory i think) |
| 12:45:24 | <schuelermine> | I have to leave, my battery is dead |
| 12:45:29 | <schuelermine> | Thanks |
| 12:45:45 | <tomsmeding> | rip battery |
| 12:45:52 | → | sondre joins (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) |
| 12:47:18 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Remote host closed the connection) |
| 12:50:06 | × | schuelermine quits (~schuelerm@2a02:3032:403:c9bf:a3eb:b0ef:ce:fa31) (Ping timeout: 264 seconds) |
| 12:50:41 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 264 seconds) |
| 12:51:17 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 12:51:42 | × | Guest31 quits (~textual@cpc146410-hari22-2-0-cust124.20-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com) |
| 12:52:42 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Remote host closed the connection) |
| 12:53:19 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:7d39:eb90:ba7d:df66) (Quit: WeeChat 2.8) |
| 12:53:54 | → | koishi_ joins (~koishi_@185.209.85.134) |
| 12:54:24 | → | eightball joins (~eight@162-226-201-119.lightspeed.tukrga.sbcglobal.net) |
| 12:58:08 | × | argento quits (~argent0@168.227.96.53) (Ping timeout: 252 seconds) |
| 12:58:42 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 268 seconds) |
| 13:01:15 | → | alx741 joins (~alx741@186.178.108.160) |
| 13:01:19 | → | sondre joins (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) |
| 13:01:32 | → | Guest43oreosplas joins (~Guest43or@ip5b40c0d8.dynamic.kabel-deutschland.de) |
| 13:01:40 | × | Guest43oreosplas quits (~Guest43or@ip5b40c0d8.dynamic.kabel-deutschland.de) (Client Quit) |
| 13:01:58 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds) |
| 13:02:05 | × | eightball quits (~eight@162-226-201-119.lightspeed.tukrga.sbcglobal.net) (Quit: Leaving) |
| 13:02:22 | → | eightball joins (~eight@162-226-201-119.lightspeed.tukrga.sbcglobal.net) |
| 13:03:22 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 13:04:04 | → | gentauro joins (~gentauro@user/gentauro) |
| 13:04:53 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) |
| 13:05:53 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 272 seconds) |
| 13:06:45 | × | koishi_ quits (~koishi_@185.209.85.134) (Quit: /ragequit) |
| 13:07:25 | × | eightball quits (~eight@162-226-201-119.lightspeed.tukrga.sbcglobal.net) (Quit: Leaving) |
| 13:09:44 | × | ku quits (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) (Read error: Connection reset by peer) |
| 13:09:47 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) (Ping timeout: 268 seconds) |
| 13:09:47 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 268 seconds) |
| 13:15:14 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 13:23:16 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 13:23:22 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 268 seconds) |
| 13:23:43 | → | argento joins (~argent0@168.227.96.53) |
| 13:28:44 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 13:30:17 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 13:31:16 | → | shryke joins (~shryke@91.103.43.254) |
| 13:33:53 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 13:34:35 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 265 seconds) |
| 13:35:14 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 13:37:47 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 13:39:30 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 244 seconds) |
| 13:42:08 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 252 seconds) |
| 13:42:08 | × | pe200012 quits (~pe200012@218.107.17.245) (Ping timeout: 252 seconds) |
| 13:42:27 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 13:43:14 | × | chaosite quits (~chaosite@user/chaosite) (Ping timeout: 252 seconds) |
| 13:43:18 | <tdammers> | arahael: I think you missed me by mere minutes, but I usually leave my server idling, so you can just ping me and I'll read later, most of the time. Anyway, glad you like ginger. |
| 13:43:18 | → | pe200012 joins (~pe200012@218.107.17.245) |
| 13:44:09 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 13:45:51 | <kuribas> | I think idris is more for practical programming, less for proving stuff. |
| 13:46:25 | <kuribas> | At least, I tried to prove stuff in idris, and I found it not very convenient. |
| 13:46:34 | <tdammers> | well yeah, that's its mission, isn't it - bring dependent types to a practical programming language. or, if you prefer, bring practical programming to a dependently typed language. |
| 13:47:04 | <kuribas> | A disadvantage is that you give up on HM type inference. |
| 13:47:44 | <tdammers> | Haskell doesn't do HM either |
| 13:48:54 | → | lbseale joins (~lbseale@ip72-194-54-201.sb.sd.cox.net) |
| 13:51:04 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 13:51:36 | → | cheater1__ joins (~Username@user/cheater) |
| 13:51:44 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 13:51:48 | cheater1__ | is now known as cheater |
| 13:54:23 | → | chaosite joins (~chaosite@user/chaosite) |
| 13:55:22 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 13:55:25 | × | kiwi_33 quits (~00000000@selfhost1.threedot14.com) (Ping timeout: 268 seconds) |
| 13:56:02 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 268 seconds) |
| 13:59:07 | × | chaosite quits (~chaosite@user/chaosite) (Ping timeout: 268 seconds) |
| 14:00:21 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 268 seconds) |
| 14:04:39 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 14:06:02 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:7d39:eb90:ba7d:df66) |
| 14:08:19 | → | Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 14:09:17 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 14:11:17 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 14:11:42 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 14:12:45 | × | connrs quits (~connrs@s1.connrs.uk) (Changing host) |
| 14:12:45 | → | connrs joins (~connrs@user/connrs) |
| 14:13:48 | → | atwm joins (~andrew@178.197.235.239) |
| 14:14:12 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 14:14:16 | → | jmcarthur joins (~textual@c-73-29-224-10.hsd1.nj.comcast.net) |
| 14:15:42 | → | nschoe joins (~quassel@178.251.84.79) |
| 14:17:29 | × | wonko quits (~wjc@user/wonko) (Remote host closed the connection) |
| 14:18:13 | → | ixlun joins (~user@109.249.184.235) |
| 14:18:47 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 14:19:01 | × | favonia quits (~favonia@user/favonia) (Quit: Ping timeout (120 seconds)) |
| 14:19:03 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 265 seconds) |
| 14:19:07 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 14:19:24 | → | favonia joins (~favonia@user/favonia) |
| 14:19:33 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 14:20:29 | → | cheater1__ joins (~Username@user/cheater) |
| 14:20:35 | <ixlun> | Hi all, I've got a Parsec parser and I'm trying to build a parsec parser. I've got the following: (<>) <$> option "" $ string "a" <*> option |
| 14:20:43 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 14:20:50 | → | allbery_b joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 14:20:51 | cheater1__ | is now known as cheater |
| 14:20:55 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Killed (NickServ (GHOST command used by allbery_b))) |
| 14:21:01 | allbery_b | is now known as geekosaur |
| 14:21:08 | <ixlun> | (<>) <$> option "" $ string "a" <*> option "" $ string "b" <*> option "" $ string "c" |
| 14:21:26 | × | jmcarthur quits (~textual@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: Textual IRC Client: www.textualapp.com) |
| 14:21:49 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 14:21:52 | <ixlun> | So I want to concatenate whatever string is parsed. Problem is (<>) only takes two strings to it's a type error. |
| 14:22:18 | <ixlun> | Is the best way to fix this to do something like: (<> . <>)? |
| 14:23:01 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 14:23:35 | <hpc> | :t (<>) |
| 14:23:35 | <lambdabot> | Semigroup a => a -> a -> a |
| 14:23:38 | <hpc> | :t mconcat |
| 14:23:39 | <lambdabot> | Monoid a => [a] -> a |
| 14:23:47 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 272 seconds) |
| 14:23:52 | → | kiweun joins (~sheepduck@2607:fea8:2a60:b700::5d55) |
| 14:23:54 | <hpc> | you probably want mconcat |
| 14:23:55 | <river> | :t (<> . <>) |
| 14:23:56 | <lambdabot> | error: parse error on input ‘.’ |
| 14:24:05 | <Hecate> | river: nice emoji |
| 14:24:16 | <ixlun> | :t ((<>) . (<>)) |
| 14:24:17 | <lambdabot> | Semigroup a => a -> (a -> a) -> a -> a |
| 14:24:22 | → | igghibu joins (~igghibu@37.120.201.126) |
| 14:24:25 | → | hughjfchen joins (~hughjfche@vmi556545.contaboserver.net) |
| 14:24:36 | <hpc> | mconcat [a, b, c, d] = a <> b <> c <> d <> mempty |
| 14:24:51 | → | jmcarthu_ joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 14:25:05 | → | aighearach_ joins (~paris@c-71-63-160-210.hsd1.or.comcast.net) |
| 14:25:22 | <Hecate> | % :t (\y -> (\x -> x <> y . y <> x)) |
| 14:25:23 | <yahb> | Hecate: Semigroup a => (a -> a) -> (a -> a) -> a -> a |
| 14:25:37 | <Hecate> | ah, you were faster ixlun |
| 14:25:51 | → | cheater1__ joins (~Username@user/cheater) |
| 14:26:03 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Killed (NickServ (GHOST command used by jmcarthu_))) |
| 14:26:13 | jmcarthu_ | is now known as jmcarthur |
| 14:26:20 | <ixlun> | The type of ((<>) . (<>)) isn't what I expected! |
| 14:26:31 | → | Megant_ joins (megant@user/megant) |
| 14:26:55 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 14:27:04 | <ixlun> | My intuition would have been: a -> a ->a |
| 14:27:17 | × | sheepduck quits (~sheepduck@2607:fea8:2a60:b700::5d55) (Read error: Connection reset by peer) |
| 14:27:17 | × | atwm quits (~andrew@178.197.235.239) (Ping timeout: 268 seconds) |
| 14:27:17 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 14:27:17 | × | xff0x quits (~xff0x@2001:1a81:528f:3900:63a6:c05a:b177:6450) (Ping timeout: 268 seconds) |
| 14:27:18 | × | Megant quits (megant@user/megant) (Ping timeout: 268 seconds) |
| 14:27:18 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Read error: Connection reset by peer) |
| 14:27:18 | × | otto_s_ quits (~user@p5de2fbac.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 14:27:23 | cheater1__ | is now known as cheater |
| 14:27:28 | × | hughjfchen quits (~hughjfche@vmi556545.contaboserver.net) (Remote host closed the connection) |
| 14:27:42 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 268 seconds) |
| 14:27:42 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 268 seconds) |
| 14:27:56 | → | xff0x joins (~xff0x@port-92-195-46-148.dynamic.as20676.net) |
| 14:27:58 | → | otto_s joins (~user@p5de2fbac.dip0.t-ipconnect.de) |
| 14:28:12 | × | aighearach quits (~paris@c-71-63-160-210.hsd1.or.comcast.net) (Ping timeout: 268 seconds) |
| 14:28:55 | × | Lycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Ping timeout: 268 seconds) |
| 14:28:55 | × | berberman_ quits (~berberman@user/berberman) (Ping timeout: 268 seconds) |
| 14:28:55 | × | jjhoo quits (jahakala@dsl-trebng21-58c18f-56.dhcp.inet.fi) (Ping timeout: 268 seconds) |
| 14:28:59 | → | jjhoo_ joins (~jahakala@dsl-trebng21-58c18f-56.dhcp.inet.fi) |
| 14:29:12 | Lord_of_Life_ | is now known as Lord_of_Life |
| 14:29:21 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 14:29:21 | × | smitop quits (uid328768@user/smitop) (Ping timeout: 268 seconds) |
| 14:29:21 | × | neceve quits (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130) (Ping timeout: 268 seconds) |
| 14:29:21 | × | riatre quits (~quassel@h203-145-233-111.ablenetvps.ne.jp) (Ping timeout: 268 seconds) |
| 14:29:22 | → | hughjfchen joins (~hughjfche@vmi556545.contaboserver.net) |
| 14:29:23 | → | riatre_ joins (~quassel@2001:310:6000:f::5198:1) |
| 14:29:58 | × | ruffy_ quits (~jonas@2a03:b0c0:3:d0::162e:a001) (Ping timeout: 268 seconds) |
| 14:30:07 | → | neceve joins (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130) |
| 14:30:24 | × | hughjfchen quits (~hughjfche@vmi556545.contaboserver.net) (Remote host closed the connection) |
| 14:30:36 | → | wagle joins (~wagle@quassel.wagle.io) |
| 14:30:40 | × | tremon quits (~tremon@217-63-61-89.cable.dynamic.v4.ziggo.nl) (Ping timeout: 268 seconds) |
| 14:31:11 | → | involans joins (~alex@cpc92718-cmbg20-2-0-cust157.5-4.cable.virginm.net) |
| 14:31:11 | → | smitop joins (uid328768@user/smitop) |
| 14:31:19 | → | hughjfchen joins (~hughjfche@vmi556545.contaboserver.net) |
| 14:31:20 | × | brandonh quits (~brandonh@151.38.202.252) (Ping timeout: 268 seconds) |
| 14:31:30 | × | hughjfchen quits (~hughjfche@vmi556545.contaboserver.net) (Client Quit) |
| 14:31:49 | × | AgentM quits (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) (Ping timeout: 268 seconds) |
| 14:31:50 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 14:32:26 | <tdammers> | :t mconcat <$> mapM (option "" . string) [ "a", "b", "c" ] |
| 14:32:27 | <lambdabot> | error: |
| 14:32:27 | <lambdabot> | • Variable not in scope: option :: [Char] -> b0 -> f b |
| 14:32:27 | <lambdabot> | • Perhaps you meant ‘optional’ (imported from Control.Applicative) |
| 14:32:30 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 14:32:30 | × | ornxka quits (~ornxka@user/ornxka) (Ping timeout: 268 seconds) |
| 14:32:47 | <tdammers> | something like that? |
| 14:32:48 | → | tremon joins (~tremon@217-63-61-89.cable.dynamic.v4.ziggo.nl) |
| 14:33:00 | → | berberman joins (~berberman@user/berberman) |
| 14:33:10 | → | atwm joins (~andrew@178.197.235.239) |
| 14:33:12 | × | bfrk quits (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) (Ping timeout: 268 seconds) |
| 14:33:12 | × | dyeplexer quits (~dyeplexer@user/dyeplexer) (Ping timeout: 268 seconds) |
| 14:33:23 | → | brandonh joins (~brandonh@151.38.202.252) |
| 14:33:29 | → | dyeplexer joins (~dyeplexer@user/dyeplexer) |
| 14:33:43 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 14:33:44 | × | anandprabhu quits (~anandprab@87.201.97.214) (Quit: Leaving) |
| 14:33:51 | <ski> | @type (fmap mconcat . sequenceA) [Text.Parsec.option "" (Text.Parsec.string "a"),Text.Parsec.option "" (Text.Parsec.string "b"),Text.Parsec.option "" (Text.Parsec.string "c")] |
| 14:33:53 | <lambdabot> | Text.Parsec.Prim.Stream s m Char => Text.Parsec.Prim.ParsecT s u m [Char] |
| 14:34:00 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 14:34:09 | → | whaletechho joins (~whaletech@user/whaletechno) |
| 14:34:25 | → | ornxka joins (~ornxka@user/ornxka) |
| 14:34:50 | → | ruffy_ joins (~jonas@2a03:b0c0:3:d0::162e:a001) |
| 14:34:51 | → | AgentM joins (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) |
| 14:35:14 | × | kuribas quits (~user@ptr-25vy0i7o5gw6tky01tr.18120a2.ip6.access.telenet.be) (Ping timeout: 268 seconds) |
| 14:35:14 | × | gawen quits (~gawen@user/gawen) (Ping timeout: 268 seconds) |
| 14:35:46 | → | gawen joins (~gawen@user/gawen) |
| 14:36:03 | → | kuribas`` joins (~user@ptr-25vy0i7o5gw6tky01tr.18120a2.ip6.access.telenet.be) |
| 14:36:08 | × | michalz quits (~user@185.246.204.55) (Ping timeout: 268 seconds) |
| 14:36:50 | <ixlun> | I like it! I didn't think of putting the parsing steps into an array and useing concat! |
| 14:37:04 | <ski> | s/array/list/ |
| 14:37:41 | × | atwm quits (~andrew@178.197.235.239) (Ping timeout: 252 seconds) |
| 14:37:52 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 14:38:01 | <ski> | (if all your parsing actions there are of that form, then something like tdammers' version would be nicer) |
| 14:38:52 | → | sifu joins (~marek@219.244.200.146.dyn.plus.net) |
| 14:38:52 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 14:39:20 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Ping timeout: 252 seconds) |
| 14:40:08 | <jmcarthur> | A semimodule over a semiring consists of a commutative monoid. Does anybody know if the commutativity of the monoid is inevitable from the other axioms or if it's just an extra property? If the latter, is there a name for a semimodule where the monoid is not commutative? |
| 14:40:12 | <ixlun> | I have to say, having written a full C parser with Bison, using Haskell for writing parsers is a dream! |
| 14:41:14 | → | michalz joins (~user@185.246.204.45) |
| 14:41:31 | <jmcarthur> | I have seen a proof that commutativity is inevitable in a module, but it made use of additive inverses. |
| 14:41:52 | × | kuribas`` quits (~user@ptr-25vy0i7o5gw6tky01tr.18120a2.ip6.access.telenet.be) (*.net *.split) |
| 14:41:52 | × | AgentM quits (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) (*.net *.split) |
| 14:41:52 | × | Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (*.net *.split) |
| 14:41:52 | × | otto_s quits (~user@p5de2fbac.dip0.t-ipconnect.de) (*.net *.split) |
| 14:41:52 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (*.net *.split) |
| 14:41:52 | × | Dynom quits (~niels@80-114-12-206.cable.dynamic.v4.ziggo.nl) (*.net *.split) |
| 14:41:52 | × | werneta quits (~werneta@mobile-166-176-57-108.mycingular.net) (*.net *.split) |
| 14:41:52 | × | whaletechno quits (~whaletech@user/whaletechno) (*.net *.split) |
| 14:41:52 | × | farn quits (~farn@2a03:4000:7:3cd:d4ab:85ff:feeb:f505) (*.net *.split) |
| 14:41:52 | × | np quits (znc@user/nerdypepper) (*.net *.split) |
| 14:42:05 | → | Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 14:43:19 | → | Dynom joins (~niels@80-114-12-206.cable.dynamic.v4.ziggo.nl) |
| 14:43:22 | <tdammers> | ixlun: there is a little itty bitty caveat, which is that recursive-descent parsers such as those you write in Parsec tend to perform worse than the kind of parsers you can build with bison/flex (or yacc/lex or whatever) |
| 14:43:44 | <hpc> | (or in haskell, alex/happy) |
| 14:43:45 | <tdammers> | though IMO the developer ergonomics you gain are almost always worth it |
| 14:43:46 | → | werneta joins (~werneta@mobile-166-176-57-108.mycingular.net) |
| 14:43:50 | <tdammers> | right, yeah |
| 14:44:02 | → | bfrk joins (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) |
| 14:44:08 | <jmcarthur> | I'm asking because I'm trying to work out a notion of "thickness" in alpha compositing, and I want to try to find a reasonable algebraic structure for it. Alpha compositing is not commutative, but I am looking something module-like to talk about thickness. |
| 14:44:18 | → | nerdypepper joins (znc@152.67.162.71) |
| 14:45:19 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 14:46:12 | <jmcarthur> | e.g. A thicker layer will be less transparent than a thinner one of the same material. Layering two sheets of equal thickness should be the same as one sheet of twice the thickness. |
| 14:46:22 | <ixlun> | tdammers: Agreed, I suppose each use case is different but the gains I get with writing a parser in this way far outweighs the performance loss. |
| 14:46:36 | × | mnrmnaugh quits (~mnrmnaugh@pool-96-252-87-182.bstnma.fios.verizon.net) (Ping timeout: 268 seconds) |
| 14:46:51 | → | slowButPresent joins (~slowButPr@user/slowbutpresent) |
| 14:46:55 | ← | bfrk parts (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) () |
| 14:47:19 | <tdammers> | ixlun: absolutely. I generally use (mega-)parsec myself, all else being equal |
| 14:47:37 | → | cheater1__ joins (~Username@user/cheater) |
| 14:47:47 | <tdammers> | frankly, I have yet to be in a situation where I can't get a recursive-descent parser to perform well enough for my needs. though those situations certainly do exist. |
| 14:47:51 | <ixlun> | One other question I've got. I've noticed that whenever I use (<|>), I almost always need to prefix the lhs with 'try' so that the rhs parser runs. Why doesn't (<|>) imply try on the lhs, or what is the case where you wouldn't want a try on the lhs? |
| 14:47:51 | × | cheater quits (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 14:47:59 | cheater1__ | is now known as cheater |
| 14:48:45 | <tdammers> | excessive use of "try" leads to useless error messages |
| 14:49:03 | <jmcarthur> | FWIW, the need to use try is kind of a quirk (not necessarily a flaw) of Parsec. Not all parser combinator libraries require it. |
| 14:49:17 | <tdammers> | and it can also make parsers more difficult to debug, and lead to performance drains |
| 14:49:21 | → | kuribas`` joins (~user@ptr-25vy0i7o5gw6tky01tr.18120a2.ip6.access.telenet.be) |
| 14:49:21 | → | AgentM joins (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) |
| 14:49:21 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 14:49:21 | → | otto_s joins (~user@p5de2fbac.dip0.t-ipconnect.de) |
| 14:49:21 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 14:49:21 | → | farn joins (~farn@2a03:4000:7:3cd:d4ab:85ff:feeb:f505) |
| 14:49:41 | <tdammers> | you should only wrap in "try" those parts of your parsers that you need to backtrack on in case they don't succeed |
| 14:50:18 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 268 seconds) |
| 14:50:24 | → | pavonia joins (~user@user/siracusa) |
| 14:50:43 | <tdammers> | for example, if you have a parser like string "{{" *> someExpression <* string "}}", then you don't want to wrap the whole thing in try, but rather just the first bit (the string "{{") part, because once you have seen a "{{", you are committed to parsing a {{ }} block |
| 14:50:44 | <jmcarthur> | You can sometimes avoid using try, or at least avoid backtracking really far, with some thoughtful refactoring. |
| 14:50:55 | <jmcarthur> | ^^ yeah like that |
| 14:52:22 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 14:52:28 | <ixlun> | Right, so 'try' gives you control over when to backtrack. |
| 14:52:32 | <tdammers> | megaparsec, unlike parsec, implicitly wraps more constructs in try, so you don't need to explicitly try very often, at least if your parser is structured somewhat nicely, and the grammar isn't insane |
| 14:52:43 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 272 seconds) |
| 14:53:08 | <tdammers> | yes. "try" means "if the argument fails, undo any consuming the argument may have done, and then fail" |
| 14:53:49 | <ixlun> | One thing that would be nice to see is if you could pass a set of megaparsec combinators to a program and it spits out the grammar for you. I know Bison gives you a really nice print out of your grammar in debug mode. |
| 14:54:00 | × | gehmehgeh quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 14:54:16 | <tdammers> | so, say you write a parser like so: string "hello" <|> string "world". And now you feed it the input "helo". The lhs is tried first, and it starts consuming things as long as they match: h, e, l, but then it sees "o" where it expects "l", and fails |
| 14:54:37 | <tdammers> | but at that point, it has already consumed 3 characters from the input, and that isn't undone as you head into the rhs of the <|> |
| 14:54:50 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 14:54:58 | <tdammers> | so the rhs now starts working on the remaining input, "o", instead of the whole thing, "helo", as it should have |
| 14:55:00 | → | mnrmnaugh joins (~mnrmnaugh@pool-96-252-87-182.bstnma.fios.verizon.net) |
| 14:55:28 | <jmcarthur> | In order to spit out a grammar like that, the interface could not be monadic, at least not in the way parsec is. It's more plausible for a less powerful combinator library to do this, though. |
| 14:55:32 | <tdammers> | however, wrap the lhs in "try", and it will backtrack when it fails, rolling back to the input reading "helo", and the rhs operates on that |
| 14:56:33 | <hpc> | in other words, (string "hello" <|> string "world") will successfully parse "helworld" |
| 14:57:30 | <jmcarthur> | Hmm... maybe there are other problems with my semimodule idea. It's not clear to me that thickness*(a + b) should be the same as thickness*a + thickness*b. |
| 14:58:08 | <ixlun> | Ah interesting. so by not using 'try' you may parse inputs that you aren't expecting too |
| 14:58:52 | <hpc> | jmcarthur: think of it as sequencing operations, maybe? |
| 14:59:16 | → | notzmv joins (~zmv@user/notzmv) |
| 15:00:35 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 15:00:38 | <ski> | % parse (string "hello" <|> string "world") "" "helworld" |
| 15:00:38 | <yahb> | ski: Left (line 1, column 1):; unexpected "w"; expecting "hello" |
| 15:00:58 | → | favonia joins (~favonia@user/favonia) |
| 15:01:11 | <jmcarthur> | hpc: If thickness was restricted to natural numbers, sure, and I could just stick with a monoid for the whole thing, but I am trying to come up with an approach that allows thicknesses to be nonnegative reals. |
| 15:01:28 | <jmcarthur> | My plan is to try to define that (*) operation, once I figure out what its properties should be. |
| 15:02:05 | × | cheater quits (~Username@user/cheater) (Ping timeout: 264 seconds) |
| 15:02:12 | → | cheater1__ joins (~Username@user/cheater) |
| 15:02:14 | cheater1__ | is now known as cheater |
| 15:02:16 | <jmcarthur> | Maybe even negative reals if that happens to work out nicely, but it's not a requirement. |
| 15:02:39 | × | Lycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 15:05:05 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 15:06:07 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) |
| 15:06:56 | → | aditya joins (~aditya@106.212.79.20) |
| 15:06:58 | → | Shaeto joins (~Shaeto@94.25.234.55) |
| 15:08:12 | → | wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com) |
| 15:09:40 | × | nschoe quits (~quassel@178.251.84.79) (Remote host closed the connection) |
| 15:09:55 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 15:11:06 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) (Ping timeout: 264 seconds) |
| 15:12:54 | → | nschoe joins (~quassel@178.251.84.79) |
| 15:12:59 | → | chomwitt joins (~Pitsikoko@athedsl-20549.home.otenet.gr) |
| 15:13:52 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 15:14:17 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 15:16:16 | × | Shaeto quits (~Shaeto@94.25.234.55) (Quit: WeeChat 3.1) |
| 15:16:35 | → | atwm joins (~andrew@178.197.235.239) |
| 15:18:33 | × | sh9 quits (~sh9@softbank060116136158.bbtec.net) (Quit: WeeChat 3.0.1) |
| 15:21:48 | × | nschoe quits (~quassel@178.251.84.79) (Ping timeout: 244 seconds) |
| 15:22:35 | → | nschoe joins (~quassel@178.251.84.79) |
| 15:23:12 | × | aditya quits (~aditya@106.212.79.20) (Read error: Connection reset by peer) |
| 15:23:15 | <jmcarthur> | I think this stackoverflow question is basically about what I'm looking for https://mathoverflow.net/questions/208412/what-are-some-examples-of-non-commutative-mathbbq-monoids-and-or-mathbbr |
| 15:23:44 | → | Shaeto joins (~Shaeto@94.25.234.55) |
| 15:24:59 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 15:25:56 | → | lbseale_ joins (~lbseale@ip72-194-54-201.sb.sd.cox.net) |
| 15:26:19 | <opqdonut> | mmmmh... mathbbq |
| 15:26:41 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 264 seconds) |
| 15:27:01 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 15:27:46 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 15:27:51 | × | atwm quits (~andrew@178.197.235.239) (Quit: WeeChat 3.1) |
| 15:28:49 | × | sifu quits (~marek@219.244.200.146.dyn.plus.net) (Remote host closed the connection) |
| 15:29:06 | × | lbseale quits (~lbseale@ip72-194-54-201.sb.sd.cox.net) (Ping timeout: 264 seconds) |
| 15:29:31 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 15:30:35 | × | argento quits (~argent0@168.227.96.53) (Ping timeout: 265 seconds) |
| 15:31:01 | → | xkapastel joins (uid17782@id-17782.tinside.irccloud.com) |
| 15:31:34 | × | brandonh quits (~brandonh@151.38.202.252) (Quit: brandonh) |
| 15:32:05 | × | nschoe quits (~quassel@178.251.84.79) (Ping timeout: 264 seconds) |
| 15:32:15 | → | nschoe joins (~quassel@2a04:cec0:118b:9ec7:c878:346:7ebb:d0f1) |
| 15:32:40 | → | boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com) |
| 15:32:51 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 268 seconds) |
| 15:33:26 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 15:33:46 | → | pe200012_ joins (~pe200012@120.236.162.14) |
| 15:33:46 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:7d39:eb90:ba7d:df66) (Ping timeout: 264 seconds) |
| 15:33:54 | × | pe200012 quits (~pe200012@218.107.17.245) (Ping timeout: 264 seconds) |
| 15:35:11 | → | imdoor joins (~imdoor@balticom-142-78-50.balticom.lv) |
| 15:35:12 | × | rahguzar quits (~rahguzar@212.189.140.214) (Quit: Connection closed) |
| 15:35:18 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 15:35:35 | → | rahguzar joins (~rahguzar@212.189.140.214) |
| 15:36:18 | → | lbseale joins (~lbseale@ip72-194-54-201.sb.sd.cox.net) |
| 15:36:33 | × | lbseale_ quits (~lbseale@ip72-194-54-201.sb.sd.cox.net) (Ping timeout: 268 seconds) |
| 15:39:54 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 264 seconds) |
| 15:40:28 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 15:41:20 | × | boioioing quits (~boioioing@cpe-76-84-141-127.neb.res.rr.com) (Quit: Gorn... bye...) |
| 15:41:29 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 268 seconds) |
| 15:41:54 | → | chddr joins (~Thunderbi@31.148.23.125) |
| 15:42:21 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 15:44:10 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 15:44:14 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:3866:f955:de69:46b2) |
| 15:44:33 | × | poljar1 quits (~poljar@78-2-43-255.adsl.net.t-com.hr) (Remote host closed the connection) |
| 15:44:48 | → | bor0 joins (~boro@77.28.64.72) |
| 15:44:57 | → | poljar1 joins (~poljar@78-2-43-255.adsl.net.t-com.hr) |
| 15:45:18 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 15:45:29 | × | imdoor quits (~imdoor@balticom-142-78-50.balticom.lv) (Quit: imdoor) |
| 15:48:17 | → | boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com) |
| 15:48:47 | <bor0> | Hi. I have a sort of mathematical question, but it has to do with my implementation of a number theory in Haskell. Suppose we have a formula `A = B` and a rule that converts `x = y` to `S x = S y`. Now, applying this rule to `A = B` makes sense, we get as output `S A = S B`. But, what about applying rules to subformulas? Are there any restrictions? E.g. applying `S x = S y` to `A = B` within `A = B /\ C = D`. My system is currently broken in that it can convert |
| 15:48:47 | <bor0> | a formula from `A=B /\ Exists B:(B=C)` to `A=B /\ B=C`, so likely I'm missing some restriction around bound variables or something. Happy to elaborate further on the question! |
| 15:49:05 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:3866:f955:de69:46b2) (Ping timeout: 272 seconds) |
| 15:49:51 | × | rahguzar quits (~rahguzar@212.189.140.214) (Quit: Connection closed) |
| 15:49:59 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 15:50:14 | <river> | > what about applying rules to subformulas? Are there any restrictions? |
| 15:50:15 | <lambdabot> | <hint>:1:70: error: |
| 15:50:15 | <lambdabot> | parse error (possibly incorrect indentation or mismatched brackets) |
| 15:50:31 | → | rahguzar joins (~rahguzar@212.189.140.214) |
| 15:50:34 | × | Shaeto quits (~Shaeto@94.25.234.55) (Quit: WeeChat 3.1) |
| 15:50:39 | <river> | a subformula can be defined as a context with a hole |
| 15:50:54 | <river> | and if x = y then C[x] = C[y] |
| 15:51:01 | <river> | so you can rewrite in subformulas |
| 15:51:18 | → | Shaeto joins (~Shaeto@94.25.234.55) |
| 15:51:40 | <tomsmeding> | are you asking how to do rewriting in general in terms with bound variables? |
| 15:51:46 | <bor0> | Yes! |
| 15:51:56 | <tomsmeding> | anything more specific would require knowledge about how you're representing things :p |
| 15:52:03 | <ski> | yes |
| 15:52:18 | <tomsmeding> | is this perhaps a case where you want capture-avoiding substitution? (that might be a good web-search term) |
| 15:52:51 | <bor0> | It's all in https://github.com/bor0/hoare-imp/blob/master/src, though I don't expect anyone to go through the 500 LoC to just answer my question :) |
| 15:52:55 | <tomsmeding> | i.e. if you're substituting a variable x with an expression E, then you are not allowed to substitute under a binder that binds x |
| 15:53:00 | <ski> | bor0 : how is it elimianting the existential, in that example ? |
| 15:53:43 | <bor0> | Hey ski! Basically it's the Path traversal function, if you recall. Right now it just ignores quantifiers https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L66-L67 and I am sure that's the error |
| 15:54:02 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 15:54:36 | <bor0> | Thanks, tomsmeding. That's helpful, I'll dig more into that |
| 15:54:40 | <tomsmeding> | what does FOL stand for? |
| 15:54:49 | <bor0> | "First-Order Logic" |
| 15:54:58 | <tomsmeding> | oh right |
| 15:54:59 | <ski> | you could have a rule that says that if `phi0' implies `phi1', and `psi0' implies `psi1', then `phi0 /\ psi0' implies `phi1 /\ psi1' |
| 15:55:33 | <ski> | (and ditto for other connectives) |
| 15:56:33 | <bor0> | So from GEB there was this restriction which kinda patched another similar issue - https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L219. This is why I'm suspecting around bound variables. What you suggested might work, though it'd probably require a bigger refactor.. |
| 15:57:14 | × | boioioing quits (~boioioing@cpe-76-84-141-127.neb.res.rr.com) (Quit: Gorn... bye...) |
| 15:57:52 | → | ku joins (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) |
| 15:57:59 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 15:58:04 | <tomsmeding> | bor0: can you give an example call of that function applyFOLRule that goes wrong? |
| 15:58:19 | × | ku quits (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) (Max SendQ exceeded) |
| 15:58:45 | × | prite quits (~pritam@user/pritambaral) (Ping timeout: 268 seconds) |
| 15:58:52 | → | ku joins (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) |
| 15:58:55 | <tomsmeding> | to me it kind of looks like applyFOLRule in itself is quite fine, but it lays some restrictions on what Paths are fine |
| 15:59:05 | <bor0> | Sure: it's in https://github.com/bor0/hoare-imp/commit/d891212a5f7cbf26483f8051fab57e36ab6641f2 |
| 15:59:37 | → | brandonh joins (~brandonh@151.38.151.222) |
| 15:59:41 | <bor0> | Though, e.g. `applyFOLRule [GoLeft] ruleAddS (A = B /\ C = D)` (pseudo-code) works fine - S A = S B /\ C = D |
| 15:59:53 | × | Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection) |
| 15:59:56 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 16:00:08 | → | Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 16:00:40 | <bor0> | So basically `applyFOLRule` within `applyFOLRule` easily exploits it |
| 16:00:53 | → | boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com) |
| 16:01:11 | → | schuelermine joins (~anselmsch@ip5b409cba.dynamic.kabel-deutschland.de) |
| 16:01:12 | <bor0> | Or maybe the problem is `applyFOLRule` within `applyFOLRule` on the _same_ formula... |
| 16:02:00 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 265 seconds) |
| 16:02:04 | ← | boioioing parts (~boioioing@cpe-76-84-141-127.neb.res.rr.com) () |
| 16:02:23 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 252 seconds) |
| 16:02:24 | <tomsmeding> | bor0: what does it even mean to have a path [GoLeft,GoRight] for a formula that has only one And? |
| 16:02:34 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 16:03:21 | <bor0> | Here's the full definition of it: https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L61-L76. In this case, it will just apply the function at the "bottom" |
| 16:03:39 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 16:04:00 | <tomsmeding> | that sounds like a convenience laxness that you'd not want in a logic system |
| 16:04:10 | <tomsmeding> | but maybe that's me :) |
| 16:04:47 | <bor0> | Yeah, I should make that stricter and make it return either an error or a proof like others |
| 16:05:30 | × | ku quits (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) (Remote host closed the connection) |
| 16:05:56 | → | boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com) |
| 16:05:59 | → | ku joins (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) |
| 16:06:08 | × | dpl quits (~dpl@77-121-78-163.chn.volia.net) (Remote host closed the connection) |
| 16:06:09 | × | xkapastel quits (uid17782@id-17782.tinside.irccloud.com) (Quit: .) |
| 16:06:29 | → | dpl joins (~dpl@77-121-78-163.chn.volia.net) |
| 16:06:39 | → | prite joins (~pritam@user/pritambaral) |
| 16:06:49 | <tomsmeding> | yeah so in terms of logic, what's going wrong there is that you have a proof prfAeqB that claims A=B, and you're applying that under an 'exists B' binder |
| 16:06:58 | <tomsmeding> | which of course defines a different B |
| 16:07:16 | × | schuelermine quits (~anselmsch@ip5b409cba.dynamic.kabel-deutschland.de) (Quit: WeeChat 3.1) |
| 16:07:53 | <tomsmeding> | one different way to approach this might be to adopt a convention that bound variables never shadow a free variable |
| 16:07:55 | × | favonia quits (~favonia@user/favonia) (Quit: The Lounge - https://thelounge.chat) |
| 16:08:45 | × | zebrag quits (~chris@user/zebrag) (Remote host closed the connection) |
| 16:09:01 | <tomsmeding> | I believe that's called the Barendregt convention, but I may be mistaken |
| 16:09:22 | <tomsmeding> | as long as you always ensure that this is the case, you can rewrite freely and you'll never shadow anything |
| 16:09:30 | → | Ariakenom joins (~Ariakenom@2001:9b1:efb:fc00:84c1:f198:927e:8e8c) |
| 16:09:51 | <tomsmeding> | but I'm not sure if that's practical to achieve in your system |
| 16:10:53 | × | shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 244 seconds) |
| 16:10:56 | <tomsmeding> | bor0: this function that gets passed to applyFOLRule, does that really need to be a full Haskell function? Could it perhaps also be some kind of expression with a hole? |
| 16:11:23 | <bor0> | It's a full Haskell function, but limited to rule*. E.g. https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L255 |
| 16:11:24 | × | cheater quits (~Username@user/cheater) (Ping timeout: 244 seconds) |
| 16:11:46 | <tomsmeding> | if you could inspect that "function" inside applyFOLRule, then when you descend below a binder, you could check whether the bound variable name exists anywhere within the function, and if so, first rename the binder to something fresh |
| 16:11:59 | <tomsmeding> | but you can't look inside a Haskell function, so you can't currently do that |
| 16:12:03 | → | cheater joins (~Username@user/cheater) |
| 16:12:10 | → | Bartosz joins (~textual@24.35.90.211) |
| 16:12:34 | <bor0> | I'm okay to just error on it e.g. like https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L237. But I am unsure about the condition on which to error... |
| 16:12:40 | <tomsmeding> | will the output of that function always be a single equality? |
| 16:13:10 | <bor0> | well you can applyFOLRule ruleSymmetry within A=B/\B=C/\D=E to get A=C/\D=E |
| 16:13:17 | <bor0> | This is the case where it works :) |
| 16:13:26 | <tomsmeding> | the condition is that the function f itself, without its parameter, contains a reference to a variable with the same name as the binder you're descending under in applyFOLRule |
| 16:13:38 | <tomsmeding> | but you can't currently check that criterion because Haskell function |
| 16:14:10 | <tomsmeding> | bor0: but then the output of 'f' (here ruleSymmetry) will still be a single equality, right? |
| 16:14:41 | <tomsmeding> | oh wait no it's more general |
| 16:15:32 | <tomsmeding> | bor0: am I at least kind of clear in what I mean when I say that f does or doesn't contain a reference to a variable? :p |
| 16:17:14 | <tomsmeding> | in the example from that commit, you're descending under a binder that binds B, but the function f is basically (\expr -> rewrite B to A in expr) |
| 16:17:41 | × | chddr quits (~Thunderbi@31.148.23.125) (Ping timeout: 264 seconds) |
| 16:17:48 | <tomsmeding> | so f mentions the free B, but the binder now shadows that B, hence the wrong answer |
| 16:18:14 | <bor0> | Yeah, right now `f` does not have any knowledge about variables. :) |
| 16:18:23 | <bor0> | It's just getting blindly applied |
| 16:19:29 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection) |
| 16:19:44 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 268 seconds) |
| 16:20:02 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 16:20:09 | × | jess quits (~jess@libera/staff/jess) () |
| 16:20:24 | → | jess joins (~jess@libera/staff/jess) |
| 16:20:35 | → | o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) |
| 16:21:50 | <tomsmeding> | I wonder how much of your code would still work if your applyFOLRule gets reduced to taking a variable name A, an expression F, and an expression E, where it replaces all free occurrences of A with F in E |
| 16:22:18 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 16:22:54 | <tomsmeding> | that's a well-understood function where you can easily check, when going under a binder for B in E, whether A=B (and if so, stop recursing), or if B is free in F (and if so, first rename the binder of B to a fresh variable, and then continue recursing) |
| 16:23:01 | <tomsmeding> | that's capture-avoiding substitution |
| 16:23:12 | <tomsmeding> | but it only works if you can inspect A and F |
| 16:24:13 | <tomsmeding> | alternative: use "partial De Bruijn" indices, which is a name I just thought up |
| 16:24:31 | <tomsmeding> | represent free variables like you do now, but use De Bruijn indices for all bound variables |
| 16:24:43 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 265 seconds) |
| 16:24:52 | <tomsmeding> | then you kind of automatically have to adhere to the Barendregt convention |
| 16:25:08 | <bor0> | Hey! I was working on this example and just when I was about to paste it I saw that you are actually hosting the pastebin, lol! <3 |
| 16:25:20 | coot | is now known as the-coot |
| 16:25:30 | <tomsmeding> | working with De Bruijn indices does make some things quite a bit more difficult, but those are exactly the points where you should watch out with shadowing anyway :p |
| 16:25:33 | <bor0> | https://paste.tomsmeding.com/2MU96uol this is an answer to "but then the output of 'f' (here ruleSymmetry) will still be a single equality, right?" |
| 16:25:37 | <tomsmeding> | bor0: :) |
| 16:26:51 | <bor0> | I am okay with even a simpler solution - don't do any variable replacement, just crash when the programmer tries to prove something using it |
| 16:26:57 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 16:27:17 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 16:27:22 | <tomsmeding> | but then you still have to detect the problem! |
| 16:27:28 | <tomsmeding> | and you need the same things for that |
| 16:27:43 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 272 seconds) |
| 16:28:21 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 272 seconds) |
| 16:29:04 | <tomsmeding> | bor0: ok right good example, you really use the generality of a full Haskell function |
| 16:29:10 | <bor0> | I had similar problem with `ruleGeneralize`. The way I solved it was to accept a list of variables (in the premise): https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L219-L225 |
| 16:29:37 | × | rahguzar quits (~rahguzar@212.189.140.214) (Ping timeout: 272 seconds) |
| 16:29:38 | <bor0> | When we are not in a fantasy (within implication really) this is how we use it: https://github.com/bor0/hoare-imp/blob/fdb70a94a7e49ddff4e12c4096996f9c619a204c/examples/ExampleTNT2.hs#L118. When we are in a fantasy, we have to pass the premise `(Just premise)`. https://github.com/bor0/hoare-imp/blob/fdb70a94a7e49ddff4e12c4096996f9c619a204c/examples/ExampleTNT2.hs#L129 |
| 16:30:11 | <ski> | (why the `fromRight's in the example ?) |
| 16:30:42 | × | nschoe quits (~quassel@2a04:cec0:118b:9ec7:c878:346:7ebb:d0f1) (Remote host closed the connection) |
| 16:30:58 | <bor0> | It's a dirty hack to avoid nested `whenRight`s https://github.com/bor0/hoare-imp/blob/master/src/Common.hs#L6-L12 |
| 16:31:56 | → | nschoe joins (~quassel@2a04:cec0:118b:9ec7:45a:fcee:e159:4f31) |
| 16:32:21 | <tomsmeding> | I'm not sure how to solve your problem in a nice way tbh; what I would do, probably, is encode the axioms of my logic in a data type instead of Haskell functions, and work with that |
| 16:32:32 | <tomsmeding> | hence ensuring you can always inspect everything |
| 16:32:38 | × | myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 252 seconds) |
| 16:32:40 | × | chomwitt quits (~Pitsikoko@athedsl-20549.home.otenet.gr) (Ping timeout: 268 seconds) |
| 16:32:45 | <tomsmeding> | you also get the ability to print out proofs that way :) |
| 16:33:05 | <bor0> | Ah! :) Yeah.. Proofs right now are just basically Haskell functions |
| 16:33:18 | <bor0> | I get to use all the fancy stuff like let = ... etc for free |
| 16:33:26 | <tomsmeding> | Maybe there's a way to ensure your implementation never goes wrong, but I think it's a very risky endeavour :) |
| 16:33:29 | <bor0> | But it seems it isn't really for free.. |
| 16:33:36 | <tomsmeding> | yeah |
| 16:33:51 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 16:34:08 | <tomsmeding> | I have to go though; good luck :) |
| 16:34:35 | <bor0> | Thank you! Discussion was great. I will look into the bits you suggested earlier and see if it's easy to incorporate some of them with small refactors :) |
| 16:35:22 | × | whaletechho quits (~whaletech@user/whaletechno) (Quit: ha det bra) |
| 16:35:23 | → | myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net) |
| 16:36:53 | × | Topsi quits (~Tobias@dyndsl-095-033-095-132.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 16:36:59 | <ski> | bor0 : `whenRight' is called `(>>=)' |
| 16:37:29 | <ski> | @src Either (>>=) |
| 16:37:29 | <lambdabot> | Left l >>= _ = Left l |
| 16:37:29 | <lambdabot> | Right r >>= k = k r |
| 16:37:36 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 16:38:05 | × | oxide quits (~lambda@user/oxide) (Ping timeout: 264 seconds) |
| 16:38:07 | <bor0> | Hah. I now need to rewrite all the examples! :D Thanks ski. That's definitely an improvement! |
| 16:39:18 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 16:39:24 | → | schuelermine joins (~anselmsch@user/schuelermine) |
| 16:39:38 | → | oxide joins (~lambda@user/oxide) |
| 16:40:30 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:40:48 | → | Jeanne-Kamikaze joins (~Jeanne-Ka@static-198-54-133-134.cust.tzulo.com) |
| 16:41:00 | <ski> | it seems like `applyFOLRule' should perhaps allow its callback to possibly fail .. if it's going to be an arbitrary (uninspectable) Haskell function |
| 16:41:53 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 244 seconds) |
| 16:45:19 | → | imdoor joins (~imdoor@balticom-142-78-50.balticom.lv) |
| 16:45:27 | × | notzmv quits (~zmv@user/notzmv) (Read error: Connection reset by peer) |
| 16:46:55 | <kuribas``> | Why does cassava have so crappy error handling? |
| 16:46:56 | <bor0> | What if `go` keeps track of the bound variables, and if one of those appear in `x` within https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L65 then just error? |
| 16:47:03 | × | Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 16:47:41 | <bor0> | That's probably too strict... |
| 16:48:12 | → | Deide joins (~Deide@wire.desu.ga) |
| 16:48:12 | × | Deide quits (~Deide@wire.desu.ga) (Changing host) |
| 16:48:12 | → | Deide joins (~Deide@user/deide) |
| 16:50:18 | × | igghibu quits (~igghibu@37.120.201.126) (Quit: Textual IRC Client: www.textualapp.com) |
| 16:50:22 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 16:51:10 | × | the-coot quits (~coot@37.30.49.19.nat.umts.dynamic.t-mobile.pl) (Quit: the-coot) |
| 16:51:11 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 16:51:13 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 16:52:41 | → | mononote joins (~mononote@user/mononote) |
| 16:55:19 | → | rahguzar joins (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) |
| 16:56:05 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 16:58:20 | × | mononote quits (~mononote@user/mononote) (Quit: Quit) |
| 16:58:47 | × | brandonh quits (~brandonh@151.38.151.222) (Read error: Connection reset by peer) |
| 16:59:15 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 17:01:29 | × | sciencentistguy quits (~sciencent@194.110.13.3) (Ping timeout: 264 seconds) |
| 17:02:25 | <ski> | bor0 : fwiw, i dunno why "Using `applyFOLRule` within `applyFOLRule` is not allowed." |
| 17:02:45 | <bor0> | It's a temporary patch to avoid this error :) |
| 17:02:58 | <ski> | it seems to me it would naturally satisfy a distributive law |
| 17:03:01 | <bor0> | (Until I/we get it right xD) |
| 17:03:17 | <dminuoso> | kuribas``: No idea, but it's a recurring theme. |
| 17:03:23 | <dminuoso> | Perhaps you can help and improve it? |
| 17:03:56 | <kuribas``> | dminuoso: if they don't mind breaking changes... |
| 17:04:08 | → | shiraeeshi joins (~shiraeesh@109.166.59.30) |
| 17:04:26 | <ski> | bor0 : a minor thing, there's no need to pass `f' as a parameter to `go' |
| 17:04:43 | <ski> | (since it never changes) |
| 17:04:58 | → | bfrk joins (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) |
| 17:05:00 | <kuribas``> | dminuoso: for example, FromNamedRecord returning a structured error, with column and row information |
| 17:05:17 | <dminuoso> | kuribas``: I suspect the poor diagnostics is from ruthless usage of attoparsec. :-) |
| 17:05:34 | <ski> | (you will need `ScopedTypeVariables' to have a type signature on `go', though, if you go for that) |
| 17:06:00 | <kuribas``> | dminuoso: that could be it... |
| 17:06:46 | × | nschoe quits (~quassel@2a04:cec0:118b:9ec7:45a:fcee:e159:4f31) (Ping timeout: 265 seconds) |
| 17:07:19 | → | econo joins (uid147250@user/econo) |
| 17:07:22 | × | waleee quits (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Ping timeout: 264 seconds) |
| 17:08:02 | <ski> | bor0 : where's `PropCalc' and `FOL' (and `Arith') defined ? |
| 17:08:26 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 17:08:29 | → | dpl_ joins (~dpl@77-121-78-163.chn.volia.net) |
| 17:08:30 | <bor0> | https://github.com/bor0/hoare-imp/blob/master/src/Gentzen.hs and https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs |
| 17:08:40 | → | cheater joins (~Username@user/cheater) |
| 17:08:44 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 17:09:15 | → | mikoto-chan joins (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) |
| 17:09:18 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 17:09:25 | <dminuoso> | kuribas``: Realistically the only thing you can do in attoparsec, is decorate stuff with (<?>) |
| 17:09:56 | → | notzmv joins (~zmv@user/notzmv) |
| 17:09:59 | <kuribas``> | dminuoso: still, adding column and row info seems very doable... |
| 17:10:16 | <kuribas``> | dminuoso: as attoparsec only needs to split the rows into columns. |
| 17:10:32 | → | peach joins (sid482179@id-482179.charlton.irccloud.com) |
| 17:10:46 | <dminuoso> | kuribas``: column/row info? |
| 17:10:55 | <dminuoso> | How can you even track that? |
| 17:11:12 | <dminuoso> | This is not megaparsec where you can add some monadic state |
| 17:11:31 | × | dpl quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 268 seconds) |
| 17:11:48 | <kuribas``> | dminuoso: parse in two steps, step one is split row into fields |
| 17:11:54 | <kuribas``> | as a list |
| 17:11:58 | <bor0> | ski, Interestingly, applyPropRule doesn't seem to have the same defect https://github.com/bor0/hoare-imp/blob/master/src/Gentzen.hs#L31. Likely because it doesn't have any support for quantifiers |
| 17:12:01 | <kuribas``> | then parse each list |
| 17:12:03 | → | brandonh joins (~brandonh@151.38.139.116) |
| 17:12:06 | <kuribas``> | list element |
| 17:12:21 | <dminuoso> | kuribas``: I suspect this drastically impact performance |
| 17:12:35 | <dminuoso> | Since you'd be running many tiny attoparsec parsers for each row |
| 17:12:55 | <kuribas``> | I would care more about good errors than blazing performance |
| 17:13:53 | <dminuoso> | Then your goals are incompatible with cassavas goal, which strives to be competitive with pythons 'cvs' |
| 17:13:55 | <dminuoso> | *csv |
| 17:14:45 | <dminuoso> | kuribas``: What one could do, is rework `cassava` to work with `parsers` perhaps, so you can re-parse with trifecta and generate better error messages? |
| 17:14:51 | <dminuoso> | Im not sure how viable this is, though. |
| 17:15:25 | <kuribas``> | I suppose I could parse into (Vector (Vector ByteString)), then use my own parser ByteString -> a |
| 17:15:38 | <kuribas``> | that would not be so hard to implement |
| 17:15:47 | × | imdoor quits (~imdoor@balticom-142-78-50.balticom.lv) (Quit: imdoor) |
| 17:15:50 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 17:16:26 | × | nerdypepper quits (znc@152.67.162.71) (Changing host) |
| 17:16:26 | → | nerdypepper joins (znc@user/nerdypepper) |
| 17:17:24 | × | shiraeeshi quits (~shiraeesh@109.166.59.30) (Ping timeout: 265 seconds) |
| 17:17:40 | × | danidiaz quits (~ESDPC@148.3.54.112) (Quit: Leaving.) |
| 17:18:53 | × | werneta quits (~werneta@mobile-166-176-57-108.mycingular.net) (Ping timeout: 264 seconds) |
| 17:18:54 | × | ikex quits (~ash@user/ikex) (Ping timeout: 264 seconds) |
| 17:19:32 | × | bfrk quits (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) (Ping timeout: 268 seconds) |
| 17:20:27 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 17:21:26 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:22:14 | × | AgentM quits (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) (Quit: Leaving.) |
| 17:22:48 | Megant_ | is now known as Megant |
| 17:23:17 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 17:24:40 | <kuribas``> | dminuoso: maybe megaparsec is a better parser for such a case? |
| 17:25:26 | <kuribas``> | "Attoparsec is sometimes faster but not that feature-rich. It should be used when you want to process large amounts of data where performance matters more than quality of error messages." |
| 17:28:06 | → | Guest8311 joins (~Guest83@187.83.249.216.dyn.smithville.net) |
| 17:28:55 | → | wonko joins (~wjc@62.115.229.50) |
| 17:29:13 | → | shiraeeshi joins (~shiraeesh@109.166.59.30) |
| 17:29:57 | → | chomwitt joins (~Pitsikoko@athedsl-20549.home.otenet.gr) |
| 17:31:23 | → | lavaman joins (~lavaman@98.38.249.169) |
| 17:34:00 | <nshepperd> | I don't think I've ever used cassava's fancy record parsing. i always parse a vector of vectors of text then convert |
| 17:34:08 | → | AgentM joins (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) |
| 17:34:52 | <nshepperd> | or Vector (Map Text Text) when i want named columns |
| 17:35:19 | dminuoso | uses the record parsing |
| 17:35:37 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 244 seconds) |
| 17:37:25 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:39:43 | → | pbrisbin joins (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) |
| 17:41:59 | <johnw> | I use megaparsec for all my parsing needs these days; it's quite good |
| 17:42:58 | × | waleee quits (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Ping timeout: 268 seconds) |
| 17:43:18 | <Hecate> | idem |
| 17:43:35 | → | wenzel joins (~wenzel@user/wenzel) |
| 17:44:37 | → | waleee joins (~waleee@h-98-128-228-119.NA.cust.bahnhof.se) |
| 17:44:44 | → | UpstreamSalmon joins (uid12077@id-12077.stonehaven.irccloud.com) |
| 17:45:13 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 17:45:27 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:3866:f955:de69:46b2) |
| 17:45:47 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 17:48:09 | × | shryke quits (~shryke@91.103.43.254) (Ping timeout: 272 seconds) |
| 17:50:06 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:3866:f955:de69:46b2) (Ping timeout: 264 seconds) |
| 17:50:11 | × | neceve quits (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130) (Ping timeout: 252 seconds) |
| 17:50:20 | → | ddellacosta joins (~ddellacos@86.106.143.131) |
| 17:50:27 | → | solomon joins (~solomon@165.227.48.175) |
| 17:51:47 | <kuribas``> | nshepperd: I'll do that then |
| 17:53:15 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 17:56:29 | × | jneira quits (~jneira@166.red-81-39-172.dynamicip.rima-tde.net) (Quit: Connection closed) |
| 17:57:33 | → | vicfred joins (~vicfred@user/vicfred) |
| 18:01:16 | × | kuribas`` quits (~user@ptr-25vy0i7o5gw6tky01tr.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 18:04:33 | × | myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 268 seconds) |
| 18:05:00 | → | amahl joins (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 18:06:02 | → | argento joins (~argent0@168.227.96.53) |
| 18:06:54 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 264 seconds) |
| 18:10:59 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 18:11:03 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 18:12:30 | <johnw> | hmmm.. i'll have to look into the fancy record parsing; I'm using vectors of vectors of text right now, but end up needing to convert most of it anyway |
| 18:12:36 | <johnw> | just found https://hackage.haskell.org/package/tapioca |
| 18:13:01 | → | danidiaz joins (~ESDPC@148.3.54.112) |
| 18:13:51 | × | pbrisbin quits (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) (Ping timeout: 244 seconds) |
| 18:14:28 | → | Shaeto_ joins (~Shaeto@94.25.234.213) |
| 18:15:39 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 268 seconds) |
| 18:16:02 | × | dunkeln quits (~dunkeln@94.129.65.28) (Quit: leaving) |
| 18:16:48 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 18:17:06 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 18:17:27 | × | AgentM quits (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) (Quit: Leaving.) |
| 18:17:29 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:3866:f955:de69:46b2) |
| 18:17:55 | × | Shaeto quits (~Shaeto@94.25.234.55) (Ping timeout: 272 seconds) |
| 18:19:02 | <johnw> | although the latter doesn't seem to be much better than the Generic stuff in cassava itself |
| 18:19:21 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 18:19:30 | → | cheater joins (~Username@user/cheater) |
| 18:19:43 | → | megaTherion joins (~therion@unix.io) |
| 18:19:48 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 18:19:49 | × | dyeplexer quits (~dyeplexer@user/dyeplexer) (Remote host closed the connection) |
| 18:20:42 | × | ixlun quits (~user@109.249.184.235) (Read error: Connection reset by peer) |
| 18:20:55 | → | ixlun joins (~user@109.249.184.235) |
| 18:21:57 | × | bor0 quits (~boro@77.28.64.72) (Quit: This computer has gone to sleep) |
| 18:26:00 | × | ddellacosta quits (~ddellacos@86.106.143.131) (Remote host closed the connection) |
| 18:26:10 | → | ddellacosta joins (~ddellacos@86.106.143.131) |
| 18:27:38 | × | ubikium quits (~ubikium@2400:2200:4f2:4b71:94bf:c634:be62:7c0d) (Read error: Connection reset by peer) |
| 18:27:53 | → | ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) |
| 18:28:43 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 18:30:31 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:30:57 | → | pbrisbin joins (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) |
| 18:31:15 | → | favonia joins (~favonia@user/favonia) |
| 18:33:53 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 18:34:29 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 18:35:17 | → | favonia joins (~favonia@user/favonia) |
| 18:37:21 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 18:37:24 | → | newtoliberachat2 joins (~xyz@1.39.167.172) |
| 18:38:14 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 18:38:15 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 18:39:33 | ← | newtoliberachat2 parts (~xyz@1.39.167.172) () |
| 18:43:21 | × | brandonh quits (~brandonh@151.38.139.116) (Quit: brandonh) |
| 18:45:26 | × | solomon quits (~solomon@165.227.48.175) (Ping timeout: 250 seconds) |
| 18:48:16 | → | Erutuon joins (~Erutuon@71-34-10-193.mpls.qwest.net) |
| 18:54:31 | <maerwald> | johnw: heh, my former work colleague wrote it... it's less boilerplate |
| 18:55:57 | → | favonia joins (~favonia@user/favonia) |
| 18:56:11 | → | Guest81 joins (~Guest81@040-194-158-163.dynamic.caiway.nl) |
| 18:56:29 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 18:56:42 | <Guest81> | Question, are Haskell `Functor`s, "positive" functors? |
| 18:57:03 | <monochrom> | Yes. covariant. |
| 18:57:04 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 18:57:18 | <Guest81> | But not strictly-positive |
| 18:57:40 | <Guest81> | positive and covariant are the same thing? |
| 18:57:45 | <monochrom> | I don't know what that is. |
| 18:58:21 | → | __monty__ joins (~toonn@user/toonn) |
| 18:58:39 | × | pbrisbin quits (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) (Ping timeout: 272 seconds) |
| 18:58:48 | → | favonia joins (~favonia@user/favonia) |
| 18:59:08 | <monochrom> | Since you put "positive" in quotes I take it that you acknowledge you only have a feeling not a rigorous definition so I filled in the closest widely-known rigorous definition which is covariant. |
| 18:59:50 | × | hololeap quits (~hololeap@user/hololeap) (Read error: Connection reset by peer) |
| 19:00:50 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 19:01:34 | → | favonia joins (~favonia@user/favonia) |
| 19:01:37 | × | cheater quits (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 19:01:46 | × | schuelermine quits (~anselmsch@user/schuelermine) (Quit: WeeChat 3.1) |
| 19:01:49 | → | cheater joins (~Username@user/cheater) |
| 19:01:52 | <Guest81> | I see |
| 19:05:38 | → | eggplant_ joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 19:05:45 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 19:06:13 | × | boioioing quits (~boioioing@cpe-76-84-141-127.neb.res.rr.com) (Ping timeout: 268 seconds) |
| 19:06:20 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 19:07:03 | → | favonia joins (~favonia@user/favonia) |
| 19:07:49 | → | chaosite joins (~chaosite@user/chaosite) |
| 19:08:06 | → | zebrag joins (~chris@user/zebrag) |
| 19:09:13 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:3866:f955:de69:46b2) (Ping timeout: 272 seconds) |
| 19:11:10 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:12:47 | → | eightball joins (~eight@86.106.121.164) |
| 19:13:27 | × | favonia quits (~favonia@user/favonia) (Quit: The Lounge - https://thelounge.chat) |
| 19:17:50 | → | favonia joins (~favonia@user/favonia) |
| 19:21:49 | <dmj`> | Guest81: positive just means the type variable is in the codomain (input / arg), negative means its in the domain (output / return type) |
| 19:21:51 | → | sedeki joins (~textual@user/sedeki) |
| 19:21:56 | <dmj`> | :t fmap |
| 19:21:57 | <lambdabot> | Functor f => (a -> b) -> f a -> f b |
| 19:21:58 | <dmj`> | :t contramap |
| 19:21:59 | <lambdabot> | Contravariant f => (a -> b) -> f b -> f a |
| 19:22:24 | <dmj`> | er, I flipped them, positive is output, negative is input |
| 19:22:28 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 19:23:24 | → | favonia joins (~favonia@user/favonia) |
| 19:25:53 | → | boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com) |
| 19:26:34 | × | nerdypepper quits (znc@user/nerdypepper) (Ping timeout: 268 seconds) |
| 19:27:25 | × | rahguzar quits (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Ping timeout: 265 seconds) |
| 19:27:59 | → | nerdypepper joins (znc@152.67.162.71) |
| 19:28:39 | nf | is now known as nii |
| 19:28:54 | × | Guest8311 quits (~Guest83@187.83.249.216.dyn.smithville.net) (Quit: Client closed) |
| 19:29:01 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 19:30:10 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Client Quit) |
| 19:30:52 | nii | is now known as nf |
| 19:31:06 | × | eggplant_ quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 19:31:37 | × | chaosite quits (~chaosite@user/chaosite) (Read error: Connection reset by peer) |
| 19:32:32 | <dmwit> | That's... sort of right. |
| 19:32:34 | × | Jeanne-Kamikaze quits (~Jeanne-Ka@static-198-54-133-134.cust.tzulo.com) (Ping timeout: 264 seconds) |
| 19:32:37 | <dmwit> | And sort of not. |
| 19:32:37 | → | jneira joins (~jneira@166.red-81-39-172.dynamicip.rima-tde.net) |
| 19:33:03 | <dmwit> | I have some writing on positive vs. negative here: https://stackoverflow.com/a/9243982/791604 |
| 19:33:23 | → | schuelermine joins (~schuelerm@user/schuelermine) |
| 19:33:28 | <dmwit> | (There's some other stuff about MonadIO in there that you can ignore.) |
| 19:33:46 | <schuelermine> | hi |
| 19:36:51 | <schuelermine> | one thing that baffles me about Haskell's design is why the syntax sugar for enumFromTo isn't an infix operator |
| 19:37:03 | <schuelermine> | why isn't (..) just an alias for it |
| 19:37:14 | <schuelermine> | Why is it [a..b]? |
| 19:37:17 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 272 seconds) |
| 19:37:35 | → | shapr joins (~user@pool-108-28-144-11.washdc.fios.verizon.net) |
| 19:37:53 | <ski> | how to do `enumFromThenTo', then ? |
| 19:38:08 | <ski> | (and `enumFromThen') |
| 19:38:10 | <schuelermine> | you could even make |
| 19:38:10 | <schuelermine> | (x1, x2) ... xi = enumFromThenTo x1 x2 xi |
| 19:38:28 | <cdsmith> | schuelermine: It sort of fits into a bunch of other sugar around list comprehensions, lists with step, etc. There may be a simpler for that one case, but it would stick out from the rest |
| 19:38:40 | <schuelermine> | true |
| 19:39:16 | ski | idly notes `@undo' doesn't undo enumerations |
| 19:40:12 | → | brandonh joins (~brandonh@151.38.169.228) |
| 19:41:33 | × | danidiaz quits (~ESDPC@148.3.54.112) (Quit: Leaving.) |
| 19:41:34 | <monochrom> | "x .. y" being sometimes enumFromTo and some other times enumFromThenTo, depending on the type of x, is very complicating to implement. |
| 19:42:07 | <schuelermine> | monochrom my suggestion had three dots for enumFromThenTo |
| 19:42:08 | <ski> | i suppose mixfix could possibly do it |
| 19:42:16 | <monochrom> | Fine. |
| 19:42:19 | <monochrom> | "x ... y" being sometimes enumFromTo and some other times enumFromThenTo, depending on the type of x, is very complicating to implement. |
| 19:42:43 | <ski> | heh |
| 19:42:46 | × | cheater quits (~Username@user/cheater) (Ping timeout: 264 seconds) |
| 19:42:52 | <schuelermine> | No, .. vs ... distinguishes them |
| 19:42:59 | <monochrom> | Ah sorry. |
| 19:43:03 | → | cheater joins (~Username@user/cheater) |
| 19:43:25 | <ski> | any corresponding suggestion for `enumFrom' and `enumFromThen' ? |
| 19:43:29 | <schuelermine> | no |
| 19:44:23 | dmj` | reads dmwit's SO post |
| 19:44:42 | <monochrom> | I don't care either way, but my impression is that more people like [x .. y] and [x, x2 .. y] |
| 19:45:10 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 19:45:50 | <monochrom> | As for the real "why", some committee wanted it this way, and they had the final say. |
| 19:46:35 | <c_wraith> | the committee got the Enum instance for Float and Double completely wrong, though. There were two useful things it could have done, they chose neither. |
| 19:47:07 | <monochrom> | In fact my recollection is that they had this exact rule against spending infinite time on syntax hairsplitting: on syntactic matters, the first proposal passes automatically. |
| 19:47:23 | × | Guest81 quits (~Guest81@040-194-158-163.dynamic.caiway.nl) (Quit: Client closed) |
| 19:47:36 | <monochrom> | So yes it is supposed to be arbitary. |
| 19:47:49 | × | sedeki quits (~textual@user/sedeki) (Quit: Textual IRC Client: www.textualapp.com) |
| 19:49:40 | <monochrom> | Where is the Wadler quote about "programmers spend all days picking on syntax and no time thinking about semantics"? |
| 19:50:05 | <monochrom> | Anyway one more data point for that. |
| 19:50:16 | <yushyin> | https://wiki.haskell.org/Wadler%27s_Law ? |
| 19:50:30 | → | chaosite joins (~chaosite@user/chaosite) |
| 19:51:00 | <monochrom> | Yeah that thanks :) |
| 19:52:07 | <monochrom> | I need to bookmark it so next time it is my answer to every syntactic why question. |
| 19:52:20 | <monochrom> | To bad there isn't one for library why question. |
| 19:52:32 | <monochrom> | But really the same nature. |
| 19:52:52 | → | GIANTWORLDKEEPER joins (~pjetcetal@2.95.204.25) |
| 19:53:07 | <yushyin> | you can see that law in actions in various ghc proposal threads :D |
| 19:53:50 | <monochrom> | Very encouraging to those who have high hopes for human nature. |
| 19:54:30 | × | UpstreamSalmon quits (uid12077@id-12077.stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 19:55:16 | → | Jeanne-Kamikaze joins (~Jeanne-Ka@static-198-54-133-102.cust.tzulo.com) |
| 19:55:48 | <Las[m]> | I'm trying to build a project that depends on haskell-src-exts with cabal, and I get this odd error: cabal: The program 'happy' version >=1.19 is required but the version of <path>/bin/happy could not be determined. |
| 19:55:54 | → | mjs2600_ joins (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) |
| 19:55:58 | <Las[m]> | The file is there, and it works fine, I'm not sure why this happens |
| 19:56:12 | <Las[m]> | in the path it says happy-1.20.0 too |
| 19:57:21 | <dmj`> | Las[m]: can you paste your build output, but turn on verbosity (-v) |
| 19:58:35 | <Las[m]> | Thanks, will do, waiting for it to give me the error again |
| 19:59:45 | × | shiraeeshi quits (~shiraeesh@109.166.59.30) (Remote host closed the connection) |
| 19:59:57 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 20:00:38 | × | mjs2600_ quits (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) (Quit: ZNC 1.8.2 - https://znc.in) |
| 20:01:19 | × | wonko quits (~wjc@62.115.229.50) (Ping timeout: 244 seconds) |
| 20:04:48 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 20:05:25 | → | Guest3 joins (~Guest3@187.83.249.216.dyn.smithville.net) |
| 20:05:58 | × | pavonia quits (~user@user/siracusa) (Read error: Connection reset by peer) |
| 20:06:25 | × | Guest3 quits (~Guest3@187.83.249.216.dyn.smithville.net) (Client Quit) |
| 20:12:20 | → | pavonia joins (~user@user/siracusa) |
| 20:17:20 | → | beka joins (~beka@104.193.170-254.PUBLIC.monkeybrains.net) |
| 20:17:43 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 20:19:27 | × | mc47 quits (~yecinem@89.246.239.190) (Read error: Connection reset by peer) |
| 20:20:31 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) |
| 20:20:42 | × | ixlun quits (~user@109.249.184.235) (Read error: Connection reset by peer) |
| 20:20:50 | × | dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.1) |
| 20:21:33 | → | ixlun joins (~user@109.249.184.235) |
| 20:21:50 | × | Dynom quits (~niels@80-114-12-206.cable.dynamic.v4.ziggo.nl) (Quit: WeeChat 3.1) |
| 20:22:41 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 20:25:21 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 20:26:08 | × | ddellacosta quits (~ddellacos@86.106.143.131) (Remote host closed the connection) |
| 20:28:09 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 20:29:31 | × | beka quits (~beka@104.193.170-254.PUBLIC.monkeybrains.net) (Remote host closed the connection) |
| 20:31:03 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 20:31:58 | × | wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 20:32:00 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Client Quit) |
| 20:35:05 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 264 seconds) |
| 20:35:21 | × | chomwitt quits (~Pitsikoko@athedsl-20549.home.otenet.gr) (Ping timeout: 272 seconds) |
| 20:37:35 | → | ixlun` joins (~user@109.249.184.235) |
| 20:38:46 | × | ixlun` quits (~user@109.249.184.235) (Client Quit) |
| 20:39:40 | × | favonia quits (~favonia@user/favonia) (Quit: The Lounge - https://thelounge.chat) |
| 20:40:55 | → | favonia joins (~favonia@user/favonia) |
| 20:41:07 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection) |
| 20:41:14 | × | amahl quits (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Ping timeout: 252 seconds) |
| 20:42:29 | × | brandonh quits (~brandonh@151.38.169.228) (Quit: brandonh) |
| 20:45:22 | → | pe200012 joins (~pe200012@119.131.208.84) |
| 20:45:40 | → | tonyz joins (~tonyz@user/tonyz) |
| 20:45:43 | × | pe200012_ quits (~pe200012@120.236.162.14) (Ping timeout: 265 seconds) |
| 20:46:20 | → | rahguzar joins (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) |
| 20:47:25 | → | brandonh joins (~brandonh@151.38.169.228) |
| 20:47:58 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 20:49:49 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 268 seconds) |
| 20:49:51 | × | favonia quits (~favonia@user/favonia) (Quit: The Lounge - https://thelounge.chat) |
| 20:50:27 | ← | tonyz parts (~tonyz@user/tonyz) () |
| 20:51:01 | × | zeenk quits (~zeenk@2a02:2f04:a310:b600:b098:bf18:df4d:4c41) (Quit: Konversation terminated!) |
| 20:52:07 | → | favonia joins (~favonia@user/favonia) |
| 20:55:58 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 20:57:14 | → | favonia joins (~favonia@user/favonia) |
| 20:57:15 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 20:58:13 | → | ddellacosta joins (~ddellacos@89.45.224.183) |
| 20:58:42 | → | boxscape joins (~boxscape@user/boxscape) |
| 20:59:26 | × | Shaeto_ quits (~Shaeto@94.25.234.213) (Quit: WeeChat 3.1) |
| 20:59:47 | → | Bartosz joins (~textual@24.35.90.211) |
| 21:00:01 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 21:02:41 | × | ddellacosta quits (~ddellacos@89.45.224.183) (Ping timeout: 252 seconds) |
| 21:03:09 | → | favonia joins (~favonia@user/favonia) |
| 21:04:06 | × | dhil quits (~dhil@195.213.192.85) (Quit: Leaving) |
| 21:04:22 | × | brandonh quits (~brandonh@151.38.169.228) (Quit: brandonh) |
| 21:04:39 | × | favonia quits (~favonia@user/favonia) (Client Quit) |
| 21:04:58 | → | brandonh joins (~brandonh@151.38.169.228) |
| 21:06:51 | → | favonia joins (~favonia@user/favonia) |
| 21:09:00 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 21:12:17 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 21:14:05 | × | rahguzar quits (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Ping timeout: 264 seconds) |
| 21:15:26 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 21:16:45 | → | sqrt2 joins (~ben@tunnel330957-pt.tunnel.tserv6.fra1.ipv6.he.net) |
| 21:17:32 | × | argento quits (~argent0@168.227.96.53) (Ping timeout: 252 seconds) |
| 21:19:16 | → | argento joins (~argent0@168.227.96.53) |
| 21:20:01 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 21:21:16 | × | Jeanne-Kamikaze quits (~Jeanne-Ka@static-198-54-133-102.cust.tzulo.com) (Quit: Leaving) |
| 21:22:22 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 21:23:59 | × | prite quits (~pritam@user/pritambaral) (Ping timeout: 244 seconds) |
| 21:25:28 | → | mekeor joins (~user@2001:a61:3a45:d101:3a96:2c15:924e:ebf9) |
| 21:27:31 | → | Guest41 joins (~Guest41@187.83.249.216.dyn.smithville.net) |
| 21:28:42 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 21:30:38 | → | ddellacosta joins (~ddellacos@86.106.121.222) |
| 21:32:42 | × | chisui quits (~chisui@200116b86662dd0045dcdbf42fb73e43.dip.versatel-1u1.de) (Ping timeout: 250 seconds) |
| 21:33:00 | → | lavaman joins (~lavaman@98.38.249.169) |
| 21:35:01 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.2-dev) |
| 21:35:27 | × | ddellacosta quits (~ddellacos@86.106.121.222) (Ping timeout: 268 seconds) |
| 21:36:52 | × | Ariakenom quits (~Ariakenom@2001:9b1:efb:fc00:84c1:f198:927e:8e8c) (Read error: Connection reset by peer) |
| 21:37:25 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 244 seconds) |
| 21:40:22 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 264 seconds) |
| 21:41:28 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) |
| 21:41:46 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 21:44:57 | → | mjs2600 joins (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) |
| 21:46:10 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection) |
| 21:46:17 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) |
| 21:46:41 | × | chaosite quits (~chaosite@user/chaosite) (Ping timeout: 252 seconds) |
| 21:47:38 | → | eddiemundo[m] joins (~jshenmatr@2001:470:69fc:105::a80) |
| 21:49:32 | × | Erutuon quits (~Erutuon@71-34-10-193.mpls.qwest.net) (Changing host) |
| 21:49:32 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 21:49:46 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 21:49:55 | × | Erutuon quits (~Erutuon@user/erutuon) (Quit: WeeChat 2.8) |
| 21:50:05 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 21:51:02 | × | Erutuon quits (~Erutuon@user/erutuon) (Client Quit) |
| 21:51:13 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 21:51:42 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 21:52:27 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:54:17 | → | ddellacosta joins (~ddellacos@86.106.143.66) |
| 21:58:25 | → | chaosite joins (~chaosite@user/chaosite) |
| 21:59:32 | <eddiemundo[m]> | a |
| 21:59:51 | × | o1lo01ol1o quits (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) (Remote host closed the connection) |
| 22:00:36 | → | o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) |
| 22:00:37 | niko | is now known as o |
| 22:01:20 | <ski> | b |
| 22:01:44 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 22:03:03 | × | Guest41 quits (~Guest41@187.83.249.216.dyn.smithville.net) (Quit: Client closed) |
| 22:03:11 | × | ystael quits (~ystael@user/ystael) (Quit: Lost terminal) |
| 22:03:31 | eddiemundo[m] | is now known as eddiemundo |
| 22:03:49 | × | chaosite quits (~chaosite@user/chaosite) (Ping timeout: 268 seconds) |
| 22:05:40 | × | o1lo01ol1o quits (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) (Ping timeout: 268 seconds) |
| 22:09:36 | × | abhixec quits (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net) (Quit: leaving) |
| 22:11:37 | × | L29Ah quits (~L29Ah@user/l29ah) (Remote host closed the connection) |
| 22:12:03 | × | michalz quits (~user@185.246.204.45) (Remote host closed the connection) |
| 22:12:10 | → | hubvu joins (uid495858@id-495858.tinside.irccloud.com) |
| 22:12:27 | → | shiraeeshi joins (~shiraeesh@109.166.59.30) |
| 22:14:06 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 22:14:19 | × | eddiemundo quits (~jshenmatr@2001:470:69fc:105::a80) (Quit: node-irc says goodbye) |
| 22:14:33 | → | eddiemundo joins (~jshenmatr@2001:470:69fc:105::a80) |
| 22:14:39 | <shapr> | c |
| 22:14:44 | × | srk quits (~sorki@user/srk) (Ping timeout: 252 seconds) |
| 22:14:44 | × | eddiemundo quits (~jshenmatr@2001:470:69fc:105::a80) (Client Quit) |
| 22:15:14 | → | eddiemundo joins (~eddiemund@2001:470:69fc:105::a80) |
| 22:15:51 | × | eddiemundo quits (~eddiemund@2001:470:69fc:105::a80) (Client Quit) |
| 22:15:55 | <hpc> | c++ |
| 22:16:07 | → | eddiemundo joins (~eddiemund@2001:470:69fc:105::a80) |
| 22:17:06 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 22:18:21 | × | eddiemundo quits (~eddiemund@2001:470:69fc:105::a80) (Client Quit) |
| 22:18:36 | → | eddiemundo joins (~eddiemund@2001:470:69fc:105::a80) |
| 22:18:48 | × | eddiemundo quits (~eddiemund@2001:470:69fc:105::a80) (Client Quit) |
| 22:19:51 | × | mekeor quits (~user@2001:a61:3a45:d101:3a96:2c15:924e:ebf9) (Ping timeout: 268 seconds) |
| 22:22:24 | × | ddellacosta quits (~ddellacos@86.106.143.66) (Remote host closed the connection) |
| 22:25:43 | × | Natch quits (~natch@c-e070e255.014-297-73746f25.bbcust.telenor.se) (Read error: Connection reset by peer) |
| 22:30:41 | → | srk joins (~sorki@user/srk) |
| 22:34:30 | × | urdh quits (~urdh@h88-129-148-132.cust.a3fiber.se) (Ping timeout: 264 seconds) |
| 22:35:41 | × | Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.) |
| 22:37:50 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:39:58 | × | brandonh quits (~brandonh@151.38.169.228) (Quit: brandonh) |
| 22:40:29 | → | bfrk joins (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) |
| 22:40:45 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection) |
| 22:41:00 | → | urdh joins (~urdh@h88-129-148-132.cust.a3fiber.se) |
| 22:41:06 | × | Deide quits (~Deide@user/deide) (Quit: Seeee yaaaa) |
| 22:41:19 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) |
| 22:43:07 | → | adium joins (adium@user/adium) |
| 22:44:17 | × | Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 22:45:17 | → | o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) |
| 22:45:32 | × | acertain quits (sid470584@stonehaven.irccloud.com) (Ping timeout: 252 seconds) |
| 22:45:46 | × | amir quits (sid22336@user/amir) (Ping timeout: 264 seconds) |
| 22:45:46 | × | zot quits (sid449795@stonehaven.irccloud.com) (Ping timeout: 264 seconds) |
| 22:45:49 | × | zopsi quits (sid153252@id-153252.stonehaven.irccloud.com) (Ping timeout: 272 seconds) |
| 22:45:56 | × | hydroxonium quits (uid500654@id-500654.stonehaven.irccloud.com) (Read error: Connection reset by peer) |
| 22:45:56 | × | dmj` quits (sid72307@id-72307.stonehaven.irccloud.com) (Read error: Connection reset by peer) |
| 22:46:01 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Ping timeout: 272 seconds) |
| 22:46:01 | × | hamishmack quits (sid389057@id-389057.stonehaven.irccloud.com) (Ping timeout: 272 seconds) |
| 22:46:04 | × | mthvedt quits (uid501949@id-501949.stonehaven.irccloud.com) (Read error: Connection reset by peer) |
| 22:46:04 | × | astra quits (sid289983@user/astrazeneca) (Read error: Connection reset by peer) |
| 22:46:05 | × | rubin55 quits (sid175221@id-175221.stonehaven.irccloud.com) (Read error: Connection reset by peer) |
| 22:46:06 | × | peteretep quits (sid143467@id-143467.stonehaven.irccloud.com) (Read error: Connection reset by peer) |
| 22:46:08 | × | jakesyl quits (sid56879@id-56879.stonehaven.irccloud.com) (Read error: Connection reset by peer) |
| 22:46:08 | × | hnOsmium0001 quits (uid453710@id-453710.stonehaven.irccloud.com) (Read error: Connection reset by peer) |
| 22:46:10 | × | Firedancer quits (sid336191@id-336191.stonehaven.irccloud.com) (Read error: Connection reset by peer) |
| 22:46:32 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:47:05 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 264 seconds) |
| 22:47:11 | × | ehamberg quits (sid18208@stonehaven.irccloud.com) (Ping timeout: 252 seconds) |
| 22:47:11 | × | joel135 quits (sid136450@stonehaven.irccloud.com) (Ping timeout: 252 seconds) |
| 22:47:11 | × | jneira quits (~jneira@166.red-81-39-172.dynamicip.rima-tde.net) (Quit: Connection closed) |
| 22:47:44 | × | leif quits (uid501722@id-501722.stonehaven.irccloud.com) (Ping timeout: 252 seconds) |
| 22:47:55 | × | SanchayanMaity quits (sid478177@id-478177.stonehaven.irccloud.com) (Ping timeout: 272 seconds) |
| 22:49:10 | × | urdh quits (~urdh@h88-129-148-132.cust.a3fiber.se) (Quit: Boom!) |
| 22:49:58 | → | urdh joins (~urdh@h88-129-148-132.cust.a3fiber.se) |
| 22:50:05 | × | o1lo01ol1o quits (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) (Ping timeout: 264 seconds) |
| 22:51:28 | → | zot joins (sid449795@id-449795.stonehaven.irccloud.com) |
| 22:51:33 | → | ehamberg joins (sid18208@id-18208.stonehaven.irccloud.com) |
| 22:51:34 | → | dmj` joins (sid72307@id-72307.stonehaven.irccloud.com) |
| 22:51:37 | → | hydroxonium joins (uid500654@id-500654.stonehaven.irccloud.com) |
| 22:51:43 | → | peteretep joins (sid143467@id-143467.stonehaven.irccloud.com) |
| 22:51:43 | → | acertain joins (sid470584@id-470584.stonehaven.irccloud.com) |
| 22:51:44 | → | amir joins (sid22336@user/amir) |
| 22:51:45 | → | hamishmack joins (sid389057@id-389057.stonehaven.irccloud.com) |
| 22:51:46 | → | mthvedt joins (uid501949@id-501949.stonehaven.irccloud.com) |
| 22:51:46 | → | zopsi joins (sid153252@id-153252.stonehaven.irccloud.com) |
| 22:51:53 | → | rubin55 joins (sid175221@id-175221.stonehaven.irccloud.com) |
| 22:52:02 | → | astra_ joins (sid289983@id-289983.stonehaven.irccloud.com) |
| 22:52:03 | → | Firedancer joins (sid336191@id-336191.stonehaven.irccloud.com) |
| 22:52:03 | → | jakesyl joins (sid56879@id-56879.stonehaven.irccloud.com) |
| 22:52:05 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 22:52:22 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 264 seconds) |
| 22:52:30 | → | SanchayanMaity joins (sid478177@id-478177.stonehaven.irccloud.com) |
| 22:52:40 | → | joel135 joins (sid136450@id-136450.stonehaven.irccloud.com) |
| 22:52:50 | → | leif joins (uid501722@id-501722.stonehaven.irccloud.com) |
| 22:53:20 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 22:54:42 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 22:55:16 | → | ddellacosta joins (~ddellacos@89.45.224.222) |
| 22:56:50 | × | aplainzetakind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Quit: Free ZNC ~ Powered by LunarBNC: https://LunarBNC.net) |
| 22:57:55 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Client Quit) |
| 22:58:06 | astra_ | is now known as amish |
| 23:00:02 | × | amish quits (sid289983@id-289983.stonehaven.irccloud.com) () |
| 23:00:10 | × | ddellacosta quits (~ddellacos@89.45.224.222) (Ping timeout: 264 seconds) |
| 23:00:17 | → | amish joins (sid289983@id-289983.stonehaven.irccloud.com) |
| 23:02:02 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 23:02:18 | × | amish quits (sid289983@id-289983.stonehaven.irccloud.com) (Changing host) |
| 23:02:18 | → | amish joins (sid289983@user/amish) |
| 23:02:55 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 23:03:02 | → | o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) |
| 23:03:24 | amish | is now known as astra |
| 23:03:29 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) |
| 23:03:49 | → | pe200012_ joins (~pe200012@119.131.208.84) |
| 23:03:57 | × | pe200012 quits (~pe200012@119.131.208.84) (Ping timeout: 265 seconds) |
| 23:04:56 | → | abhixec joins (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net) |
| 23:04:57 | × | urdh quits (~urdh@h88-129-148-132.cust.a3fiber.se) (Quit: Boom!) |
| 23:06:16 | → | urdh joins (~urdh@h88-129-148-132.cust.a3fiber.se) |
| 23:07:32 | × | o1lo01ol1o quits (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) (Ping timeout: 252 seconds) |
| 23:09:22 | → | L29Ah joins (~L29Ah@user/l29ah) |
| 23:11:03 | → | aplainzetakind joins (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 23:15:42 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 23:22:22 | → | bfrk1 joins (~Thunderbi@200116b84593d400e083e41adfb91d63.dip.versatel-1u1.de) |
| 23:24:22 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 23:24:39 | × | bfrk quits (~Thunderbi@200116b84534a60005aeadf137ee420f.dip.versatel-1u1.de) (Ping timeout: 272 seconds) |
| 23:24:39 | bfrk1 | is now known as bfrk |
| 23:27:04 | × | dpl_ quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 268 seconds) |
| 23:27:28 | × | shapr quits (~user@pool-108-28-144-11.washdc.fios.verizon.net) (Ping timeout: 244 seconds) |
| 23:29:50 | → | ddellacosta joins (~ddellacos@86.106.143.222) |
| 23:33:56 | × | alex3 quits (~Chel@BSN-77-82-41.static.siol.net) (Ping timeout: 252 seconds) |
| 23:34:53 | × | ddellacosta quits (~ddellacos@86.106.143.222) (Ping timeout: 265 seconds) |
| 23:35:36 | × | Scotty_Trees quits (~Scotty_Tr@162-234-179-169.lightspeed.brhmal.sbcglobal.net) (Quit: Leaving) |
| 23:37:38 | → | eldritch_ joins (~eldritch@134.209.221.71) |
| 23:37:59 | → | notzmv joins (~zmv@user/notzmv) |
| 23:39:47 | → | alex3 joins (~Chel@BSN-77-82-41.static.siol.net) |
| 23:43:01 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 272 seconds) |
| 23:46:45 | → | mustafa joins (~mustafa@rockylinux/releng/mstg) |
| 23:47:21 | → | willbush joins (~user@47.183.200.14) |
| 23:49:29 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 264 seconds) |
| 23:53:13 | → | Scotty_Trees joins (~Scotty_Tr@162-234-179-169.lightspeed.brhmal.sbcglobal.net) |
| 23:56:42 | × | cheater quits (~Username@user/cheater) (Ping timeout: 264 seconds) |
| 23:56:58 | → | cheater joins (~Username@user/cheater) |
All times are in UTC on 2021-05-31.