Logs: freenode/#haskell
| 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.