Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 415 416 417 418 419 420 421 422 423 424 425 .. 5022
502,152 events total
2020-10-04 23:49:59 xerox_ joins (~xerox@unaffiliated/xerox)
2020-10-04 23:50:37 leapingfrogs joins (~leapingfr@host86-136-28-78.range86-136.btcentralplus.com)
2020-10-04 23:51:50 × wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 256 seconds)
2020-10-04 23:51:55 conal joins (~conal@209.58.132.107)
2020-10-04 23:52:46 × GyroW quits (~GyroW@unaffiliated/gyrow) (Quit: Someone ate my pie)
2020-10-04 23:53:00 GyroW joins (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be)
2020-10-04 23:53:00 × GyroW quits (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be) (Changing host)
2020-10-04 23:53:00 GyroW joins (~GyroW@unaffiliated/gyrow)
2020-10-04 23:55:21 × alp quits (~alp@2a01:e0a:58b:4920:f043:ba1b:f5d1:917) (Ping timeout: 272 seconds)
2020-10-04 23:55:54 × leapingfrogs quits (~leapingfr@host86-136-28-78.range86-136.btcentralplus.com) (Ping timeout: 265 seconds)
2020-10-04 23:56:45 × motte quits (~weechat@unaffiliated/motte) (Ping timeout: 240 seconds)
2020-10-04 23:57:29 wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-10-04 23:57:30 × brettgilio quits (~brettgili@brettgilio.com) (Quit: Long live IRC! <https://brettgilio.com>)
2020-10-04 23:57:36 mav2 joins (~mav@p5b02806a.dip0.t-ipconnect.de)
2020-10-05 00:00:00 <quintasan> Is there any way I could write a function Hasql.Decoders.Result (Int32, Text) -> Tea where Tea is Tea { id :: Int32, name :: Text }? https://hackage.haskell.org/package/hasql-1.4.4.2/docs/Hasql-Decoders.html here are the docs. If my approach is not the correct one then let me know as well because I'm a beginner
2020-10-05 00:00:02 × Hellaenergy quits (~Hellaener@185.244.214.216) ()
2020-10-05 00:00:10 × atk quits (~Arch-TK@ircpuzzles/staff/Arch-TK) (Quit: Well this is unexpected.)
2020-10-05 00:00:30 atk joins (~Arch-TK@ircpuzzles/staff/Arch-TK)
2020-10-05 00:02:08 brettgilio joins (~brettgili@brettgilio.com)
2020-10-05 00:04:25 × mav2 quits (~mav@p5b02806a.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2020-10-05 00:04:54 × sep2 quits (49dc4892@c-73-220-72-146.hsd1.ca.comcast.net) (Remote host closed the connection)
2020-10-05 00:04:55 × DavidEichmann quits (~david@43.240.198.146.dyn.plus.net) (Ping timeout: 240 seconds)
2020-10-05 00:05:01 nineonine joins (~nineonine@216-19-190-182.dyn.novuscom.net)
2020-10-05 00:05:26 alp joins (~alp@2a01:e0a:58b:4920:d122:6c79:ff7:b4e4)
2020-10-05 00:06:01 nineonin_ joins (~nineonine@50.216.62.2)
2020-10-05 00:09:29 × nineonine quits (~nineonine@216-19-190-182.dyn.novuscom.net) (Ping timeout: 260 seconds)
2020-10-05 00:12:24 × nineonin_ quits (~nineonine@50.216.62.2) (Ping timeout: 258 seconds)
2020-10-05 00:13:12 × pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Ping timeout: 272 seconds)
2020-10-05 00:14:21 pfurla joins (~pfurla@64.145.79.141)
2020-10-05 00:18:08 × seanvert quits (~user@177.84.244.242) (Read error: Connection reset by peer)
2020-10-05 00:19:30 nineonine joins (~nineonine@50.216.62.2)
2020-10-05 00:20:01 seanvert joins (~user@177.84.244.242)
2020-10-05 00:23:27 hackage crc 0.1.1.0 - Implements various Cyclic Redundancy Checks (CRC) https://hackage.haskell.org/package/crc-0.1.1.0 (MichaelXavier)
2020-10-05 00:24:27 × emmanuel_erc quits (~user@2604:2000:1382:ce03:88f9:ad61:775c:c25) (Ping timeout: 240 seconds)
2020-10-05 00:25:24 snakemasterflex joins (~snakemast@213.100.206.23)
2020-10-05 00:25:27 hackage crc 0.1.1.1 - Implements various Cyclic Redundancy Checks (CRC) https://hackage.haskell.org/package/crc-0.1.1.1 (MichaelXavier)
2020-10-05 00:25:49 × nineonine quits (~nineonine@50.216.62.2) (Ping timeout: 258 seconds)
2020-10-05 00:27:39 × alp quits (~alp@2a01:e0a:58b:4920:d122:6c79:ff7:b4e4) (Ping timeout: 272 seconds)
2020-10-05 00:28:29 × seanvert quits (~user@177.84.244.242) (Read error: Connection reset by peer)
2020-10-05 00:29:14 × ahmr88 quits (~ahmr88@cpc85006-haye22-2-0-cust131.17-4.cable.virginm.net) (Remote host closed the connection)
2020-10-05 00:29:55 × snakemasterflex quits (~snakemast@213.100.206.23) (Ping timeout: 240 seconds)
2020-10-05 00:33:23 emmanuel_erc joins (~user@2604:2000:1382:ce03:88f9:ad61:775c:c25)
2020-10-05 00:34:11 × Wuzzy quits (~Wuzzy@p5790e6f5.dip0.t-ipconnect.de) (Remote host closed the connection)
2020-10-05 00:34:13 <JohnTalent> sounds like a honeypot.
2020-10-05 00:34:23 <sm[m]> JohnTalent: also yesod, IHP, maybe clckwrks
2020-10-05 00:34:42 <JohnTalent> sm[m]: yeah, that makes perfect sense in english.
2020-10-05 00:34:44 × elliott__ quits (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) (Ping timeout: 272 seconds)
2020-10-05 00:34:56 × cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Quit: leaving)
2020-10-05 00:35:00 <sm[m]> nobody uses clckwrks but it keeps on ticking, maybe it's good!
2020-10-05 00:35:35 seanvert joins (~user@177.84.244.242)
2020-10-05 00:36:33 polyrain joins (~polyrain@2001:8003:e501:6901:5451:58df:dd7d:42b9)
2020-10-05 00:38:54 × mathlover2 quits (~mathlover@2604:6000:1013:129e:c3f:af24:28bd:eee4) (Quit: Leaving)
2020-10-05 00:39:20 × seanvert quits (~user@177.84.244.242) (Read error: Connection reset by peer)
2020-10-05 00:40:26 × pfurla quits (~pfurla@64.145.79.141) (Ping timeout: 272 seconds)
2020-10-05 00:41:33 pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net)
2020-10-05 00:45:36 <jackdk> quintasan: The key is that the `Result` type has a `Functor` instance. This means you can `fmap` over it. Let me prepare a snippet
2020-10-05 00:49:09 × raehik quits (~raehik@cpc96984-rdng25-2-0-cust109.15-3.cable.virginm.net) (Ping timeout: 260 seconds)
2020-10-05 00:50:37 <jackdk> quintasan: Here are some examples that may clear things up: https://www.irccloud.com/pastebin/RNBBmdUn/Tea.hs
2020-10-05 00:51:16 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2020-10-05 00:56:06 torax joins (~torax@185.163.110.116)
2020-10-05 00:57:19 plutoniix joins (~q@ppp-223-24-188-55.revip6.asianet.co.th)
2020-10-05 00:58:38 <quintasan> jackdk: This still gives me Result Tea which... not exactly what I wanted. Hasql uses some weird (to me of course) idea of Encoders and Decoders and I wanted to write a decoder once and reuse it multiple times but it seems that my approach is either incorrect or I'm not good enough
2020-10-05 00:58:39 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:c50d:40d9:7a86:602b) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-05 00:58:58 <jackdk> quintasan: Oh I must've misread you sorry
2020-10-05 00:59:01 <quintasan> And I'm still having problems with Text vs. [Char]
2020-10-05 00:59:59 <ski> jackdk : nitpick, that's using function extensionality, not eta-reduction
2020-10-05 01:00:06 <quintasan> jackdk: No worries, I'm trying to build a web application in Haskell coming from Rails so it's kind of frustrating when I can't do simple stuff like writing things to database and getting hashes back
2020-10-05 01:00:25 <jackdk> ski: thank you
2020-10-05 01:00:44 × Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 256 seconds)
2020-10-05 01:00:47 <ski> function extensionality says that if `f x = g x' for every `x', then `f = g'
2020-10-05 01:01:25 <jackdk> makes sense, cheers
2020-10-05 01:01:41 <ski> eta-conversion says that `\x -> (...) x' (where `x' doesn't occur (freely) in `...') is equal to `...'. (forward direction is eta-reduction, backward is eta-expansion)
2020-10-05 01:01:43 wei2912 joins (~wei2912@unaffiliated/wei2912)
2020-10-05 01:01:58 <ski> they're closely related, though. you can prove they're equivalent
2020-10-05 01:03:59 <dolio> Sometimes.
2020-10-05 01:04:00 <ski> (you could try to prove this, if you want to. it's not terribly complicated. you'll need to know beta-conversion, though, that `(\x -> <body>) <argument>' is equal to `<body>' with all (free) occurances of `x' replaced by `<argument>')
2020-10-05 01:04:03 × plutoniix quits (~q@ppp-223-24-188-55.revip6.asianet.co.th) (Ping timeout: 260 seconds)
2020-10-05 01:04:42 × ddellacosta quits (~dd@86.106.121.168) (Ping timeout: 256 seconds)
2020-10-05 01:05:28 <ski> mm .. i suppose it depends on what ambient theory one has
2020-10-05 01:05:39 <jackdk> quintasan: looking at the examples in https://github.com/nikita-volkov/hasql , it looks like Result is passed to the constructor of Statement, and you run Statements using Hasql.Session.statement
2020-10-05 01:05:47 <ski> (one'll need some version of congruence as well, i think)
2020-10-05 01:06:10 <jackdk> quintasan: then you use Hasql.Session.run to turn a (Session a) and a Connection into IO (Either QueryError a)
2020-10-05 01:07:08 <dolio> Yeah. For instance, Agda's "propositional equality" admits eta, but not extensionality.
2020-10-05 01:07:10 <jackdk> quintasan: the bottom of the readme on github talks about a hasql-th lib that automatically generates the Statement for you from the SQL string, so that might be a little easier
2020-10-05 01:07:47 <dolio> At least in the normal mode.
2020-10-05 01:08:08 × conal quits (~conal@209.58.132.107) (Quit: Computer has gone to sleep.)
2020-10-05 01:08:45 heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-10-05 01:14:10 <ski> dolio : hm, so one can't formalize `f = \x -> f x = \x -> g x = g', then ?
2020-10-05 01:14:54 × polyrain quits (~polyrain@2001:8003:e501:6901:5451:58df:dd7d:42b9) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-05 01:15:38 <dolio> There's no way to apply the extensionality hypothesis for the middle step.
2020-10-05 01:16:40 <dolio> You basically want to apply both sides to an abstract variable, but there's no way to do that.
2020-10-05 01:16:52 plutoniix joins (~q@175.176.222.7)
2020-10-05 01:17:01 × irc_user quits (uid423822@gateway/web/irccloud.com/x-jgthhmutdxudiomv) (Quit: Connection closed for inactivity)
2020-10-05 01:18:32 <ski> mhm, i see. so it's the congruence step that's problematic
2020-10-05 01:18:38 <dolio> Yeah.
2020-10-05 01:19:25 <dolio> Congruence holds judgmentally, but has no propositional equivalent.
2020-10-05 01:19:34 <ski> is this related to decidability of type-checking ? intensional vs. extensional type theory ?
2020-10-05 01:19:43 <dolio> The way to write it propositionally is basically extensionality.
2020-10-05 01:19:52 <ski> (i don't think i understand the latter distinction that well)
2020-10-05 01:20:15 <dolio> Or, it's extensionality up to eta.

All times are in UTC.