Logs on 2022-08-04 (liberachat/#haskell)
| 00:02:46 | × | EsoAlgo quits (~EsoAlgo@129.146.136.145) (Ping timeout: 268 seconds) |
| 00:07:50 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 00:08:29 | → | mvk joins (~mvk@2607:fea8:5ce3:8500::d5f2) |
| 00:08:39 | → | yaroot_ joins (~yaroot@p3374048-ipngn8502souka.saitama.ocn.ne.jp) |
| 00:10:54 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 00:11:25 | × | yaroot quits (~yaroot@2400:4052:ac0:d900:680e:dbff:fe1e:4953) (Ping timeout: 244 seconds) |
| 00:11:25 | yaroot_ | is now known as yaroot |
| 00:15:20 | → | fserucas_ joins (~fserucas@83.223.235.72) |
| 00:17:32 | × | fserucas quits (~fserucas@83.223.235.72) (Ping timeout: 245 seconds) |
| 00:18:15 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 00:20:57 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 00:22:20 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 00:22:24 | → | jargon joins (~jargon@184.101.188.251) |
| 00:22:46 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 00:26:14 | × | burnsidesLlama quits (~burnsides@119247164140.ctinets.com) (Remote host closed the connection) |
| 00:26:27 | → | burnsidesLlama joins (~burnsides@119247164140.ctinets.com) |
| 00:26:41 | → | talismanick joins (~talismani@2601:200:c100:3850::dd64) |
| 00:27:38 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 00:27:38 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 00:27:38 | → | wroathe joins (~wroathe@user/wroathe) |
| 00:30:01 | × | burnsidesLlama quits (~burnsides@119247164140.ctinets.com) (Remote host closed the connection) |
| 00:30:53 | → | burnsidesLlama joins (~burnsides@119247164140.ctinets.com) |
| 00:30:55 | × | talismanick quits (~talismani@2601:200:c100:3850::dd64) (Remote host closed the connection) |
| 00:31:11 | → | talismanick joins (~talismani@2601:200:c100:3850::dd64) |
| 00:32:08 | × | burnsidesLlama quits (~burnsides@119247164140.ctinets.com) (Remote host closed the connection) |
| 00:32:20 | → | burnsidesLlama joins (~burnsides@119247164140.ctinets.com) |
| 00:40:25 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 00:42:07 | × | sandy_doo quits (~sandydoo@185.209.196.136) (Ping timeout: 245 seconds) |
| 00:43:00 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 00:45:28 | × | merijn quits (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 268 seconds) |
| 00:51:24 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 00:52:00 | → | Guest15 joins (~Guest15@2601:643:897f:5f73:798:18eb:66c5:dd30) |
| 00:53:25 | × | burnsidesLlama quits (~burnsides@119247164140.ctinets.com) (Remote host closed the connection) |
| 00:54:18 | → | burnsidesLlama joins (~burnsides@119247164140.ctinets.com) |
| 00:57:50 | × | xff0x quits (~xff0x@2405:6580:b080:900:40d:d87e:58e3:1ef6) (Ping timeout: 240 seconds) |
| 01:02:22 | → | frost joins (~frost@user/frost) |
| 01:03:44 | × | Guest15 quits (~Guest15@2601:643:897f:5f73:798:18eb:66c5:dd30) (Quit: Client closed) |
| 01:10:57 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:11:14 | × | Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 01:17:06 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:29:52 | × | vglfr quits (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 01:30:18 | × | burnsidesLlama quits (~burnsides@119247164140.ctinets.com) () |
| 01:30:23 | <albet70> | @free reverse :: [a] -> [a] |
| 01:30:23 | <lambdabot> | $map f . reverse = reverse . $map f |
| 01:30:44 | <albet70> | how lambdabot implement this 'free'? |
| 01:30:54 | → | vglfr joins (~vglfr@194.9.14.33) |
| 01:31:12 | <Axman6> | its source code is https://github.com/lambdabot/lambdabot |
| 01:31:39 | <Axman6> | https://github.com/lambdabot/lambdabot/tree/master/lambdabot-haskell-plugins/src/Lambdabot/Plugin/Haskell/Free |
| 01:32:22 | <Axman6> | @free f :: (((a -> b) -> c) -> d) -> d |
| 01:32:22 | <lambdabot> | (forall f2 f3. (forall f4 f5. h . f4 = f5 . g => k (f2 f4) = f3 f5) => p (q f2) = f1 f3) => p (f q) = f |
| 01:32:22 | <lambdabot> | f1 |
| 01:33:29 | <Axman6> | but I would guess the theorems for free paper would be more useful |
| 01:35:24 | <qrpnxz1> | messing with with unboxed values pretty yucky in haskell :(( |
| 01:35:37 | <Axman6> | what makes you say that? |
| 01:36:32 | <EvanR> | unboxed literals can be a bit weird |
| 01:36:49 | <EvanR> | general values are guaranteed to behave thanks to the kind system |
| 01:36:56 | <qrpnxz1> | error messages when you don't have MagicHash and UnboxedTuples enabled are pretty bad. If i didn't know about the extensions before hand, and probably be out of luck. I have to pull in all these special GHC modules because they are basically second-class "implementation details" Math is just a mess |
| 01:37:02 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 01:37:37 | <qrpnxz1> | i can get by, but it's just not nice |
| 01:40:20 | → | mrmr1 joins (~mrmr@user/mrmr) |
| 01:42:07 | × | mrmr quits (~mrmr@user/mrmr) (Ping timeout: 245 seconds) |
| 01:42:08 | mrmr1 | is now known as mrmr |
| 01:43:38 | geekosaur | is pretty sure it's not supposed to be nice |
| 01:47:05 | <qrpnxz1> | it's disappointing but understandable |
| 01:47:07 | × | vglfr quits (~vglfr@194.9.14.33) (Ping timeout: 245 seconds) |
| 01:47:13 | qrpnxz1 | is now known as qrpnxz |
| 01:47:57 | <Axman6> | they literally are implementation details, after all |
| 01:48:17 | → | vglfr joins (~vglfr@194.9.14.33) |
| 01:49:32 | <qrpnxz> | they shouldn't be though. Unboxed are important enough to get the same amount of attention as anything in the report. |
| 01:50:12 | <qrpnxz> | well let me check first that they aren't in the report actually |
| 01:50:43 | <qrpnxz> | looks like no |
| 01:50:47 | <geekosaur> | they're not. and other haskell impls don't have them |
| 01:50:52 | <EvanR> | the issue is with some syntax for unboxed literals |
| 01:51:14 | <EvanR> | the kind of stuff we usually can't complain about because it's syntax and so bikeshedding xD |
| 01:51:54 | <EvanR> | the issue about not knowing about extensions is kind of not an issue though |
| 01:52:13 | <geekosaur> | they're specific to ghc. and I'd argue that if you need to care and aren't a ghc dev, you've made a wrong life choice somewhere. (rust?) |
| 01:52:14 | <qrpnxz> | Syntax can be pretty important. I dont' mind the # thing actually, it's just the terrible messages when you do go to use it |
| 01:52:41 | × | vglfr quits (~vglfr@194.9.14.33) (Ping timeout: 268 seconds) |
| 01:52:49 | <geekosaur> | what's it to do? per the report # is a perfectly valid operator name, and i8n fact in use on hackage |
| 01:52:50 | → | vglfr joins (~vglfr@194.9.14.33) |
| 01:53:14 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 268 seconds) |
| 01:53:14 | <qrpnxz> | yeah, (#) is used in lens for example for reviewing |
| 01:53:23 | <qrpnxz> | idk that that actually clashes with magichash |
| 01:54:47 | <EvanR> | as long as space around operators is required it's easy |
| 01:54:56 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 01:54:56 | <qrpnxz> | on a related note, not being able to mix symbols with letters in names in general is also a big sad |
| 01:55:05 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 01:55:12 | <EvanR> | space around operators is not required though xD |
| 01:55:19 | <EvanR> | making mixed names impossible |
| 01:55:50 | <qrpnxz> | not so, there would just be a different interpretation based on if you had the space or not. |
| 01:55:51 | <geekosaur> | I think that changed with OverloadedRecordDot |
| 01:56:20 | <EvanR> | oh jeez... we are lost then |
| 01:56:36 | → | instantaphex joins (~jb@c-73-171-252-84.hsd1.fl.comcast.net) |
| 01:57:29 | <qrpnxz> | i would love for example if functions that return Maybe could by convention end in ?. I'd celebrate that with a few drinks |
| 01:57:31 | <geekosaur> | (actually the spaces around operators thing has been coming since BangPatterns, but only got rationalized with OverloadedRecordDot) |
| 01:57:56 | <EvanR> | what if they return Maybe (Maybe Something), two question marks? xD |
| 01:58:32 | <qrpnxz> | mmm, i'd say one mark :) but interesting case |
| 01:58:48 | <geekosaur> | BangPatterns, TypeApplications, NegativeLiterals and friends, etc. all had special spacing rules that got combined together with OverloadedRecordDot |
| 01:58:54 | <EvanR> | code in the maybe monad would probably get pretty noisy |
| 01:59:11 | <qrpnxz> | isn't it the opposite of noise because i don't have to case match |
| 01:59:23 | <EvanR> | there would just be a lot of ? |
| 01:59:45 | <qrpnxz> | there's a lot of 'e' and 'a' too, pesky common letters |
| 02:00:04 | <EvanR> | well, letters and punctuation marks aren't on equal footing |
| 02:00:25 | → | nate4 joins (~nate@98.45.169.16) |
| 02:00:28 | <EvanR> | letters blend together to form words and entire sentences we can see at once, while strings of punctuation marks are just that |
| 02:00:36 | <qrpnxz> | wecouldalsotypelikethis,butthespacesareworthit |
| 02:00:57 | <EvanR> | perl exists |
| 02:01:06 | × | zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 02:01:28 | <qrpnxz> | idk enough about perl to have anything to reply to that :) |
| 02:01:41 | × | hippoid quits (~hippoid@c-98-220-13-8.hsd1.il.comcast.net) (Ping timeout: 255 seconds) |
| 02:01:44 | <EvanR> | if you like code containing a lot of punctuation |
| 02:02:12 | <qrpnxz> | oh yeah, the variable names in perl indicate type i think? or interpretation rather (?) |
| 02:02:40 | <EvanR> | no that's bad C++ |
| 02:02:40 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 02:03:16 | <qrpnxz> | then i could also do things like do { a? <- fallible; case a? of { Just a -> ... |
| 02:04:52 | <geekosaur> | isn't that swift? |
| 02:05:03 | → | zaquest joins (~notzaques@5.130.79.72) |
| 02:05:07 | <qrpnxz> | i think ? is an operator in swift |
| 02:05:27 | <qrpnxz> | that does early return on optionals |
| 02:05:53 | <geekosaur> | mm, I think there's a language that has that trailing ? (mis?)feature. ruby? |
| 02:06:07 | <qrpnxz> | early return for Maybe comes free with laziness, but only if you re associate all your binds correctly |
| 02:06:14 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 240 seconds) |
| 02:06:21 | <qrpnxz> | geekosaur: as an operator or convention? |
| 02:06:32 | <geekosaur> | convention |
| 02:06:32 | <qrpnxz> | scheme has it as convention for predicates |
| 02:06:39 | <qrpnxz> | which is also nice |
| 02:06:41 | <geekosaur> | allowed at the end of names |
| 02:06:54 | <qrpnxz> | even? |
| 02:06:56 | <qrpnxz> | odd? |
| 02:06:58 | <qrpnxz> | that's just nice |
| 02:07:07 | <geekosaur> | in any case I should have gone to bed half an hour ago |
| 02:07:21 | <qrpnxz> | 👋 |
| 02:07:24 | <geekosaur> | (guess that's better than lisp's "p" suffix for predicates) |
| 02:08:28 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 02:12:56 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 02:20:53 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 02:20:53 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:20:53 | finn_elija | is now known as FinnElija |
| 02:25:34 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 02:27:18 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 02:28:04 | → | Guest|26 joins (~Guest|26@S0106020fb5669598.ed.shawcable.net) |
| 02:28:25 | × | Guest|26 quits (~Guest|26@S0106020fb5669598.ed.shawcable.net) (Client Quit) |
| 02:28:54 | <monochrom> | Oh, so "lisp" is a predicate... :) |
| 02:29:11 | <qrpnxz> | xd |
| 02:29:25 | monochrom | writes in CV: I know lisp, scheme?, and isJava. |
| 02:29:34 | <qrpnxz> | haha |
| 02:34:35 | <instantaphex> | Is there a way to free form type over multiple lines in ghci? I know I can use :{ :} to enter multiple lines, but I find that typos are getting me down and I can't go back and fix them. |
| 02:35:33 | <Axman6> | use a file |
| 02:35:53 | <instantaphex> | You got me there |
| 02:36:45 | × | merijn quits (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 02:37:02 | <monochrom> | ghci is not an IDE |
| 02:37:50 | <monochrom> | I don't understand the obsession with hand-typing lengthy code at the REPL. |
| 02:38:20 | <monochrom> | Some people cite Python but Python's REPL isn't a better editor than ghci either. |
| 02:39:04 | <instantaphex> | I don't hand type lengthy code per se, but it would be nice to have sort of a scratch pad type repl type thing at times |
| 02:39:12 | × | td_ quits (~td@94.134.91.79) (Ping timeout: 245 seconds) |
| 02:39:28 | <Axman6> | almost like... a file... in an editor... :P |
| 02:39:29 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 02:39:30 | <instantaphex> | Or a vim plugin that would let me highlight a block of code and run it |
| 02:39:51 | <monochrom> | My recollection is that only Smalltalk came half-close to that dream, and no one alive has seen Smalltalk by now. |
| 02:40:19 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 02:40:28 | <instantaphex> | I briefly looked at a smalltalk tutorial at one point out of curiosity. I noped out pretty fast |
| 02:41:11 | <monochrom> | In this case I mean Smalltalk's IDE. |
| 02:41:18 | → | td_ joins (~td@94.134.91.223) |
| 02:41:56 | <instantaphex> | I feel like the Clojure community is super into repling hard core. I guess not so much for haskell devs |
| 02:42:39 | <monochrom> | Ah I forgot Clojure. Yeah it gets pretty close. |
| 02:42:56 | <instantaphex> | I've seen them use terms like REPL driven development |
| 02:43:08 | <instantaphex> | Never tried Clojure so I have no idea |
| 02:45:09 | × | zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 02:45:12 | <monochrom> | Clojure is an extremely dynamic language. Hot-fixing code at the REPL is an option. |
| 02:45:34 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Ping timeout: 268 seconds) |
| 02:46:10 | <monochrom> | (In principle you could do that to Scheme too, but it's the Clojure people who are serious about it.) |
| 02:47:21 | × | bitdex_ quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 02:47:44 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:03:53 | × | nate4 quits (~nate@98.45.169.16) (Ping timeout: 252 seconds) |
| 03:10:11 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 03:10:33 | × | jero98772 quits (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) (Remote host closed the connection) |
| 03:11:11 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:16:22 | → | Guest55 joins (~Guest55@c-71-198-235-211.hsd1.ca.comcast.net) |
| 03:18:23 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 03:21:54 | <sm> | I'm alive! Smalltalk is awesome and still here |
| 03:23:20 | → | frost30 joins (~frost@user/frost) |
| 03:23:29 | × | frost quits (~frost@user/frost) (Quit: Client closed) |
| 03:23:34 | × | frost30 quits (~frost@user/frost) (Client Quit) |
| 03:28:14 | × | Vajb quits (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) (Read error: Connection reset by peer) |
| 03:28:22 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) |
| 03:28:47 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 03:35:23 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 03:36:19 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 03:38:06 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) |
| 03:38:23 | × | tinwood_ quits (~tinwood@general.default.akavanagh.uk0.bigv.io) (Quit: No Ping reply in 180 seconds.) |
| 03:39:49 | → | tinwood joins (~tinwood@general.default.akavanagh.uk0.bigv.io) |
| 03:39:49 | × | tinwood quits (~tinwood@general.default.akavanagh.uk0.bigv.io) (Changing host) |
| 03:39:49 | → | tinwood joins (~tinwood@canonical/tinwood) |
| 03:44:38 | × | rekahsoft quits (~rekahsoft@bras-base-wdston4533w-grc-02-142-113-160-8.dsl.bell.ca) (Ping timeout: 240 seconds) |
| 03:45:39 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 03:45:48 | → | Vajb joins (~Vajb@2001:999:70c:2b99:3e15:6929:5bc6:c014) |
| 03:47:15 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 03:51:30 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 03:52:34 | × | vglfr quits (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 03:53:22 | → | vglfr joins (~vglfr@194.9.14.33) |
| 03:58:29 | → | mbuf joins (~Shakthi@122.165.55.71) |
| 04:03:14 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 04:03:39 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 252 seconds) |
| 04:06:15 | × | causal quits (~user@50.35.83.177) (Quit: WeeChat 3.6) |
| 04:10:53 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) () |
| 04:11:50 | × | instantaphex quits (~jb@c-73-171-252-84.hsd1.fl.comcast.net) (Ping timeout: 240 seconds) |
| 04:22:04 | <EvanR> | clojure repl was cool when I tried it, until you veer into the java |
| 04:23:11 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 04:26:51 | × | vglfr quits (~vglfr@194.9.14.33) (Ping timeout: 268 seconds) |
| 04:28:51 | → | vglfr joins (~vglfr@194.9.14.33) |
| 04:31:22 | × | vglfr quits (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 04:32:06 | → | vglfr joins (~vglfr@194.9.14.33) |
| 04:37:02 | × | merijn quits (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 04:39:33 | × | vglfr quits (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 04:40:52 | → | vglfr joins (~vglfr@194.9.14.33) |
| 04:43:22 | × | vglfr quits (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 04:43:50 | <Clinton[m]> | `GHC.Generic` has this function `to :: Rep a x -> a`. I'm trying to write a function that goes from `MyUntypedData -> Maybe (Rep a x)`. I can then just use `to` to create the actual type. |
| 04:43:51 | <Clinton[m]> | But what is `x` here? I need to make it something because `Rep a` has type `Type -> Type` and hence can't be a return value of a function. But what should I make it? Or will anything do here (could I just make it `()` for example?) |
| 04:54:29 | → | instantaphex joins (~jb@c-73-171-252-84.hsd1.fl.comcast.net) |
| 04:58:26 | → | titibandit joins (~titibandi@xdsl-78-35-214-18.nc.de) |
| 04:58:38 | × | instantaphex quits (~jb@c-73-171-252-84.hsd1.fl.comcast.net) (Ping timeout: 240 seconds) |
| 05:00:55 | → | nate4 joins (~nate@98.45.169.16) |
| 05:05:02 | × | nate4 quits (~nate@98.45.169.16) (Ping timeout: 240 seconds) |
| 05:10:27 | → | vglfr joins (~vglfr@194.9.14.33) |
| 05:10:38 | × | machinedgod quits (~machinedg@d172-219-86-154.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 05:13:28 | → | ghn joins (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 05:13:39 | × | leeks quits (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 05:15:50 | × | ghn quits (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Client Quit) |
| 05:17:17 | → | ghn joins (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 05:17:55 | → | gmg joins (~user@user/gehmehgeh) |
| 05:21:29 | <glguy> | Clinton[m]: the way to make a Rep a x is with from :: Generic a => a -> Rep a x |
| 05:22:03 | <glguy> | the extra type parameter you're asking about only exists to support Generic1 |
| 05:22:12 | <glguy> | you can just set it to whatever |
| 05:22:35 | <glguy> | but it doesn't sound like the usecase you described makes much sense |
| 05:23:28 | <Clinton[m]> | glguy: I think I've worked out that I can just leave the `x` open, I can still make a concrete value that represents it without restricting `x` so it doesn't matter |
| 05:24:03 | → | euandreh joins (~euandreh@179.214.113.107) |
| 05:24:57 | <glguy> | right, it doesn't matter what you put there |
| 05:26:17 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 05:31:25 | → | instantaphex joins (~jb@c-73-171-252-84.hsd1.fl.comcast.net) |
| 05:33:54 | → | razetime joins (~quassel@43.254.111.18) |
| 05:35:41 | × | instantaphex quits (~jb@c-73-171-252-84.hsd1.fl.comcast.net) (Ping timeout: 252 seconds) |
| 05:39:51 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 05:44:26 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 05:47:08 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 05:51:52 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 05:57:23 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 05:57:48 | → | coot joins (~coot@213.134.190.95) |
| 06:00:54 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 06:10:12 | <albet70> | @djinn join :: ((((a->r)->r)->r)->r)-> ((a->r)->r) |
| 06:10:12 | <lambdabot> | Cannot parse command |
| 06:10:35 | <albet70> | @djinn ((((a->r)->r)->r)->r)-> ((a->r)->r) |
| 06:10:35 | <lambdabot> | f a b = a (\ c -> c b) |
| 06:13:33 | <albet70> | f a b = a (\ c -> c b), is this f join when m is Cont? |
| 06:14:44 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 06:15:19 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 06:16:34 | × | razetime quits (~quassel@43.254.111.18) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 06:19:39 | → | misterfish joins (~misterfis@ip214-130-173-82.adsl2.static.versatel.nl) |
| 06:20:01 | × | PiDelport quits (uid25146@id-25146.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 06:22:01 | <Axman6> | @unmtl Cont r a |
| 06:22:01 | <lambdabot> | (a -> r) -> r |
| 06:22:25 | <Axman6> | @unmtl ContT r (Cont r) a |
| 06:22:25 | <lambdabot> | (a -> (r -> r) -> r) -> (r -> r) -> r |
| 06:22:36 | <Axman6> | not sure if that's relevant |
| 06:23:09 | × | ghn quits (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Quit: ghn) |
| 06:23:13 | → | instantaphex joins (~jb@c-73-171-252-84.hsd1.fl.comcast.net) |
| 06:23:28 | → | ghn joins (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 06:23:52 | <albet70> | @unmtl Cont r (Cont r) |
| 06:23:52 | <lambdabot> | err: `Cont r' is not applied to enough arguments, giving `/\A. (A -> r) -> r' |
| 06:25:44 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 06:26:13 | <albet70> | join :: Cont r (Cont r a) -> Cont r a, this is wrong? |
| 06:28:52 | × | coot quits (~coot@213.134.190.95) (Quit: coot) |
| 06:28:57 | × | instantaphex quits (~jb@c-73-171-252-84.hsd1.fl.comcast.net) (Ping timeout: 268 seconds) |
| 06:32:53 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
| 06:33:31 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 06:34:42 | → | fef joins (~thedawn@user/thedawn) |
| 06:35:05 | × | merijn quits (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 06:35:10 | <albet70> | @djinn (a->)->((a->r)->r)->(b->r)->r |
| 06:35:10 | <lambdabot> | Cannot parse command |
| 06:35:26 | <albet70> | @djinn (a->r)->((a->r)->r)->(b->r)->r |
| 06:35:26 | <lambdabot> | f a b _ = b a |
| 06:41:02 | × | jargon quits (~jargon@184.101.188.251) (Remote host closed the connection) |
| 06:41:38 | → | chele joins (~chele@user/chele) |
| 06:41:44 | × | ghn quits (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Quit: ghn) |
| 06:42:02 | → | ghn joins (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 06:42:59 | × | titibandit quits (~titibandi@xdsl-78-35-214-18.nc.de) (Remote host closed the connection) |
| 06:43:25 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:5f26:adbf:e619:7a29) |
| 06:44:03 | → | Pickchea joins (~private@user/pickchea) |
| 06:44:22 | × | vglfr quits (~vglfr@194.9.14.33) (Ping timeout: 268 seconds) |
| 06:44:30 | → | vglfr joins (~vglfr@194.9.14.33) |
| 06:50:05 | → | acidjnk joins (~acidjnk@p200300d6e7058699cc6cce398877ca6f.dip0.t-ipconnect.de) |
| 06:55:56 | × | misterfish quits (~misterfis@ip214-130-173-82.adsl2.static.versatel.nl) (Ping timeout: 268 seconds) |
| 06:57:16 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:57:19 | <ski> | albet70 : yes, that's `join' |
| 06:57:41 | <ski> | (eta-reduced, even) |
| 06:58:02 | → | yvan-sraka joins (~yvan-srak@209.red-2-139-126.dynamicip.rima-tde.net) |
| 07:00:20 | → | ubert joins (~Thunderbi@77.119.221.71.wireless.dyn.drei.com) |
| 07:00:56 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 07:07:27 | → | irfan joins (~irfan@user/irfan) |
| 07:08:21 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 07:09:56 | <irfan> | hello, is there a way to use `TypeApplications` to replace type annotations for values like `x :: C a => a`? |
| 07:10:31 | <ski> | do you mean `x :: forall a. C a => a' ? |
| 07:11:13 | <irfan> | ski: yeah |
| 07:11:55 | <ski> | then you should be able to use `x @T', for whatever `T' you want to use in place of `a', rather than using a type ascription like `x :: T' |
| 07:12:53 | <irfan> | ski: but expressions like `2 @Int` don't seem to work, at least in GHCi? |
| 07:12:57 | × | vglfr quits (~vglfr@194.9.14.33) (Ping timeout: 245 seconds) |
| 07:13:14 | × | ghn quits (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Quit: ghn) |
| 07:13:33 | → | ghn joins (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 07:13:38 | <[exa]> | irfan: try `fromInteger @Int 2` |
| 07:14:07 | <[exa]> | (2 is not a function, but a syntactic sugar) |
| 07:15:02 | <irfan> | [exa]: ah, so `TypeApplications` is only meant for being used by functions, correct? |
| 07:15:11 | <ski> | (that `x' was also not a function) |
| 07:15:17 | <ski> | irfan : no |
| 07:15:25 | <irfan> | ski: no. |
| 07:16:04 | <irfan> | ski: Cannot apply expression of type ‘t1’ |
| 07:16:09 | <[exa]> | irfan: you can apply types to whatever accepts the type arguments, no problem with that |
| 07:16:26 | <ski> | % maxBound @Int |
| 07:16:26 | <yahb2> | 9223372036854775807 |
| 07:16:35 | <ski> | @type maxBound |
| 07:16:36 | <lambdabot> | Bounded a => a |
| 07:16:43 | <ski> | `maxBound' is not a function |
| 07:16:53 | <[exa]> | just that `2 @Int` desugars to `(fromInteger (Magical2Integer)) @Int`, which is not really what we wanted |
| 07:17:05 | <[exa]> | irfan: ^ |
| 07:17:45 | <ski> | (s/apply types to/apply to types/) |
| 07:18:34 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 07:18:49 | → | titibandit joins (~titibandi@xdsl-78-35-214-18.nc.de) |
| 07:18:50 | <ski> | it would make sense to me to have `2 @Int' working, though |
| 07:19:31 | <irfan> | [exa]: ah, i see. i had not declared the type for the value i was applying it for. that's why it was not working. thanks for the clarification, ski, [exa]! |
| 07:19:34 | <ski> | GHC authors might be convincable to make that work |
| 07:19:46 | <irfan> | ski: agreed. |
| 07:20:04 | → | gurkenglas joins (~gurkengla@p57b8a60f.dip0.t-ipconnect.de) |
| 07:20:16 | <ski> | irfan : declared the type, how ? |
| 07:22:51 | <irfan> | ski: explicitly declared for some type in question i had. from the docs, i think it's not supposed to work for inferred types. |
| 07:24:21 | → | alternateved joins (~user@staticline-31-183-149-36.toya.net.pl) |
| 07:25:12 | <ski> | "it" referring to ? |
| 07:25:22 | <irfan> | % view = show |
| 07:25:22 | <yahb2> | <no output> |
| 07:25:29 | <ski> | perhaps your `x' was actually monomorphic ? |
| 07:25:34 | <irfan> | % view @Int $ 7 |
| 07:25:34 | <yahb2> | <interactive>:106:1: error: ; • Cannot apply expression of type ‘a0 -> String’ ; to a visible type argument ‘Int’ ; • In the expression: view @Int ; In the expression: view @Int... |
| 07:26:11 | <irfan> | ski: no, i've got the restriction turned off. |
| 07:27:34 | <irfan> | % let view :: Show a => a -> String; view = show |
| 07:27:34 | <yahb2> | <no output> |
| 07:27:40 | <irfan> | view @Int $ 7 |
| 07:27:57 | <irfan> | % view @Int $ 7 |
| 07:27:57 | <yahb2> | "7" |
| 07:31:05 | <ski> | % let view = show |
| 07:31:05 | <yahb2> | <no output> |
| 07:31:09 | <ski> | % :t view |
| 07:31:09 | <yahb2> | view :: Show a => a -> String |
| 07:31:13 | <ski> | % view @Int 2 |
| 07:31:13 | <yahb2> | <interactive>:128:1: error: ; • Cannot apply expression of type ‘a0 -> String’ ; to a visible type argument ‘Int’ ; • In the expression: view @Int 2 ; In an equation for ‘it’: i... |
| 07:31:52 | → | MajorBiscuit joins (~MajorBisc@86-88-79-148.fixed.kpn.net) |
| 07:32:28 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 07:35:47 | → | dos__^^ joins (~user@user/dos/x-1723657) |
| 07:36:42 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 07:38:03 | → | zeenk joins (~zeenk@2a02:2f04:a311:2d00:6865:d863:4c93:799f) |
| 07:39:03 | → | tcard_ joins (~tcard@p945242-ipngn9701hodogaya.kanagawa.ocn.ne.jp) |
| 07:39:54 | → | vglfr joins (~vglfr@194.9.14.33) |
| 07:40:03 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Read error: Connection reset by peer) |
| 07:40:20 | → | dibblego joins (~dibblego@122-199-1-30.ip4.superloop.com) |
| 07:40:21 | × | dibblego quits (~dibblego@122-199-1-30.ip4.superloop.com) (Changing host) |
| 07:40:21 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 07:41:02 | × | Jonno_FTW quits (~come@user/jonno-ftw/x-0835346) (Ping timeout: 255 seconds) |
| 07:41:17 | × | son0p quits (~ff@181.136.122.143) (Ping timeout: 245 seconds) |
| 07:41:42 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 245 seconds) |
| 07:41:42 | × | tcard quits (~tcard@p945242-ipngn9701hodogaya.kanagawa.ocn.ne.jp) (Ping timeout: 245 seconds) |
| 07:41:42 | × | ByronJohnson quits (~bairyn@50-250-232-19-static.hfc.comcastbusiness.net) (Ping timeout: 245 seconds) |
| 07:42:43 | → | Jonno_FTW joins (~come@api.carswap.me) |
| 07:42:43 | × | Jonno_FTW quits (~come@api.carswap.me) (Changing host) |
| 07:42:43 | → | Jonno_FTW joins (~come@user/jonno-ftw/x-0835346) |
| 07:43:25 | → | ByronJohnson joins (~bairyn@50-250-232-19-static.hfc.comcastbusiness.net) |
| 07:43:32 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 07:49:26 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:5f26:adbf:e619:7a29) (Ping timeout: 240 seconds) |
| 07:49:42 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 07:50:35 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:8097:2d55:dcdf:fe15) |
| 07:51:11 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 07:52:44 | → | machinedgod joins (~machinedg@d172-219-86-154.abhsia.telus.net) |
| 07:54:42 | → | Midjak joins (~Midjak@82.66.147.146) |
| 07:55:25 | × | yvan-sraka quits (~yvan-srak@209.red-2-139-126.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 07:55:44 | → | yvan-sraka joins (~yvan-srak@209.red-2-139-126.dynamicip.rima-tde.net) |
| 07:56:03 | → | frost joins (~frost@user/frost) |
| 08:04:26 | → | kuribas joins (~user@188.189.234.111) |
| 08:04:42 | → | sandy_doo joins (~sandydoo@185.209.196.136) |
| 08:09:27 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:12:46 | × | titibandit quits (~titibandi@xdsl-78-35-214-18.nc.de) (Remote host closed the connection) |
| 08:15:28 | → | sandydoo joins (~sandydoo@194.87.95.71) |
| 08:15:29 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 08:15:52 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 08:16:43 | → | VictorHugenay joins (~jh@user/VictorHugenay) |
| 08:17:20 | × | sandy_doo quits (~sandydoo@185.209.196.136) (Ping timeout: 268 seconds) |
| 08:19:53 | → | sandy_doo joins (~sandydoo@146.70.117.210) |
| 08:22:09 | × | merijn quits (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 08:22:16 | × | sandydoo quits (~sandydoo@194.87.95.71) (Ping timeout: 268 seconds) |
| 08:23:12 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
| 08:23:30 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 08:28:33 | × | Techcable quits (~Techcable@user/Techcable) (Remote host closed the connection) |
| 08:30:06 | → | Techcable joins (~Techcable@user/Techcable) |
| 08:36:52 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 08:39:58 | → | Jade1 joins (~Jade1@ip-178-201-128-039.um46.pools.vodafone-ip.de) |
| 08:40:39 | → | hsw joins (~hsw@112-104-144-236.adsl.dynamic.seed.net.tw) |
| 08:42:07 | × | MajorBiscuit quits (~MajorBisc@86-88-79-148.fixed.kpn.net) (Ping timeout: 245 seconds) |
| 08:43:15 | → | MajorBiscuit joins (~MajorBisc@c-001-031-013.client.tudelft.eduvpn.nl) |
| 08:45:11 | <kuribas> | When it comes to correctness, it looks to my like the Curry/Howard isomorphism is the only way to get there. |
| 08:45:37 | <kuribas> | At least for formal correctness, not testing. |
| 08:45:53 | <kuribas> | Most efforts seem to lead in that direction. |
| 08:46:01 | <kuribas> | Haskell is become more and more dependently typed. |
| 08:46:22 | <merijn> | That depends how you write Haskell... |
| 08:47:47 | → | __monty__ joins (~toonn@user/toonn) |
| 08:51:11 | <kuribas> | I mean if you want to do metaprogramming and still have correctness. |
| 08:51:28 | <kuribas> | Either you give up on correctness, or you end up with a lot of type level computations. |
| 08:51:51 | <kuribas> | And Generics are a really ugly part of haskell. |
| 08:54:47 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 08:57:10 | → | benin0 joins (~benin@183.82.25.146) |
| 08:57:19 | <merijn> | kuribas: Depends, you can do meta programming with TTH too |
| 08:58:10 | <kuribas> | sure, but it is harder to get correct. |
| 08:58:14 | × | zeenk quits (~zeenk@2a02:2f04:a311:2d00:6865:d863:4c93:799f) (Quit: Konversation terminated!) |
| 08:58:29 | <kuribas> | does TTH ensure the generated program is typesafe? |
| 08:58:55 | <kuribas> | Well, it cannot crash at runtime, so that's something. |
| 09:01:55 | → | nate4 joins (~nate@98.45.169.16) |
| 09:05:37 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 09:06:34 | <kuribas> | Still, I find using TH to generate types or constraints a lot more cumbersome that calculating a type in the same language. |
| 09:06:42 | × | nate4 quits (~nate@98.45.169.16) (Ping timeout: 245 seconds) |
| 09:07:04 | × | Jade1 quits (~Jade1@ip-178-201-128-039.um46.pools.vodafone-ip.de) (Quit: Client closed) |
| 09:07:16 | <merijn> | kuribas: TTH is type safe, yes |
| 09:07:33 | <kuribas> | Can it deal with polymorphic functions and data? |
| 09:07:35 | <merijn> | In that it only generates code that typechecks |
| 09:07:52 | → | Jade1 joins (~Jade1@ip-178-201-128-039.um46.pools.vodafone-ip.de) |
| 09:07:56 | <kuribas> | hmm, right |
| 09:09:46 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 09:12:23 | × | ozkutuk quits (~ozkutuk@176.240.173.153) (Ping timeout: 252 seconds) |
| 09:13:07 | × | mbuf quits (~Shakthi@122.165.55.71) (Ping timeout: 252 seconds) |
| 09:13:50 | → | mbuf joins (~Shakthi@122.165.55.71) |
| 09:13:53 | → | ozkutuk joins (~ozkutuk@176.240.173.153) |
| 09:15:53 | × | Luj quits (~Luj@2a01:e0a:5f9:9681:abed:9db1:6133:89ac) (Quit: Ping timeout (120 seconds)) |
| 09:16:14 | → | Luj joins (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) |
| 09:19:36 | → | enemeth79 joins (uid309041@id-309041.lymington.irccloud.com) |
| 09:21:16 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:21:35 | × | mbuf quits (~Shakthi@122.165.55.71) (Read error: Connection reset by peer) |
| 09:21:47 | → | mbuf joins (~Shakthi@122.165.55.71) |
| 09:22:27 | × | shriekingnoise quits (~shrieking@186.137.167.202) (Quit: Quit) |
| 09:27:36 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 09:27:43 | × | fef quits (~thedawn@user/thedawn) (Ping timeout: 268 seconds) |
| 09:28:27 | <ski> | ("TTH" as opposed to "TH" ?) |
| 09:28:37 | <merijn> | yes |
| 09:28:49 | <ski> | what does the former expand to ? |
| 09:28:56 | × | Jade1 quits (~Jade1@ip-178-201-128-039.um46.pools.vodafone-ip.de) (Quit: Client closed) |
| 09:28:57 | <merijn> | Typed TH |
| 09:29:03 | <ski> | ah, right |
| 09:29:37 | ski | 's more familiar with MetaML (and to some extent MetaOCaml) |
| 09:30:06 | <ski> | kuribas : still wondering how CH factors into it |
| 09:30:40 | × | yvan-sraka quits (~yvan-srak@209.red-2-139-126.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 09:31:11 | <ski> | (type systems for staged programming have been related to modal logics, mind) |
| 09:32:35 | <ski> | kuribas : what's the difference between generation and calculation, there ? |
| 09:32:37 | <kuribas> | ski: CH? |
| 09:32:43 | <ski> | Curry-Howard |
| 09:33:17 | → | EvanR_ joins (~EvanR@user/evanr) |
| 09:33:51 | <kuribas> | Well, thinking of types as proofs helps in modelling complex logic. |
| 09:34:01 | <kuribas> | with GADTs, dependent types, etc... |
| 09:34:15 | × | EvanR quits (~EvanR@user/evanr) (Remote host closed the connection) |
| 09:34:25 | <kuribas> | With dependent types I can make a type that contains arbitrary code to solve a constraint. |
| 09:35:00 | <kuribas> | But without them I am forced to generate the Constraints or types using TH. |
| 09:35:33 | <ski> | itym inhabitants of types as proofs |
| 09:36:16 | <kuribas> | yes |
| 09:36:23 | <ski> | well, you said "same language", which i took to be TH |
| 09:36:57 | <kuribas> | well, TH is haskell, but it operates on a syntactic level. |
| 09:37:22 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 09:37:23 | <kuribas> | Though dependent type checking does also... hmm... |
| 09:37:28 | <merijn> | It operates at an AST level, though? |
| 09:37:35 | <ski> | so what is the difference between generating a type, and calculating a type, in TH ? |
| 09:37:39 | <merijn> | dependent types aren't syntactic? |
| 09:37:40 | <kuribas> | merijn: right |
| 09:37:48 | <ski> | (or did i misunderstand your statement) |
| 09:37:59 | <kuribas> | merijn: dependent type checking works by normalisation of expressions. |
| 09:38:10 | <kuribas> | merijn: equality is syntactic equality after type checking. |
| 09:39:09 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 09:39:20 | <kuribas> | well, before type checking... |
| 09:40:09 | <kuribas> | I just seem to be able to better solve hard type level stuff when thinking of types as propositions. |
| 09:40:28 | <kuribas> | GADTs as carrying "proofs". |
| 09:41:21 | <kuribas> | I don't mean to say that formal proofs are alway better than just writing tests. |
| 09:41:42 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 245 seconds) |
| 09:41:50 | <kuribas> | But when you go the way of formal correctness, it seems you end up with Curry/Howard. |
| 09:42:04 | <merijn> | Not really |
| 09:42:12 | <merijn> | At least, I don't see it |
| 09:42:40 | <kuribas> | merijn: counterexample? |
| 09:43:24 | → | kenran joins (~kenran@p200300df770eae00d275524cc766554f.dip0.t-ipconnect.de) |
| 09:43:46 | <ski> | Racket has an interesting higher-order contract system, which can interact usefully with Typed Racket |
| 09:44:24 | <kuribas> | contracts sounds to me like runtime testing, no? |
| 09:44:26 | × | sandy_doo quits (~sandydoo@146.70.117.210) (Ping timeout: 268 seconds) |
| 09:44:32 | <ski> | intuitionistic logic doesn't necessarily imply CH |
| 09:44:36 | <ski> | kuribas : yes, indeed |
| 09:45:04 | <merijn> | kuribas: A lot of formal methods verification stuff doesn't really interact with CH all that much |
| 09:45:29 | <merijn> | kuribas: It's a lot more "designing state machines and proof certain transitions/states can never happen" |
| 09:45:55 | <kuribas> | right. Maybe I am thinking more about "correct by construction". |
| 09:46:10 | <kuribas> | Rather than, I have a program, now prove it correct. |
| 09:46:14 | <ski> | like specifying that a higher-order function has some preconditions on its parameters, and some postcondition involving those and the result, and that the preconditions on the function parameters in turn can have pre- and post- conditions. and when a contract fails, you should properly distinguish between the higher-order function failing, and its callback failing, properly attributing blame either to the |
| 09:46:20 | <ski> | callee or the caller |
| 09:46:34 | <ski> | (i believe Wadler also wrote some paper about contracts) |
| 09:46:48 | <kuribas> | ski: but if it is runtime, can you call it still formal verification? |
| 09:47:01 | <ski> | i wouldn't |
| 09:48:22 | <kuribas> | I think "correct by construction" is much more feasible. |
| 09:48:24 | <ski> | (just mentioning it as an interesting case of "tests", one that can interact with types, iirc) |
| 09:48:31 | <lortabac> | kuribas: "correct by construction" is not the only way to prove programs correct |
| 09:48:47 | <lortabac> | you can have extrinsic proofs in the program itself |
| 09:49:03 | <lortabac> | or you can have refinements à la Liquid Haskell |
| 09:49:04 | <kuribas> | I just proving programs correct after writing the program very tedious and hard. |
| 09:49:08 | ski | . o O ( AoC ) |
| 09:49:42 | <ski> | i recently looked a bit at ATS .. quite interesting system |
| 09:49:57 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 09:50:02 | <lortabac> | kuribas: it depends |
| 09:50:35 | → | son0p joins (~ff@181.136.122.143) |
| 09:50:39 | <ski> | (being able to reason about system-level concepts like mutable locations, in a dependent setting) |
| 09:51:23 | <lortabac> | for example "correct by construction" data types means you need a different type for each invariant |
| 09:51:51 | ski | . o O ( McBride's ornaments ) |
| 09:52:08 | <lortabac> | whereas you might use lists and add extrinsic proofs for the properties you want to check |
| 09:53:08 | → | CiaoSen joins (~Jura@p200300c9570ffb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 09:54:44 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 09:58:00 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds) |
| 10:02:29 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 10:05:20 | → | sandy_doo joins (~sandydoo@146.70.117.210) |
| 10:14:21 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds) |
| 10:16:33 | × | sandy_doo quits (~sandydoo@146.70.117.210) (Ping timeout: 252 seconds) |
| 10:18:58 | <kuribas> | lortabac: also correct by construction functions, where you have to pass a constraint which proves some invariants. |
| 10:19:15 | <kuribas> | "correct by constraints" maybe ? |
| 10:34:31 | × | vglfr quits (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 10:35:38 | → | vglfr joins (~vglfr@194.9.14.33) |
| 10:42:02 | <kuribas> | ski: with dependent types you could make contracts as constraints on a passed value. |
| 10:42:13 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 10:42:56 | <kuribas> | ski: (foo:MyData) -> MeetConstraints foo FooConstraints => Result |
| 10:43:06 | <kuribas> | (maybe offtopic because this is idris) |
| 10:43:48 | <kuribas> | s/MeetConstraints/MeetContracts |
| 10:44:51 | <kuribas> | but that mostly works if the contract is easily proven. |
| 10:45:12 | <kuribas> | For complex stuff making tests is easier. |
| 10:47:07 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 10:47:11 | × | frost quits (~frost@user/frost) (Quit: Client closed) |
| 10:47:32 | → | frost joins (~frost@user/frost) |
| 10:50:07 | <lisbeths> | I want to take a second to admire haskell curry, probably one of the most syntactically successful programmers of all time. |
| 10:50:43 | <lisbeths> | Without the notion of a lambda that takes an x that returns a lamba from moses shoenfinkel, and without currying, we wouldn't have the beauty of haskell. |
| 10:50:52 | <lisbeths> | Thank you to these two brilliant men. |
| 10:58:32 | → | sandy_doo joins (~sandydoo@146.70.117.210) |
| 11:06:24 | <kuribas> | is this a bot? |
| 11:06:26 | <ski> | kuribas : hm, right. i was more thinking of executable contracts (e.g. a contract that a given function parameter only computes prime numbers) |
| 11:06:32 | <ski> | no, kuribas |
| 11:06:52 | <kuribas> | because that sounded like a random blurb of words. |
| 11:06:54 | → | xff0x joins (~xff0x@2405:6580:b080:900:13b:63d1:e32e:fe38) |
| 11:08:02 | <ski> | (well, with LiquidHaskell you can also write stuff like `{foo :: MyData | ..foo..} -> Result') |
| 11:08:12 | <kuribas> | right |
| 11:10:17 | → | misterfish joins (~misterfis@ip214-130-173-82.adsl2.static.versatel.nl) |
| 11:17:08 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 11:17:34 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 11:18:09 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 11:18:44 | <kuribas> | lisbeths: haskell curry wasn't a programmer |
| 11:19:40 | <lisbeths> | the language police have arrived |
| 11:20:06 | <kuribas> | semantics police maybe? |
| 11:21:17 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 11:21:52 | × | gurkenglas quits (~gurkengla@p57b8a60f.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 11:23:06 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Ping timeout: 268 seconds) |
| 11:26:16 | → | jean-paul[m] joins (~jean-paul@2001:470:69fc:105::d1ab) |
| 11:26:25 | ← | exarkun parts (~exarkun@user/exarkun) (WeeChat 3.5) |
| 11:29:58 | <lisbeths> | you'll never get me copper |
| 11:30:04 | lisbeths | runs |
| 11:30:14 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 11:30:19 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 244 seconds) |
| 11:30:25 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 11:31:03 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 11:31:31 | <ski> | there used to be a SyntaxPolice in here |
| 11:31:39 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 11:32:07 | <jackdk> | do you mean, "you'll never fetch me [some] copper", "you'll never take my copper", or "you [policeman] will never get me"? |
| 11:32:27 | <ski> | @quote SyntaxNinja |
| 11:32:27 | <lambdabot> | SyntaxNinja says: You'd be surprised how hard is to hire haskellers :( They're all like, "Yeah, I'll come work for you, and by 'come' I mean stay here and work remotely and by 'work for you' I mean |
| 11:32:28 | <lambdabot> | I'll keep doing what I'm doing." ;) |
| 11:32:32 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 245 seconds) |
| 11:33:01 | <Hecate> | jackdk: 3rd one :) |
| 11:34:32 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 11:36:07 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Ping timeout: 252 seconds) |
| 11:39:26 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 11:39:38 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 11:39:50 | <__monty__> | So critical of remote work. And I'm sure it's not as hard to find people willing to write non research-type Haskell nowadays. |
| 11:42:53 | <ski> | that was some years ago, true |
| 11:43:06 | <ski> | (possibly more than ten, i don't recall) |
| 11:43:29 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 11:43:50 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 11:57:52 | <merijn> | I mean, that quote is referring to "we tried hire ekmett, dons, bos, simon marlow, etc." |
| 11:58:17 | <merijn> | I mean, 90% of #haskell was people like that 10-15 years ago |
| 11:58:30 | <merijn> | At least, the active portion :p |
| 12:00:35 | <ski> | it was a fun time :b |
| 12:01:23 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 12:06:49 | × | ozkutuk quits (~ozkutuk@176.240.173.153) (Quit: The Lounge - https://thelounge.chat) |
| 12:07:38 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 12:09:08 | × | enemeth79 quits (uid309041@id-309041.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 12:09:18 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 12:19:37 | × | Pickchea quits (~private@user/pickchea) (Ping timeout: 245 seconds) |
| 12:24:15 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 12:24:32 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 12:25:38 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:29:39 | → | kuribas` joins (~user@silversquare.silversquare.eu) |
| 12:30:52 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 245 seconds) |
| 12:31:33 | × | kuribas quits (~user@188.189.234.111) (Ping timeout: 268 seconds) |
| 12:31:39 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:33:56 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 12:38:11 | × | noteness quits (~noteness@user/noteness) (Remote host closed the connection) |
| 12:41:03 | → | noteness joins (~noteness@user/noteness) |
| 12:43:04 | <siers> | work they did not? |
| 12:43:13 | <Axman6> | those were the days... |
| 12:43:58 | <Axman6> | Here I am, writing Haskell* remotely for the man, doin my job. What a chump |
| 12:44:21 | <siers> | what is the product about? |
| 12:44:27 | <Axman6> | (* "Haskell" = Daml) |
| 12:45:18 | <siers> | anyway, I have an actual question. I am looking at this recursion scheme tutorial (in scala, I'm sorry) and it is calling the fold function an "algebra" and the unfold function a "coalgebra". First, is this the correct terminology and second, why is it an algebra and is it the algebra kind of algebra — i.e. set of operations and laws on some set of elements? |
| 12:45:51 | <siers> | I guess I'm thinking of an algebraic structure |
| 12:46:38 | <ski> | the argument to the fold/unfold is the algebra/coalgebra |
| 12:47:08 | <siers> | you're absolutely right and that's what I meant, sorry |
| 12:47:15 | <siers> | fold function as in the function you pass to fold |
| 12:47:20 | <ski> | cata :: Functor f => (f r -> r) -> (Mu f -> r) -- fold |
| 12:47:32 | <siers> | mu is the fix operator? |
| 12:47:39 | <ski> | ana :: Functor f => (s -> f s) -> (s -> Nu f) -- unfold |
| 12:47:49 | <siers> | or I guess type |
| 12:47:53 | <Axman6> | @hoogle Mu |
| 12:47:53 | <lambdabot> | Data.Fix newtype Mu f |
| 12:47:53 | <lambdabot> | Data.Fix Mu :: (forall a . (f a -> a) -> a) -> Mu f |
| 12:47:53 | <lambdabot> | Data.ISO3166_CountryCodes MU :: CountryCode |
| 12:47:58 | <ski> | `Mu f' is the least fixed point of `f', and `Nu f' is the greatest one |
| 12:48:52 | <ski> | e.g. `Mu (Compose Maybe (a,))' is finite lists of `a's, while `Nu (Compose Maybe (a,))' is potentially finite streams of `a's |
| 12:49:20 | <siers> | @hoogle Compose |
| 12:49:21 | <lambdabot> | module Data.Functor.Compose |
| 12:49:21 | <lambdabot> | Data.Functor.Compose newtype Compose f g a |
| 12:49:21 | <lambdabot> | Data.Functor.Compose Compose :: f (g a) -> Compose f g a |
| 12:49:28 | <siers> | ah, ok |
| 12:49:39 | <siers> | suspected so |
| 12:49:51 | <Axman6> | Is that Mu above the right one? |
| 12:50:03 | <siers> | looks about right |
| 12:50:09 | <ski> | `Mu Maybe' is natural numbers. `Nu Maybe' is natural numbers extended with an infinity element, `inf = Succ inf' (`Nu Maybe' is also sometimes known as the "generic convergent sequence", or the "one-point compactification of the naturals") |
| 12:50:34 | <Axman6> | I think I was actually expecting to see Fix actually... newtype Fix f = Fix (f (fix f)) |
| 12:50:43 | <Axman6> | Fix* |
| 12:50:54 | <ski> | in Haskell, `Mu' and `Nu' are both expressed in the same way. but there's a conceptual distinction, when we ignore bottom elements |
| 12:51:42 | <ski> | Axman6 : well, that `Mu' above is a different encoding .. |
| 12:52:07 | × | misterfish quits (~misterfis@ip214-130-173-82.adsl2.static.versatel.nl) (Ping timeout: 245 seconds) |
| 12:52:18 | <ski> | newtype Mu f = In (f (Mu f)) -- is the encoding i was thinking of |
| 12:53:08 | → | coot joins (~coot@213.134.176.158) |
| 12:53:23 | <Axman6> | yeah that's what I was thinking about |
| 12:53:44 | <ski> | siers : anyway, consider a monoid, on a type `M'. you have a neutral element `mempty :: M', and a binary combination `mappend,(<>) :: M -> M -> M' .. you also have three laws involving these two operations |
| 12:54:02 | <siers> | right |
| 12:54:05 | × | coot quits (~coot@213.134.176.158) (Client Quit) |
| 12:54:35 | → | coot joins (~coot@213.134.176.158) |
| 12:56:06 | × | frost quits (~frost@user/frost) (Ping timeout: 252 seconds) |
| 12:56:52 | → | autophagian joins (~mika@ip5f5bf3a3.dynamic.kabel-deutschland.de) |
| 12:56:55 | <ski> | now .. given any set/type, you can form the "free monoid" on it, which is the "least restricted" set/type which includes all the elements of the former one, and also has the two monoid operations defined, such that expressions involving them and the elements are *only* considered equal if you can prove them to be equal by the laws |
| 12:57:43 | <ski> | this free monoid is the monoid of (finite) lists over the type `a', with singleton map as the inclusion, and empty list and append as the monoid operations |
| 12:59:11 | <siers> | I am not familiar with free monoids |
| 12:59:22 | <siers> | should this explanation be enough to fully grasp them? :) |
| 13:00:02 | <ski> | if the element type `a' is itself a monoid, you can "evaluate/interpret" the list of elements, by replacing empty list with `mempty :: M', and append with `mappend :: M -> M -> M' (it doesn't matter which way you associate, due to the laws) |
| 13:00:17 | <ski> | @type Control.Lens.Fold.foldBy :: (m -> m -> m) -> m -> ([m] -> m) |
| 13:00:19 | <lambdabot> | (m -> m -> m) -> m -> [m] -> m |
| 13:00:25 | <ski> | @type fold :: Monoid m => [m] -> m |
| 13:00:26 | <lambdabot> | Monoid m => [m] -> m |
| 13:00:36 | → | gurkenglas joins (~gurkengla@p57b8a60f.dip0.t-ipconnect.de) |
| 13:01:26 | <siers> | so you get a monoid for a list of elements and that's the free monoid? |
| 13:02:49 | <ski> | (you can replace `[m]' with `t m', where `Foldable t' holds, since `Foldable', more or less, means "list-like". although see "Free Monoids in Haskell" <https://web.archive.org/web/20150222212709/http://comonad.com/reader/2015/free-monoids-in-haskell/>) |
| 13:02:50 | <siers> | so in the free monoid, the items are both the elements of a and expressions with the monoid ops and "a"s? |
| 13:03:21 | <ski> | the free monoid of `a' is `[a]' (if you ignore the infinite (and the partial) lists) |
| 13:03:26 | → | nate4 joins (~nate@98.45.169.16) |
| 13:03:30 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 13:03:32 | → | waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 13:03:45 | <siers> | what's a partial list? are they in math? |
| 13:04:02 | <ski> | (you take the free monoid of a type/set (the element *type*), not of an element, or a list of them) |
| 13:04:10 | <ski> | > 0 : 1 : undefined |
| 13:04:12 | <lambdabot> | [0,1*Exception: Prelude.undefined |
| 13:04:24 | × | nek0 quits (~nek0@2a01:4f8:222:2b41::12) (Quit: The Lounge - https://thelounge.chat) |
| 13:04:29 | <ski> | in denotational semantics, written like `0 : 1 : _|_' |
| 13:05:16 | <siers> | "¬ (0 : 1 : ⊥)" :) |
| 13:05:47 | <ski> | anyway, consider the two arguments, of type `m -> m -> m' and `m', to `foldBy'. these describe the monoid operations that we've chosen to use, on `m' (the `foldBy' operation assumes that these actually satisfies the monoid laws, as a precondition) |
| 13:06:01 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 244 seconds) |
| 13:06:07 | <siers> | ski, oh, I understood that a is the type/set in one instance and an element in the other in my sentence. I am being imprecise, sorr.y |
| 13:06:43 | <ski> | using "type algebra", we can reexpress these as `(m,m) -> m' and `() -> m'. or in more mathy notation, `m^2 -> m' and `1 -> m' (or `m^0 -> m', if you prefer) |
| 13:07:08 | <ski> | so, `(m -> m -> m) -> m -> ([m] -> m) |
| 13:07:09 | <siers> | m^0 — cute :) |
| 13:07:21 | <siers> | I'll try to decode that bit about the foldBy |
| 13:07:32 | × | Furor quits (~colere@about/linux/staff/sauvin) (Ping timeout: 245 seconds) |
| 13:08:06 | <ski> | so, `(m -> m -> m) -> m -> ([m] -> m)' becomes `((m,m) -> m) -> (() -> m) -> ([m] -> m)' becomes `(Either () (m,m) -> m) -> ([m] -> m)' (you could say `Maybe' instead of `Either ()') |
| 13:08:12 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 13:08:16 | → | Colere joins (~colere@about/linux/staff/sauvin) |
| 13:08:23 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 13:08:28 | <siers> | those look isomorphic :) |
| 13:08:33 | × | nate4 quits (~nate@98.45.169.16) (Ping timeout: 268 seconds) |
| 13:08:33 | <siers> | maybe / either () |
| 13:09:05 | <ski> | this `Either () (m,m) -> m' / `1 + m^2 -> m' / `m^0 + m^2 -> m' is the type of (monoid, in this case) algebras, on `m' (assuming the laws are satisfied) |
| 13:09:21 | <ski> | it sums up all the operations of the algebra, in a single operation |
| 13:09:37 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 13:10:34 | → | Furor joins (~colere@about/linux/staff/sauvin) |
| 13:10:42 | <ski> | a Peano algebra on a set `p' consists of an element `zero :: p' and a function `succ :: p -> p'. in this case, there's no laws. e.g. `p' could be `Bool', `zero' could be `True', and `succ' could be `not' |
| 13:11:31 | → | Pickchea joins (~private@user/pickchea) |
| 13:12:22 | <siers> | ok, I got it all |
| 13:12:48 | <ski> | natural numbers is the "initial" peano algebra. for any peano algebra `(p,zero,succ)', there is a function (specifically a peano algebra (homo)morphism) `fold_zero_succ :: Nat -> p'. in Haskell, we'd express this as parameterized over `zero' and `succ', as `fold :: p -> (p -> p) -> (Nat -> p)' |
| 13:12:51 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 13:13:22 | × | Colere quits (~colere@about/linux/staff/sauvin) (Ping timeout: 245 seconds) |
| 13:14:09 | × | CiaoSen quits (~Jura@p200300c9570ffb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 13:14:24 | <siers> | yeah, I can see why that fold is a homomorphism |
| 13:14:32 | <ski> | anyway, the general pattern that seems to be emerging is that we can express the operations over the carrier / underlying set `a' as a single operation, in `F a -> a', for some functor `F' (often a polynomial one, like `F a = 1 + a^2' or `F a = 1 + a') |
| 13:14:48 | <ski> | in such a case, we talk about an `F'-algebra (`F' being a functor) |
| 13:16:11 | <ski> | (i'm not aware of how this is extended from the case of an algebra with no laws (an "anarchic algebra", like Peano, or directed multigraphs), to one with laws (like monoids, groups, rings, vector spaces, lattices, boolean algebras ..)) |
| 13:16:14 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 13:17:25 | <ski> | anyway, for unfold, we typically have, instead of a "recursive result type" `r', that we combine `r -> r -> r', and generate at leaves `r', and then use those operations to crush a structure to a single result `r' |
| 13:19:50 | <ski> | instead of that, we have a state type `s', some observations/properties, like `s -> C' for constants `C', and some state transitions, like `s -> s', or `s -> (P -> s)' (for some parameter `P'). anyway, given `unfold :: (s -> C) -> (s -> (P -> s)) -> (s -> Obj)', where `Obj' is the "OO-like" (or dynamical-system like) type we're unfolding into |
| 13:20:35 | <ski> | we can reexpress that as `(s -> (C,P -> s)) -> (s -> Ob)'. which generalizes similarly to `(s -> f s) -> (s -> Nu s)', where `f' is again a functor |
| 13:20:45 | <ski> | the input of type `s -> f s' here is the `f'-coalgebra |
| 13:20:53 | → | hippoid joins (~hippoid@d53-64-120-188.nap.wideopenwest.com) |
| 13:23:51 | <ski> | "A Tutorial on (Co)Algebras and (Co)Induction" by Bart Jacobs,Jan Rutten in 1997 at <https://www.cs.ru.nl/B.Jacobs/PAPERS/JR.pdf> might perhaps be helpful |
| 13:24:47 | <ski> | (apparently there's also a "A Tutorial on Co-induction and Functional Programming" in 1994 by Andrew D. Gordon at <https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.3914>, but i haven't read this) |
| 13:25:16 | → | superice joins (~superice@2a01:7c8:aab9:48e:5054:ff:fe7b:347) |
| 13:25:30 | <siers> | hm, wouldn't that Obj have to appear twice in unfold? I guess I misunderstood something |
| 13:26:10 | <ski> | cata phi = phi . fmap (cata phi) . out |
| 13:26:26 | <ski> | ana psi = In . fmap (ana psi) . psi |
| 13:26:46 | <ski> | (also look up "recursion schemes", and, perhaps, "Squiggol") |
| 13:28:04 | <ski> | (assuming `newtype Fix f = In {out :: f (Fix f)}' as encoding for both `Mu f' and `Nu f') |
| 13:29:25 | <siers> | I read about F-algebras once, but that made less sense than what I heard from you now. |
| 13:29:52 | → | zmt00 joins (~zmt00@user/zmt00) |
| 13:30:20 | <siers> | And I cannot believe you wrote out all of this for me (and for anyone else who's reading), that is amazing. I almost understand all of it, but I'm decoding the bit about the unfold. |
| 13:31:45 | ← | superice parts (~superice@2a01:7c8:aab9:48e:5054:ff:fe7b:347) () |
| 13:34:02 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 13:34:09 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 13:37:06 | ski | . o O ( "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" by Erik Meijer,Maarten Fokkinga,Ross Paterson in 1991-08-26 at <https://maartenfokkinga.github.io/utwente/mmf91m.pdf> ) |
| 13:37:17 | ski | . o O ( "Bananas in Space: Extending Fold and Unfold to Exponential Types" by Erik Meijer,Graham Huttom in 1995 at <https://www.cs.nott.ac.uk/~pszgmh/bananas.pdf> ) |
| 13:37:24 | ski | . o O ( "A tutorial on the universality and expressiveness of fold" by Graham Hutton in 1999-07 at <https://www.cs.nott.ac.uk/~pszgmh/bib.html#fold> ) |
| 13:37:29 | <merijn> | That first paper is rough, though :p |
| 13:38:17 | gdd1 | is now known as gdd |
| 13:39:56 | <ski> | anyway, the other encoding of `Mu f' (roughly speaking) comes from taking `cata :: (f r -> r) -> (Mu f -> r)', `flip'ping it into `flip cata :: Mu f -> (forall r. (f r -> r) -> r)', and claiming that this is a bijection, electing to define `Mu f' to amount to `forall r. (f r -> r) -> r' |
| 13:41:28 | <ski> | similarly, we can take `ana :: (s -> f s) -> (s -> Nu s)', and `uncurry' (and `flip', if we want to, which i do) it into `(exists s. (s,s -> f s)) -> Nu f', and similarly define `Nu f' as `exists s. (s,s -> f s)' |
| 13:42:45 | <ski> | the former is related to the Church (or CPS) encoding of a data type. the latter to the (what i call) "State encoding" |
| 13:43:38 | <ski> | @quote separation.of |
| 13:43:39 | <lambdabot> | GuySteele says: Some people prefer not to commingle the functional, lambda-calculus part of a language with the parts that do side effects. It seems they believe in the separation of Church and |
| 13:43:39 | <lambdabot> | state. |
| 13:43:45 | <ski> | @quote are.dual |
| 13:43:45 | <lambdabot> | ski says: I'd rather say that in Haskell, Church and State are dual |
| 13:45:08 | <ski> | @hoogle Nu |
| 13:45:09 | <lambdabot> | Data.Fix data Nu f |
| 13:45:09 | <lambdabot> | Data.Fix Nu :: (a -> f a) -> a -> Nu f |
| 13:45:09 | <lambdabot> | Data.ISO3166_CountryCodes NU :: CountryCode |
| 13:49:29 | <ski> | (er, s/s -> Nu s/s -> Nu f/) |
| 13:49:31 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 13:49:54 | <siers> | an F-algebra is the "Mu f"? |
| 13:49:54 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 13:50:23 | <ski> | no, an `F'-algebra (over carrier `r') is a value of type `F r -> r' |
| 13:50:33 | <siers> | alright |
| 13:50:38 | <ski> | an `F'-coalgebra (over carrier `s') is a value of type `s -> F s' |
| 13:50:54 | <ski> | type Algebra f r = f r -> r |
| 13:51:04 | <ski> | type Coalgebra f s = s -> f s |
| 13:51:06 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 13:51:11 | → | FurudeRika[m] joins (~chitandae@user/FurudeRika) |
| 13:51:16 | <ski> | (i've seen those type synonyms used, occasionally) |
| 13:51:50 | <ski> | cata :: Functor f => Algebra f r -> (Mu r -> r) |
| 13:52:05 | <ski> | er |
| 13:52:08 | <ski> | cata :: Functor f => Algebra f r -> (Mu f -> r) |
| 13:52:12 | <ski> | ana :: Functor f => Coalgebra f s -> (s -> Nu f) |
| 13:53:48 | × | alternateved quits (~user@staticline-31-183-149-36.toya.net.pl) (Remote host closed the connection) |
| 13:56:07 | × | VictorHugenay quits (~jh@user/VictorHugenay) (Quit: Konversation terminated!) |
| 13:58:32 | Furor | is now known as Colere |
| 14:04:27 | → | arjun joins (~arjun@user/arjun) |
| 14:10:44 | → | Nahra joins (~user@static.161.95.99.88.clients.your-server.de) |
| 14:16:11 | × | arjun quits (~arjun@user/arjun) (Read error: Connection reset by peer) |
| 14:16:19 | → | arjun_ joins (~arjun@user/arjun) |
| 14:19:00 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 14:20:05 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:8097:2d55:dcdf:fe15) (Ping timeout: 268 seconds) |
| 14:21:53 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Quit: WeeChat 3.6) |
| 14:22:01 | → | razetime joins (~quassel@117.254.34.168) |
| 14:26:11 | → | waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 14:27:17 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 14:27:37 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 14:29:00 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 14:29:10 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 14:37:42 | × | kenran quits (~kenran@p200300df770eae00d275524cc766554f.dip0.t-ipconnect.de) (Quit: WeeChat info:version) |
| 14:40:54 | × | gurkenglas quits (~gurkengla@p57b8a60f.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 14:42:41 | → | yvan-sraka joins (~yvan-srak@3.red-2-138-130.dynamicip.rima-tde.net) |
| 14:44:14 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 240 seconds) |
| 14:46:31 | → | zebrag joins (~chris@user/zebrag) |
| 14:46:42 | × | sandy_doo quits (~sandydoo@146.70.117.210) (Ping timeout: 245 seconds) |
| 14:50:38 | × | zmt00 quits (~zmt00@user/zmt00) (Quit: Leaving) |
| 14:51:18 | × | Guest55 quits (~Guest55@c-71-198-235-211.hsd1.ca.comcast.net) (Quit: Client closed) |
| 14:54:21 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 14:54:21 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 14:54:21 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 14:54:21 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Write error: Connection reset by peer) |
| 14:54:21 | × | noteness quits (~noteness@user/noteness) (Write error: Connection reset by peer) |
| 14:54:54 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 14:54:56 | → | noteness joins (~noteness@user/noteness) |
| 14:55:02 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 14:55:02 | × | ski quits (~ski@ext-1-213.eduroam.chalmers.se) (Ping timeout: 245 seconds) |
| 14:55:08 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 14:55:11 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 14:55:39 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 15:02:24 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 15:03:08 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 15:04:26 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 15:04:47 | → | zmt00 joins (~zmt00@user/zmt00) |
| 15:05:51 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 15:08:09 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 15:08:11 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Ping timeout: 268 seconds) |
| 15:08:38 | × | Pickchea quits (~private@user/pickchea) (Ping timeout: 240 seconds) |
| 15:09:32 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 15:09:54 | → | pgib joins (~textual@173.38.117.85) |
| 15:12:30 | × | yvan-sraka quits (~yvan-srak@3.red-2-138-130.dynamicip.rima-tde.net) (Ping timeout: 252 seconds) |
| 15:15:50 | × | acidjnk quits (~acidjnk@p200300d6e7058699cc6cce398877ca6f.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 15:16:34 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 15:18:23 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 15:19:44 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 15:22:32 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 15:27:32 | × | razetime quits (~quassel@117.254.34.168) (Ping timeout: 245 seconds) |
| 15:28:47 | × | kuribas` quits (~user@silversquare.silversquare.eu) (Quit: ERC (IRC client for Emacs 26.3)) |
| 15:29:28 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 15:29:48 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 15:32:43 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 15:33:00 | → | naso joins (~naso@193-116-244-197.tpgi.com.au) |
| 15:33:18 | × | naso quits (~naso@193-116-244-197.tpgi.com.au) (Client Quit) |
| 15:36:58 | × | autophagian quits (~mika@ip5f5bf3a3.dynamic.kabel-deutschland.de) (Quit: leaving) |
| 15:38:23 | → | razetime joins (~quassel@117.254.34.223) |
| 15:39:20 | × | irfan quits (~irfan@user/irfan) (Quit: leaving) |
| 15:39:55 | → | waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 15:44:10 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 15:44:10 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 15:44:38 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 15:44:40 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 15:45:42 | → | gmg joins (~user@user/gehmehgeh) |
| 15:49:49 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 15:52:03 | × | zmt00 quits (~zmt00@user/zmt00) (Read error: Connection reset by peer) |
| 15:59:44 | × | zxx7529 quits (~Thunderbi@user/zxx7529) (Quit: zxx7529) |
| 16:01:16 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 16:05:02 | × | vglfr quits (~vglfr@194.9.14.33) (Ping timeout: 245 seconds) |
| 16:08:19 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 16:08:49 | → | gmg joins (~user@user/gehmehgeh) |
| 16:11:49 | → | nek0 joins (~nek0@2a01:4f8:222:2b41::12) |
| 16:15:35 | × | razetime quits (~quassel@117.254.34.223) (Remote host closed the connection) |
| 16:23:25 | → | vglfr joins (~vglfr@194.9.14.33) |
| 16:24:16 | → | zmt00 joins (~zmt00@user/zmt00) |
| 16:24:43 | → | Inst joins (~Inst@2601:6c4:4080:3f80:59d6:821b:713c:d1d9) |
| 16:25:07 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 16:25:49 | <Inst> | also, re GHC, are there any fundamental issues with say, a language extensions adding ditto marks? i.e, two backticks unseparated indicate an argument that copies the argument on a top-level pattern match above it? |
| 16:25:56 | <Inst> | ex: Fun arg arg2 |
| 16:26:01 | <Inst> | fun `` `` |
| 16:26:38 | <Inst> | what about subcasing? I.e, within a case expression, if I want to say, case x of.... then I can say pure of, then the second of triggers a subcase |
| 16:26:58 | <Inst> | every result within the subcase now has a pure appended to its front |
| 16:27:42 | <Inst> | alternatively, fun of Pattern, everything within the subcase now presumes the pattern as a prefix |
| 16:27:57 | <Inst> | i guess it's very imperative, i.e, got a problem, add syntax |
| 16:29:10 | → | acidjnk joins (~acidjnk@p200300d6e705869994ba3201910e432a.dip0.t-ipconnect.de) |
| 16:36:13 | → | ghn1 joins (~Thunderbi@2603-6081-4900-4100-5031-9898-5d51-6f66.res6.spectrum.com) |
| 16:36:42 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 16:39:47 | × | ghn quits (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 16:39:48 | ghn1 | is now known as ghn |
| 16:42:32 | × | MajorBiscuit quits (~MajorBisc@c-001-031-013.client.tudelft.eduvpn.nl) (Ping timeout: 245 seconds) |
| 16:43:37 | × | benin0 quits (~benin@183.82.25.146) (Ping timeout: 268 seconds) |
| 16:44:04 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 16:44:29 | → | titibandit joins (~titibandi@xdsl-78-35-214-18.nc.de) |
| 16:54:26 | × | titibandit quits (~titibandi@xdsl-78-35-214-18.nc.de) (Quit: Leaving.) |
| 16:55:30 | × | obabo quits (~obabo@2E8BF8F7.catv.pool.telekom.hu) (Quit: WeeChat 3.6) |
| 17:00:39 | × | caubert_ quits (~caubert@user/caubert) (Quit: WeeChat 3.5) |
| 17:00:48 | → | caubert joins (~caubert@user/caubert) |
| 17:02:25 | <geekosaur[m]> | It's what everyone else seems to do (see MultiWayIf) |
| 17:03:47 | → | surgeon joins (~surge9nma@2001:470:69fc:105::f585) |
| 17:04:45 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 17:04:58 | → | nate4 joins (~nate@98.45.169.16) |
| 17:05:59 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 17:08:05 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:09:26 | × | nate4 quits (~nate@98.45.169.16) (Ping timeout: 240 seconds) |
| 17:09:30 | × | euandreh quits (~euandreh@179.214.113.107) (Quit: WeeChat 3.6) |
| 17:10:41 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 17:12:32 | <geekosaur> | or RecordDotSyntax which I personally think was a mistake |
| 17:19:21 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 17:23:47 | × | merijn quits (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
| 17:30:38 | × | Ram-Z quits (~Ram-Z@li1814-254.members.linode.com) (Ping timeout: 268 seconds) |
| 17:30:59 | → | AlexNoo_ joins (~AlexNoo@94.233.241.233) |
| 17:32:32 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 17:32:38 | × | AlexZenon quits (~alzenon@178.34.150.131) (Ping timeout: 240 seconds) |
| 17:34:38 | × | Alex_test quits (~al_test@178.34.150.131) (Ping timeout: 240 seconds) |
| 17:34:57 | × | AlexNoo quits (~AlexNoo@178.34.150.131) (Ping timeout: 268 seconds) |
| 17:35:27 | → | benin0 joins (~benin@2401:4900:2323:8106:8928:2ec0:5649:e0a1) |
| 17:36:20 | AlexNoo_ | is now known as AlexNoo |
| 17:36:30 | → | AlexZenon joins (~alzenon@94.233.241.233) |
| 17:38:33 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:39:10 | × | vglfr quits (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 17:39:35 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 17:39:52 | → | Alex_test joins (~al_test@94.233.241.233) |
| 17:40:46 | × | benin0 quits (~benin@2401:4900:2323:8106:8928:2ec0:5649:e0a1) (Quit: The Lounge - https://thelounge.chat) |
| 17:41:16 | → | titibandit joins (~titibandi@xdsl-78-35-214-18.nc.de) |
| 17:42:51 | × | mbuf quits (~Shakthi@122.165.55.71) (Quit: Leaving) |
| 17:43:22 | → | shriekingnoise joins (~shrieking@186.137.167.202) |
| 17:43:52 | × | byorgey quits (~byorgey@155.138.238.211) (Remote host closed the connection) |
| 17:48:51 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 17:48:51 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 17:48:51 | → | wroathe joins (~wroathe@user/wroathe) |
| 17:48:51 | → | zero joins (~z@user/zero) |
| 17:49:23 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 17:49:47 | zero | is now known as yin |
| 17:49:51 | × | fserucas_ quits (~fserucas@83.223.235.72) (Quit: Leaving) |
| 17:50:56 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 17:57:35 | × | stefan-_ quits (~cri@42dots.de) (Ping timeout: 260 seconds) |
| 17:58:50 | × | noteness quits (~noteness@user/noteness) (Remote host closed the connection) |
| 17:59:48 | → | noteness joins (~noteness@user/noteness) |
| 18:02:57 | → | Ram-Z joins (~Ram-Z@li1814-254.members.linode.com) |
| 18:05:02 | → | stefan-_ joins (~cri@42dots.de) |
| 18:05:26 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 18:05:51 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 18:06:02 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 18:06:02 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 18:06:02 | × | noteness quits (~noteness@user/noteness) (Write error: Broken pipe) |
| 18:06:02 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 18:06:02 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 18:06:24 | → | noteness joins (~noteness@user/noteness) |
| 18:06:33 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 18:06:37 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 18:06:45 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 18:06:49 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 18:06:52 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 18:07:06 | Lord_of_Life_ | is now known as Lord_of_Life |
| 18:10:32 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 255 seconds) |
| 18:10:33 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 18:10:52 | × | noteness quits (~noteness@user/noteness) (Remote host closed the connection) |
| 18:11:16 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 18:11:38 | → | noteness joins (~noteness@user/noteness) |
| 18:13:25 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 18:17:10 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 18:18:37 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:20:26 | × | Kaiepi quits (~Kaiepi@156.34.47.253) (Ping timeout: 268 seconds) |
| 18:21:08 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 18:21:16 | × | coot quits (~coot@213.134.176.158) (Quit: coot) |
| 18:21:40 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 18:22:47 | → | coot joins (~coot@213.134.176.158) |
| 18:22:47 | × | coot quits (~coot@213.134.176.158) (Remote host closed the connection) |
| 18:22:48 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 18:22:53 | × | arjun_ quits (~arjun@user/arjun) (Remote host closed the connection) |
| 18:23:29 | → | causal joins (~user@50.35.83.177) |
| 18:25:22 | × | merijn quits (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 268 seconds) |
| 18:27:20 | → | Guest55 joins (~Guest55@c-71-198-235-211.hsd1.ca.comcast.net) |
| 18:28:45 | → | econo joins (uid147250@user/econo) |
| 18:30:05 | × | foul_owl quits (~kerry@23.82.194.108) (Ping timeout: 252 seconds) |
| 18:39:57 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 18:41:05 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:42:23 | × | Cale quits (~cale@cpef48e38ee8583-cm30b7d4b3fc20.cpe.net.cable.rogers.com) (Read error: Connection reset by peer) |
| 18:42:37 | → | Cale joins (~cale@cpef48e38ee8583-cm30b7d4b3fc20.cpe.net.cable.rogers.com) |
| 18:43:42 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 18:48:53 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 268 seconds) |
| 18:49:16 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 18:49:56 | <qrpnxz> | i don't know why multiwayif exists |
| 18:50:12 | <qrpnxz> | is it cheaper than case () of? |
| 18:50:21 | <Cale> | no |
| 18:50:32 | <geekosaur> | no, and iirc it's just sugar for that |
| 18:51:07 | <qrpnxz> | well actually, if you use that other if extension dothenifmorewordsoup, then the advantage is you can remove nesting probably |
| 18:51:22 | <qrpnxz> | otherwise case will do |
| 18:51:30 | <Cale> | which one? |
| 18:51:35 | <qrpnxz> | let me look |
| 18:51:53 | <qrpnxz> | DoAndIfThenElse |
| 18:52:13 | <Cale> | oh, that just... that one is gross, and turned on by default, but useless |
| 18:52:59 | <qrpnxz> | very useful to me, i was confused as hell when i compiled something and it wasn't implicit |
| 18:53:06 | <Cale> | It lets you put semicolons in the middle of your if expressions so that if you happened to indent them incorrectly inside a do-block, you won't get bitten for it |
| 18:53:20 | <Cale> | If you indent them like: |
| 18:53:23 | <Cale> | if condition |
| 18:53:26 | <Cale> | then foo |
| 18:53:29 | <Cale> | else bar |
| 18:53:33 | <Cale> | then you don't need it |
| 18:53:39 | <Cale> | and also your code is nicer |
| 18:54:29 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 18:54:30 | <qrpnxz> | yeah, i legit had to guess that, but see that adds nesting, sometimes you want nesting, sometimes you don't. By removing the nesting i can write neat if cond then return _ else do |
| 18:54:39 | <qrpnxz> | and then keep at the same nest level |
| 18:54:50 | <Cale> | terrible :) |
| 18:55:10 | <qrpnxz> | not terrible, that's rather common in imperative code |
| 18:55:14 | <Cale> | They do that kind of thing in the GHC source code in various places, and it actually makes things hard to read |
| 18:55:30 | <Cale> | Knowing that there's an early exit is important. |
| 18:56:10 | <Cale> | Being able to visually tell that by looking at indentation is good, but once you start breaking that expectation, you have to scrutinize every do-block carefully |
| 18:57:00 | <Cale> | Like, in a long function, I might not know that I'm in one branch of a conditional, and be trying to add behaviour that applies all the time |
| 18:57:47 | <qrpnxz> | i think i get what you are getting at. Because in haskell return doesn't actually shortcut (indeed that then part may not even *say* return, it's just a monad expression), then the hint that it was returning is the "else do" bit rather than a "return" keyword |
| 18:58:16 | <geekosaur> | yep, but that just makes it doubly confusing |
| 18:58:26 | <qrpnxz> | but for me this is a minor difference. Different languages are different |
| 18:58:31 | <Cale> | Yeah, because nothing otherwise can break out of a do-block before the end apart from an exception |
| 18:58:48 | <geekosaur> | I agree with Cale, I want to see that the else leg is actually under a conditional |
| 18:59:02 | <geekosaur> | and indentation would tell me that |
| 18:59:04 | <Cale> | (or calling the function that callCC handed you, if you're in ContT or something, but you never are) |
| 18:59:12 | × | merijn quits (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
| 18:59:45 | <Cale> | You get used to being able to see do-blocks as things that usually run to completion. |
| 18:59:49 | <qrpnxz> | yeah in callCC then you can do `when cond (k _)` |
| 19:02:59 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 19:06:09 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:07:39 | × | _xor quits (~xor@74.215.182.83) (Quit: WeeChat 3.0) |
| 19:08:41 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 19:09:06 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 19:09:44 | → | kenran joins (~kenran@200116b82be9c900b06c95caadc7b21a.dip.versatel-1u1.de) |
| 19:09:47 | → | sandy_doo joins (~sandydoo@146.70.117.210) |
| 19:12:21 | × | kenran quits (~kenran@200116b82be9c900b06c95caadc7b21a.dip.versatel-1u1.de) (Client Quit) |
| 19:23:25 | <qrpnxz> | i was thinking of how do i make a type of optic that will let me do effects as i traverse, and i just realized that profunctor optics already allow that!! |
| 19:26:05 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 19:26:44 | → | ghn1 joins (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) |
| 19:27:16 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:28:07 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 19:28:50 | × | ghn quits (~Thunderbi@2603-6081-4900-4100-5031-9898-5d51-6f66.res6.spectrum.com) (Ping timeout: 255 seconds) |
| 19:28:55 | ghn1 | is now known as ghn |
| 19:30:33 | → | vglfr joins (~vglfr@194.9.14.33) |
| 19:31:59 | <qrpnxz> | or maybe van laarhoven would have suffised for what i just tested with. I'm trying to work with mutable containers in a lensy way but it's not super great. I can make something like `(a -> ST s a) -> c -> ST s c`, which is useful, but i want to do other effects as i traverse, so i thought of doing something like it's polymorphic on the transformer `forall t. (MonadTrans t) => (a -> t (ST s) a) -> |
| 19:32:01 | <qrpnxz> | c -> t (ST s) c` and that's pretty neat. Bit limited though because the last param can't be phantom, sinse `t m` is a Monad, so really maybe the optimal would be something that's an "Applicative transformer", but would that not just be: `forall f. Applicative f => (a -> Compose f (ST s) a) -> c -> Compose f (ST s) c`? that could work |
| 19:32:21 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 19:35:03 | × | vglfr quits (~vglfr@194.9.14.33) (Ping timeout: 268 seconds) |
| 19:35:55 | → | ghn1 joins (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) |
| 19:36:16 | → | vglfr joins (~vglfr@194.9.14.33) |
| 19:37:07 | × | ghn1 quits (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) (Client Quit) |
| 19:37:31 | × | ghn quits (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 19:37:46 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:38:29 | → | ghn joins (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) |
| 19:39:25 | → | coot joins (~coot@213.134.176.158) |
| 19:44:31 | × | coot quits (~coot@213.134.176.158) (Ping timeout: 252 seconds) |
| 19:45:42 | <qrpnxz> | or actually i'm stuck in monad land because i need to pass the value from the editor to the write action. Hell, even just to pass the value from read to the editor i need bind I think. Switching order to Compose (ST s) f may be more workable |
| 19:46:39 | <qrpnxz> | and actually that makes more sense, because the effect is on the value in the context of ST, not on the ST context itself |
| 19:48:42 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 19:50:32 | → | ghn1 joins (~Thunderbi@2603-6081-4900-4100-a593-ff41-38de-2384.res6.spectrum.com) |
| 19:50:51 | → | azimut_ joins (~azimut@gateway/tor-sasl/azimut) |
| 19:51:10 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 268 seconds) |
| 19:53:01 | × | ghn quits (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 19:53:02 | ghn1 | is now known as ghn |
| 20:01:32 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 20:01:44 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 20:03:05 | → | coot joins (~coot@213.134.176.158) |
| 20:04:49 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 20:05:56 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 20:07:24 | → | Kaiepi joins (~Kaiepi@156.34.47.253) |
| 20:09:17 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 20:13:37 | × | FragByte quits (~christian@user/fragbyte) (Quit: Quit) |
| 20:13:47 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 245 seconds) |
| 20:15:48 | → | FragByte joins (~christian@user/fragbyte) |
| 20:17:07 | × | sandy_doo quits (~sandydoo@146.70.117.210) (Ping timeout: 245 seconds) |
| 20:18:28 | → | zeenk joins (~zeenk@2a02:2f04:a311:2d00:6865:d863:4c93:799f) |
| 20:19:04 | → | pavonia joins (~user@user/siracusa) |
| 20:23:02 | <qrpnxz> | ah! if i create a new array in the process, then i get an honest to goodness traversal, with the only difference being that instead of taking an editor in (->) and returning one in (->), i take one in (Kleisli m) and return another one in (Kleisli m). So for example I can do `(a -> ST s (f b)) -> STArray i a -> ST s (f (Array i b))` :) |
| 20:26:01 | → | MajorBiscuit joins (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) |
| 20:26:11 | → | johnw joins (~johnw@2600:1700:cf00:db0:4977:125:61ab:9934) |
| 20:28:29 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:29:07 | → | jmd_ joins (~jmdaemon@user/jmdaemon) |
| 20:29:30 | <johnw> | is there a Haskell library that, via template Haskell or some such, can transform an ADT into its type of one-hole contexts? I.e., create the derivative of a data type? |
| 20:29:59 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 252 seconds) |
| 20:30:00 | <qrpnxz> | idk, but you can zip any structure you have a traversal to with https://hackage.haskell.org/package/zippers |
| 20:30:18 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 20:30:41 | <qrpnxz> | see also https://hackage.haskell.org/package/lens-5.1.1/docs/Control-Lens-Plated.html and https://hackage.haskell.org/package/lens-5.1.1/docs/Control-Lens-Traversal.html#g:4 |
| 20:31:08 | <qrpnxz> | johnw |
| 20:32:13 | → | stiell joins (~stiell@gateway/tor-sasl/stiell) |
| 20:32:31 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 20:34:59 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 20:36:11 | × | titibandit quits (~titibandi@xdsl-78-35-214-18.nc.de) (Remote host closed the connection) |
| 20:40:00 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:41:36 | × | talismanick quits (~talismani@2601:200:c100:3850::dd64) (Ping timeout: 244 seconds) |
| 20:44:14 | × | zer0bitz quits (~zer0bitz@2001:2003:f748:2000:f402:7db0:5697:8cad) (Ping timeout: 240 seconds) |
| 20:48:22 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 20:49:27 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:50:18 | → | Milan joins (~Milan@46.245.118.112) |
| 20:51:25 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 244 seconds) |
| 20:53:52 | <EvanR_> | johnw, that sounds like automatic differentiation, going just by the title |
| 20:55:04 | <geekosaur> | different kind of differentiation, I think |
| 20:55:28 | <geekosaur> | AD is value level, one-hole contexts is type level? |
| 20:55:52 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 20:56:17 | → | Tuplanolla joins (~Tuplanoll@91-159-69-231.elisa-laajakaista.fi) |
| 20:56:44 | <EvanR_> | man that might explain why I never got differentiation xD |
| 20:57:09 | EvanR_ | is now known as EvanR |
| 21:00:52 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:02:22 | → | Pickchea joins (~private@user/pickchea) |
| 21:06:28 | → | nate4 joins (~nate@98.45.169.16) |
| 21:07:26 | × | MajorBiscuit quits (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) (Ping timeout: 244 seconds) |
| 21:07:33 | × | ubert quits (~Thunderbi@77.119.221.71.wireless.dyn.drei.com) (Ping timeout: 268 seconds) |
| 21:07:53 | → | MajorBiscuit joins (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) |
| 21:11:25 | × | nate4 quits (~nate@98.45.169.16) (Ping timeout: 252 seconds) |
| 21:14:38 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:17:50 | × | MajorBiscuit quits (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) (Ping timeout: 240 seconds) |
| 21:18:19 | → | jero98772 joins (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) |
| 21:18:57 | → | phma_ joins (~phma@host-67-44-208-30.hnremote.net) |
| 21:19:45 | × | phma quits (phma@2001:5b0:211b:ae28:2ee:ca83:26d:80f2) (Read error: Connection reset by peer) |
| 21:19:51 | <johnw> | the reason I'm wondering about this is because yesterday, I wanted the dual of a lens: a diffuser |
| 21:20:02 | <johnw> | dual in a different sense than lens/prism |
| 21:21:18 | <johnw> | if a Lens' s a is a "focus" into some structure 's' that lets you work with 'a', a Diffuser' s a is an "abstraction" from some structure 's' to its one-hole contexts around 'a'. Why would I want this? Because if I had a diffuser 'diff', I could do `x ^. diff == y ^. diff`, and be able to know very easily whether everything *but* the value at 'a' is equal. |
| 21:23:54 | <geekosaur> | that almost sounds like a comonadic lens |
| 21:23:55 | → | MajorBiscuit joins (~MajorBisc@86-88-79-148.fixed.kpn.net) |
| 21:24:04 | <johnw> | actually, it really does |
| 21:24:10 | <geekosaur> | and I note Control.Lens.Internal.Context appears to support that |
| 21:25:13 | × | coot quits (~coot@213.134.176.158) (Quit: coot) |
| 21:28:38 | × | merijn quits (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 21:30:05 | <johnw> | a Context gets very close, but it doesn't yield the one-hole context that might actually be comparable. Instead, it encodes a functional variant of the one-hole context in the form of (a -> s) |
| 21:30:32 | <johnw> | I suppose if I have an 'a' in hand, I can just use it on the two contexts and then compare |
| 21:30:48 | <johnw> | but that doesn't work in cases where 'a' is incomparable but the rest of the context is |
| 21:31:18 | → | Etxeberrialex[m] joins (~etxeberri@2001:470:69fc:105::1:5ae6) |
| 21:31:30 | ← | Etxeberrialex[m] parts (~etxeberri@2001:470:69fc:105::1:5ae6) () |
| 21:32:30 | phma_ | is now known as phma |
| 21:32:45 | × | Inst quits (~Inst@2601:6c4:4080:3f80:59d6:821b:713c:d1d9) (Ping timeout: 244 seconds) |
| 21:35:51 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:43:50 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Write error: Connection reset by peer) |
| 21:43:50 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Write error: Broken pipe) |
| 21:43:50 | × | noteness quits (~noteness@user/noteness) (Read error: Connection reset by peer) |
| 21:43:50 | × | azimut_ quits (~azimut@gateway/tor-sasl/azimut) (Read error: Connection reset by peer) |
| 21:43:50 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Read error: Connection reset by peer) |
| 21:44:10 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 21:44:14 | → | noteness joins (~noteness@user/noteness) |
| 21:44:27 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 21:44:27 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 21:44:32 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 21:45:56 | × | MajorBiscuit quits (~MajorBisc@86-88-79-148.fixed.kpn.net) (Ping timeout: 268 seconds) |
| 21:47:44 | → | MajorBiscuit joins (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) |
| 21:57:53 | → | morrow joins (~user@bzq-110-168-31-106.red.bezeqint.net) |
| 22:01:21 | × | MajorBiscuit quits (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) (Ping timeout: 268 seconds) |
| 22:01:23 | × | acidjnk quits (~acidjnk@p200300d6e705869994ba3201910e432a.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 22:07:22 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 244 seconds) |
| 22:09:25 | → | foul_owl joins (~kerry@174-21-65-36.tukw.qwest.net) |
| 22:10:53 | → | zmt00 joins (~zmt00@user/zmt00) |
| 22:16:18 | → | talismanick joins (~talismani@96.71.204.25) |
| 22:26:01 | × | foul_owl quits (~kerry@174-21-65-36.tukw.qwest.net) (Ping timeout: 268 seconds) |
| 22:39:39 | → | foul_owl joins (~kerry@23.82.194.107) |
| 22:41:26 | × | xff0x quits (~xff0x@2405:6580:b080:900:13b:63d1:e32e:fe38) (Ping timeout: 255 seconds) |
| 22:41:42 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 22:47:53 | × | Milan quits (~Milan@46.245.118.112) (Quit: Client closed) |
| 22:56:39 | × | talismanick quits (~talismani@96.71.204.25) (Ping timeout: 252 seconds) |
| 23:01:06 | × | zeenk quits (~zeenk@2a02:2f04:a311:2d00:6865:d863:4c93:799f) (Quit: Konversation terminated!) |
| 23:04:30 | → | xff0x joins (~xff0x@2405:6580:b080:900:f3e0:1e7d:c792:ccbd) |
| 23:05:35 | × | Tuplanolla quits (~Tuplanoll@91-159-69-231.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:07:02 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 23:15:40 | × | dispater quits (~dispater@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in) |
| 23:15:59 | → | dispater joins (~dispater@user/brprice) |
| 23:16:34 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 23:17:16 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 23:17:47 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 23:18:22 | × | Nahra quits (~user@static.161.95.99.88.clients.your-server.de) (Remote host closed the connection) |
| 23:20:03 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 23:20:20 | → | gentauro joins (~gentauro@user/gentauro) |
| 23:21:02 | × | matthewmosior quits (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 23:21:47 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 23:21:57 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 23:22:12 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 23:25:54 | → | merijn joins (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 23:27:58 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Ping timeout: 244 seconds) |
| 23:28:48 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 23:28:48 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 23:28:48 | → | wroathe joins (~wroathe@user/wroathe) |
| 23:34:15 | × | morrow quits (~user@bzq-110-168-31-106.red.bezeqint.net) (Quit: leaving) |
| 23:38:05 | → | talismanick joins (~talismani@96.71.204.25) |
| 23:38:12 | × | talismanick quits (~talismani@96.71.204.25) (Remote host closed the connection) |
| 23:38:43 | → | matthewmosior joins (~matthewmo@173.170.253.91) |
| 23:48:06 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Quit: ZNC - https://znc.in) |
| 23:48:24 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
All times are in UTC on 2022-08-04.