Logs on 2020-11-18 (freenode/#haskell)
| 00:00:01 | × | havenwood1 quits (~havenwood@185.204.1.185) () |
| 00:00:36 | × | nut quits (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 00:00:58 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 00:01:06 | × | juri_ quits (~juri@178.63.35.222) (Ping timeout: 272 seconds) |
| 00:01:10 | <unclechu> | currently i have define a type family and another type family which is a multiple version of first one |
| 00:02:04 | → | jedws joins (~jedws@101.184.175.183) |
| 00:02:41 | → | juri_ joins (~juri@178.63.35.222) |
| 00:02:45 | × | peutri quits (~peutri@ns317027.ip-94-23-46.eu) (Ping timeout: 240 seconds) |
| 00:02:52 | → | peutri joins (~peutri@ns317027.ip-94-23-46.eu) |
| 00:02:54 | <unclechu> | like `type family FooMultiple (a ∷ [κ]) ∷ [b] where FooMultiple '[] = '[]; FooMultiple (x ': xs) = Foo x ': FooMultiple xs` |
| 00:03:14 | → | jzl joins (~jzl@ip238.ip-149-56-250.net) |
| 00:03:14 | × | jzl quits (~jzl@ip238.ip-149-56-250.net) (Changing host) |
| 00:03:14 | → | jzl joins (~jzl@unaffiliated/jzl) |
| 00:03:52 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:94c2:72b2:8a99:7096) (Ping timeout: 260 seconds) |
| 00:04:12 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Ping timeout: 260 seconds) |
| 00:04:31 | → | cosimone joins (~cosimone@5.171.25.59) |
| 00:06:15 | × | ben_m quits (~ben_m@unaffiliated/ben-m/x-8385872) (Quit: ZNC 1.7.5 - https://znc.in) |
| 00:06:34 | → | ben_m joins (~ben_m@56.ip-51-38-127.eu) |
| 00:06:34 | × | ben_m quits (~ben_m@56.ip-51-38-127.eu) (Changing host) |
| 00:06:34 | → | ben_m joins (~ben_m@unaffiliated/ben-m/x-8385872) |
| 00:07:46 | × | lemald quits (~eddie@capybara.lemald.org) (Ping timeout: 246 seconds) |
| 00:10:04 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Read error: Connection reset by peer) |
| 00:10:10 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 00:14:03 | → | mbomba joins (~mbomba@bras-base-toroon2719w-grc-49-142-114-9-241.dsl.bell.ca) |
| 00:14:09 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 00:15:31 | × | mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Quit: mputz) |
| 00:15:56 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:1bc1:d518:fbf:6e25) |
| 00:20:04 | × | jedws quits (~jedws@101.184.175.183) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 00:21:52 | → | Nolar joins (~Nolar@185.163.110.116) |
| 00:24:38 | → | arw_ joins (~arw@impulse.informatik.uni-erlangen.de) |
| 00:25:07 | → | AWizzArd_ joins (~code@gehrels.uberspace.de) |
| 00:25:07 | → | w2gz joins (~do@159.89.11.133) |
| 00:25:37 | × | w1gz quits (~do@159.89.11.133) (Ping timeout: 260 seconds) |
| 00:25:37 | × | arw quits (~arw@impulse.informatik.uni-erlangen.de) (Ping timeout: 260 seconds) |
| 00:25:37 | × | AWizzArd quits (~code@unaffiliated/awizzard) (Ping timeout: 260 seconds) |
| 00:26:42 | → | mputz joins (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) |
| 00:26:49 | × | dxld quits (~dxld@80-109-136-248.cable.dynamic.surfer.at) (Quit: Bye) |
| 00:28:34 | × | daGrevis quits (~daGrevis@unaffiliated/dagrevis) (Ping timeout: 256 seconds) |
| 00:28:35 | → | dxld joins (~dxld@rush.pub.dxld.at) |
| 00:28:43 | → | daGrevis joins (~daGrevis@unaffiliated/dagrevis) |
| 00:29:07 | × | LKoen quits (~LKoen@9.253.88.92.rev.sfr.net) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 00:29:17 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) |
| 00:31:23 | × | jb55 quits (~jb55@gateway/tor-sasl/jb55) (Ping timeout: 240 seconds) |
| 00:31:48 | → | jb55 joins (~jb55@gateway/tor-sasl/jb55) |
| 00:33:11 | × | mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Quit: mputz) |
| 00:33:45 | → | jedws joins (~jedws@101.184.175.183) |
| 00:34:17 | → | hekkaidekapus_ joins (~tchouri@gateway/tor-sasl/hekkaidekapus) |
| 00:34:41 | × | st8less quits (~st8less@2603:a060:11fd:0:68fe:5aed:dd91:2111) (Quit: WeeChat 2.7.1) |
| 00:34:57 | → | lemald joins (~eddie@capybara.lemald.org) |
| 00:36:03 | × | hekkaidekapus quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 240 seconds) |
| 00:36:55 | → | fendor_ joins (~fendor@77.119.128.218.wireless.dyn.drei.com) |
| 00:37:35 | → | carlomagno joins (~cararell@148.87.23.12) |
| 00:38:37 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:95c1:f982:82e4:2d79) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 00:39:49 | × | fendor quits (~fendor@178.115.128.157.wireless.dyn.drei.com) (Ping timeout: 264 seconds) |
| 00:40:13 | × | alp quits (~alp@2a01:e0a:58b:4920:ac08:1079:c3a9:84b6) (Remote host closed the connection) |
| 00:43:55 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 00:44:11 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 00:44:13 | × | benjamingr__ quits (uid23465@gateway/web/irccloud.com/x-hiupvfuftqbhepbs) (Quit: Connection closed for inactivity) |
| 00:44:41 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 00:44:43 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 00:45:00 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 00:45:19 | × | ph88 quits (~ph88@2a02:8109:9e00:7e5c:bc50:2174:75e6:7e22) (Ping timeout: 272 seconds) |
| 00:45:32 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 00:45:49 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 00:46:18 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:95c1:f982:82e4:2d79) |
| 00:46:20 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 00:46:38 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 00:47:08 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 00:49:31 | hackage | Frames-streamly 0.1.0.1 - A streamly layer for Frames I/O https://hackage.haskell.org/package/Frames-streamly-0.1.0.1 (adamCS) |
| 00:52:29 | × | Aquazi quits (uid312403@gateway/web/irccloud.com/x-fwnbgopbizdwfbcr) (Quit: Connection closed for inactivity) |
| 00:52:29 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Quit: Leaving) |
| 00:53:47 | <koz_> | When GHC describes a type variable as 'rigid', what does it mean exactly? |
| 00:58:22 | <dolio> | koz_: It means it can't be unified with any type but itself, basically. |
| 01:01:25 | × | dcoutts_ quits (~duncan@33.14.75.194.dyn.plus.net) (Ping timeout: 240 seconds) |
| 01:06:15 | × | gentauro quits (~gentauro@unaffiliated/gentauro) (Read error: Connection reset by peer) |
| 01:06:42 | → | gentauro joins (~gentauro@unaffiliated/gentauro) |
| 01:07:40 | × | jedws quits (~jedws@101.184.175.183) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 01:08:10 | × | crdrost quits (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) (Quit: This computer has gone to sleep) |
| 01:09:13 | × | m0rphism quits (~m0rphism@HSI-KBW-095-208-098-207.hsi5.kabel-badenwuerttemberg.de) (Ping timeout: 264 seconds) |
| 01:09:39 | → | jedws joins (~jedws@101.184.175.183) |
| 01:21:28 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 01:21:42 | × | ManiacTwister quits (~Twister@2a01:4f8:171:4de::40:2) (Quit: Servus!) |
| 01:22:02 | × | pjb quits (~t@2a01cb04063ec5006d6abee34943d090.ipv6.abo.wanadoo.fr) (Ping timeout: 260 seconds) |
| 01:22:24 | → | ManiacTwister joins (~Twister@2a01:4f8:171:4de::40:2) |
| 01:22:38 | × | ddellacosta quits (dd@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 260 seconds) |
| 01:23:50 | <koz_> | dolio: Ah. |
| 01:26:30 | <jchia> | Any general guidelines for making Arbitrary instances for my own types especially wrt orphaned instances? |
| 01:27:02 | <dibblego> | newtype or use hedgehog |
| 01:28:12 | × | falafel quits (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) (Ping timeout: 260 seconds) |
| 01:28:13 | → | Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 01:28:15 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:95c1:f982:82e4:2d79) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 01:28:35 | → | Guest_87 joins (b644cd01@182.68.205.1) |
| 01:28:37 | → | conal joins (~conal@64.71.133.70) |
| 01:31:58 | → | Lord_of_Life_ joins (~Lord@46.217.217.18) |
| 01:33:05 | × | Lord_of_Life quits (~Lord@46.217.219.70) (Ping timeout: 240 seconds) |
| 01:33:25 | → | abrar joins (~abrar@static-108-30-103-121.nycmny.fios.verizon.net) |
| 01:34:09 | <koz_> | You can also avoid the need for Arbitrary if you just define 'Gen a' for your stuff, and use combinators like https://hackage.haskell.org/package/QuickCheck-2.14.2/docs/Test-QuickCheck.html#v:forAll |
| 01:34:22 | <koz_> | Or rather, define stuff like 'genFoo :: Gen Foo' and use those. |
| 01:34:45 | <koz_> | It's more tedious though. |
| 01:36:44 | × | Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 272 seconds) |
| 01:40:22 | → | Audentity joins (~Audentity@4e69b241.skybroadband.com) |
| 01:44:07 | → | ddellacosta joins (dd@gateway/vpn/mullvad/ddellacosta) |
| 01:48:52 | × | thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 260 seconds) |
| 01:50:31 | hackage | Frames-streamly 0.1.0.2 - A streamly layer for Frames I/O https://hackage.haskell.org/package/Frames-streamly-0.1.0.2 (adamCS) |
| 01:51:33 | → | drbean joins (~drbean@TC210-63-209-39.static.apol.com.tw) |
| 01:52:27 | <Axman6> | unclechu: ah sorry, I hadn't read all the history |
| 01:54:00 | × | Guest_87 quits (b644cd01@182.68.205.1) (Remote host closed the connection) |
| 01:54:54 | → | dustypacer joins (~pi@2600:6c50:80:2f4a:e9d0:6569:1cea:d1d4) |
| 01:56:21 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 01:57:50 | × | Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 260 seconds) |
| 02:01:09 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 02:01:27 | → | Audentity joins (~Audentity@4e69b241.skybroadband.com) |
| 02:09:23 | × | livvy quits (~livvy@gateway/tor-sasl/livvy) (Ping timeout: 240 seconds) |
| 02:11:43 | → | kotrcka joins (~peter@ip-94-112-194-11.net.upcbroadband.cz) |
| 02:11:47 | × | Entertainment quits (~entertain@104.246.132.210) () |
| 02:13:51 | × | nuncanada quits (~dude@179.235.160.168) (Read error: Connection reset by peer) |
| 02:14:28 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 246 seconds) |
| 02:14:53 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 02:15:07 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 02:20:08 | × | alx741 quits (~alx741@181.196.68.148) (Quit: alx741) |
| 02:21:05 | × | Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 240 seconds) |
| 02:25:02 | → | Audentity joins (~Audentity@4e69b241.skybroadband.com) |
| 02:25:36 | × | solonarv quits (~solonarv@astrasbourg-653-1-156-155.w90-6.abo.wanadoo.fr) (Ping timeout: 240 seconds) |
| 02:26:01 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Ping timeout: 272 seconds) |
| 02:26:18 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 02:30:13 | → | toorevitimirp joins (~tooreviti@117.182.180.118) |
| 02:31:26 | × | ddellacosta quits (dd@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 260 seconds) |
| 02:32:57 | → | guest1118 joins (~user@49.5.6.87) |
| 02:33:15 | × | Deide quits (~Deide@217.155.19.23) (Quit: Seeee yaaaa) |
| 02:34:13 | × | jchia__ quits (~jchia@58.32.37.146) (Quit: Leaving.) |
| 02:34:32 | → | jchia__ joins (~jchia@58.32.37.146) |
| 02:34:47 | × | jchia__ quits (~jchia@58.32.37.146) (Client Quit) |
| 02:34:56 | × | drbean quits (~drbean@TC210-63-209-39.static.apol.com.tw) (Ping timeout: 240 seconds) |
| 02:35:06 | → | jchia__ joins (~jchia@58.32.37.146) |
| 02:35:21 | × | jchia__ quits (~jchia@58.32.37.146) (Client Quit) |
| 02:35:41 | → | jchia__ joins (~jchia@58.32.37.146) |
| 02:35:55 | × | jchia__ quits (~jchia@58.32.37.146) (Client Quit) |
| 02:36:19 | → | jchia__ joins (~jchia@58.32.37.146) |
| 02:36:29 | × | jchia__ quits (~jchia@58.32.37.146) (Client Quit) |
| 02:39:01 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:95c1:f982:82e4:2d79) |
| 02:41:26 | × | xff0x quits (~fox@2001:1a81:52d5:6a00:7dc4:a65f:e69e:5679) (Ping timeout: 264 seconds) |
| 02:43:19 | → | xff0x joins (~fox@2001:1a81:5310:3c00:eddd:290e:8cac:b048) |
| 02:43:56 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Ping timeout: 240 seconds) |
| 02:44:26 | → | Tario joins (~Tario@garza.riseup.net) |
| 02:47:05 | → | wroathe_ joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 02:47:45 | × | jedws quits (~jedws@101.184.175.183) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 02:48:13 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 02:48:39 | → | jedws joins (~jedws@101.184.175.183) |
| 02:49:17 | wroathe_ | is now known as wroathe |
| 02:51:19 | × | Tario quits (~Tario@garza.riseup.net) (Read error: Connection reset by peer) |
| 02:51:29 | → | Tario joins (~Tario@201.192.165.173) |
| 02:53:50 | × | lucasb quits (uid333435@gateway/web/irccloud.com/x-gwvbkmucegxpihno) (Quit: Connection closed for inactivity) |
| 02:54:16 | × | Feuermagier quits (~Feuermagi@213.178.26.41) (Ping timeout: 256 seconds) |
| 02:54:20 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 02:54:49 | × | urdh quits (~urdh@unaffiliated/urdh) (Ping timeout: 264 seconds) |
| 03:00:01 | × | Nolar quits (~Nolar@185.163.110.116) () |
| 03:00:48 | × | jedws quits (~jedws@101.184.175.183) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 03:02:49 | → | Feuermagier joins (~Feuermagi@213.178.26.41) |
| 03:04:12 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 03:06:55 | × | urodna quits (~urodna@unaffiliated/urodna) (Quit: urodna) |
| 03:15:21 | × | bqv quits (~bqv@2a02:8010:674f:0:d65d:64ff:fe52:5efe) (Quit: WeeChat 2.9) |
| 03:17:05 | → | pjb joins (~t@2a01cb04063ec500fcb709f072569e15.ipv6.abo.wanadoo.fr) |
| 03:17:20 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) |
| 03:23:01 | × | zaquest quits (~notzaques@5.128.210.178) (Ping timeout: 264 seconds) |
| 03:32:39 | × | mbomba quits (~mbomba@bras-base-toroon2719w-grc-49-142-114-9-241.dsl.bell.ca) (Quit: WeeChat 3.0) |
| 03:35:01 | × | Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 265 seconds) |
| 03:35:37 | → | zaquest joins (~notzaques@5.128.210.178) |
| 03:35:47 | → | wei2912 joins (~wei2912@unaffiliated/wei2912) |
| 03:37:28 | × | kaeru quits (~kaeru@185.163.110.116) (Remote host closed the connection) |
| 03:38:12 | → | Audentity joins (~Audentity@4e69b241.skybroadband.com) |
| 03:43:37 | → | jedws joins (~jedws@101.184.175.183) |
| 03:46:09 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 03:46:23 | → | Tario joins (~Tario@201.192.165.173) |
| 03:46:30 | × | vacm quits (~vacwm@70.23.92.191) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 03:46:43 | × | lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Killed (hitchcock.freenode.net (Nickname regained by services))) |
| 03:46:51 | → | lagothrix joins (~lagothrix@unaffiliated/lagothrix) |
| 03:50:27 | × | nados quits (~dan@69-165-210-185.cable.teksavvy.com) (Remote host closed the connection) |
| 03:50:49 | → | ystael joins (~ystael@209.6.50.55) |
| 03:50:55 | → | nados joins (~dan@69-165-210-185.cable.teksavvy.com) |
| 03:53:43 | × | theDon quits (~td@muedsl-82-207-238-136.citykom.de) (Ping timeout: 260 seconds) |
| 03:55:12 | → | theDon joins (~td@94.134.91.119) |
| 03:56:42 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 03:59:44 | × | cosimone quits (~cosimone@5.171.25.59) (Quit: cosimone) |
| 04:00:09 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Ping timeout: 256 seconds) |
| 04:00:10 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 246 seconds) |
| 04:00:38 | × | renzhi quits (~renzhi@2607:fa49:655f:e600::28da) (Ping timeout: 264 seconds) |
| 04:00:51 | → | g3762 joins (~g3762@190.84.119.211) |
| 04:00:56 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 04:08:31 | × | johnw quits (~johnw@haskell/developer/johnw) (Read error: Connection reset by peer) |
| 04:08:50 | × | kotrcka quits (~peter@ip-94-112-194-11.net.upcbroadband.cz) (Quit: Konversation terminated!) |
| 04:09:08 | → | johnw joins (~johnw@haskell/developer/johnw) |
| 04:10:26 | × | g3762 quits (~g3762@190.84.119.211) (Quit: Leaving) |
| 04:11:26 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:1bc1:d518:fbf:6e25) (Ping timeout: 264 seconds) |
| 04:11:32 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 04:14:37 | × | Tario quits (~Tario@201.192.165.173) (Ping timeout: 264 seconds) |
| 04:16:27 | → | christo joins (~chris@81.96.113.213) |
| 04:20:45 | × | christo quits (~chris@81.96.113.213) (Ping timeout: 240 seconds) |
| 04:23:12 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:9e:a33:1504:d5f7) |
| 04:28:43 | → | ksamak joins (~ksamak@195.206.169.184) |
| 04:31:36 | → | cads joins (~cads@ip-64-72-99-232.lasvegas.net) |
| 04:31:47 | × | howdoi quits (uid224@gateway/web/irccloud.com/x-hhaciizupxxisicz) (Quit: Connection closed for inactivity) |
| 04:32:43 | × | jb55 quits (~jb55@gateway/tor-sasl/jb55) (Ping timeout: 240 seconds) |
| 04:33:02 | × | acidjnk_new quits (~acidjnk@p200300d0c719ff874cf537f47d61e6af.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 04:34:44 | → | jb55 joins (~jb55@gateway/tor-sasl/jb55) |
| 04:44:12 | × | Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 256 seconds) |
| 04:44:50 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) |
| 04:45:14 | → | Noldorin joins (~noldorin@unaffiliated/noldorin) |
| 04:46:10 | × | Noldorin quits (~noldorin@unaffiliated/noldorin) (Client Quit) |
| 04:48:11 | → | Audentity joins (~Audentity@4e69b241.skybroadband.com) |
| 04:50:34 | × | conal quits (~conal@64.71.133.70) (Read error: Connection reset by peer) |
| 05:00:22 | → | spake joins (~spake@84.39.117.57) |
| 05:01:17 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Remote host closed the connection) |
| 05:01:40 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 05:03:30 | hackage | hyraxAbif 0.2.3.26 - Modules for parsing, generating and manipulating AB1 files. https://hackage.haskell.org/package/hyraxAbif-0.2.3.26 (andrevdm) |
| 05:10:00 | → | plutoniix joins (~q@ppp-27-55-83-124.revip3.asianet.co.th) |
| 05:10:41 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:9e:a33:1504:d5f7) (Ping timeout: 272 seconds) |
| 05:11:30 | hackage | hyraxAbif 0.2.3.27 - Modules for parsing, generating and manipulating AB1 files. https://hackage.haskell.org/package/hyraxAbif-0.2.3.27 (andrevdm) |
| 05:15:13 | logicmoo | is now known as dmiles |
| 05:15:33 | × | texasmynsted quits (~texasmyns@212.102.45.118) (Ping timeout: 265 seconds) |
| 05:15:49 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Ping timeout: 264 seconds) |
| 05:18:15 | → | guest111` joins (~user@49.5.6.87) |
| 05:19:58 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Ping timeout: 246 seconds) |
| 05:20:50 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 05:22:42 | × | guest1118 quits (~user@49.5.6.87) (Ping timeout: 260 seconds) |
| 05:23:01 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:eb39:3323:4fa4:f361) |
| 05:26:00 | → | day_ joins (~Unknown@unaffiliated/day) |
| 05:27:24 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:95c1:f982:82e4:2d79) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 05:29:23 | × | day quits (~Unknown@unaffiliated/day) (Ping timeout: 260 seconds) |
| 05:29:24 | day_ | is now known as day |
| 05:34:31 | → | Sanchayan joins (~Sanchayan@106.201.35.233) |
| 05:43:45 | → | falafel joins (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) |
| 05:46:00 | × | guest111` quits (~user@49.5.6.87) (Ping timeout: 265 seconds) |
| 05:53:43 | → | larou joins (5eae2591@gateway/web/cgi-irc/kiwiirc.com/ip.94.174.37.145) |
| 05:53:53 | <larou> | hello! |
| 05:57:02 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 05:57:59 | <larou> | unclechu your looking for defunctionalisation |
| 05:58:26 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) |
| 06:00:01 | × | ksamak quits (~ksamak@195.206.169.184) () |
| 06:00:27 | <larou> | <unclechu> it is still impossible in GHC to use higher-order type families? i mean that i can’t use partially applied type family as an argument for another type family |
| 06:00:30 | <larou> | yes you can |
| 06:00:33 | <larou> | defunctionalise it |
| 06:01:08 | <larou> | type level functions as first class citizens, modulo, defunctionalization |
| 06:01:41 | <larou> | then your type level map is easy |
| 06:01:55 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 06:02:45 | <larou> | type family Map :: (f :: a ~> b) -> m a -> m b |
| 06:03:12 | <larou> | erg, Map :: (f a ~> b) -> m a -> m b |
| 06:03:29 | <larou> | Map :: (a ~> b) -> m a -> m b |
| 06:03:31 | <larou> | sorry |
| 06:05:08 | <larou> | type family Map (f :: a ~> b) (xs :: [] a) :: m b where Map _ '[] = '[]; Map f (x ': xs) = f @@ x ': Map f xs |
| 06:05:25 | <larou> | that @@ is because f :: a ~> b, not f :: a -> b |
| 06:06:51 | <larou> | https://pastebin.com/raw/U4Bd48Cq |
| 06:07:21 | <larou> | and you make type instances for Apply for defunctionalisation symbols |
| 06:07:44 | <larou> | that you want to apply using Map |
| 06:08:07 | <larou> | that is, for every ~> you use, in order to get something of that type, you have to "defunctionalise it" |
| 06:08:26 | <larou> | which consists of writing a datatype and making it an instance of apply |
| 06:09:00 | × | jedws quits (~jedws@101.184.175.183) (Remote host closed the connection) |
| 06:09:10 | <larou> | the type of the datatype you make has the same type signature as the type family you defunctionalising, except with ~> instead of -> |
| 06:09:25 | <larou> | and you need one extra symbol for each arrow you change |
| 06:09:36 | → | jedws joins (~jedws@101.184.175.183) |
| 06:09:55 | <larou> | the instance takes the function and its arguments, what it means to "Apply" the datatype |
| 06:10:30 | <larou> | and simply calls the type family, or another defunctionalisation symbol that has fewer ~> |
| 06:11:09 | <larou> | in order to build up all the symbols allowing apply to be chained over multiple inputs like f @@ x @@ y |
| 06:15:14 | <unclechu> | larou: thanks! i’ll dive into this later |
| 06:15:26 | × | zenzike quits (uid257060@gateway/web/irccloud.com/x-ekbwjbhyjbwovlhi) (Quit: Connection closed for inactivity) |
| 06:18:07 | × | falafel quits (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) (Ping timeout: 260 seconds) |
| 06:21:05 | × | Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 240 seconds) |
| 06:24:52 | → | Audentity joins (~Audentity@4e69b241.skybroadband.com) |
| 06:29:35 | × | Sonderblade quits (~helloman@94.191.137.65.mobile.tre.se) (Quit: Konversation terminated!) |
| 06:30:30 | → | supercoven joins (~Supercove@dsl-hkibng31-54fae0-18.dhcp.inet.fi) |
| 06:31:49 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:32:54 | × | coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 06:41:47 | → | hereEthereal joins (4913050a@c-73-19-5-10.hsd1.wa.comcast.net) |
| 06:43:55 | <Axman6> | @hoogle (@@) |
| 06:43:56 | <lambdabot> | Data.Singletons ( |
| 06:43:56 | <lambdabot> | Data.Singletons type a |
| 06:43:56 | <lambdabot> | Diagrams.Angle ( |
| 06:48:26 | → | benjamingr__ joins (uid23465@gateway/web/irccloud.com/x-aztrejkfdpbhytuo) |
| 06:50:44 | → | danvet joins (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) |
| 06:53:43 | × | Audentity quits (~Audentity@4e69b241.skybroadband.com) (Ping timeout: 260 seconds) |
| 06:54:23 | × | PacoV quits (~pcoves@16.194.31.93.rev.sfr.net) (Quit: leaving) |
| 06:57:03 | → | Audentity joins (~Audentity@4e69b241.skybroadband.com) |
| 06:57:53 | → | forcer1 joins (~forcer@s91904426.blix.com) |
| 07:00:11 | → | danvet_ joins (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453) |
| 07:05:14 | → | bitmagie joins (~Thunderbi@200116b806bfae005d76ad0c90a5d25b.dip.versatel-1u1.de) |
| 07:07:25 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 07:07:42 | × | plutoniix quits (~q@ppp-27-55-83-124.revip3.asianet.co.th) (Quit: Leaving) |
| 07:08:33 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Ping timeout: 260 seconds) |
| 07:08:36 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Ping timeout: 240 seconds) |
| 07:09:00 | → | bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) |
| 07:09:21 | × | bitmagie quits (~Thunderbi@200116b806bfae005d76ad0c90a5d25b.dip.versatel-1u1.de) (Client Quit) |
| 07:10:17 | × | Bigcheese quits (~quassel@unaffiliated/bigcheese) (Ping timeout: 260 seconds) |
| 07:10:36 | × | Rudd0 quits (~Rudd0@185.189.115.98) (Ping timeout: 240 seconds) |
| 07:11:37 | × | rprije quits (~rprije@124.148.131.132) (Ping timeout: 264 seconds) |
| 07:12:08 | → | urdh joins (~urdh@unaffiliated/urdh) |
| 07:12:13 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 07:13:11 | → | Bigcheese joins (~quassel@unaffiliated/bigcheese) |
| 07:15:08 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 07:15:14 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:16:47 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:19:16 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 07:20:10 | → | alp joins (~alp@2a01:e0a:58b:4920:f15e:f3ed:dd53:300e) |
| 07:20:39 | × | larou quits (5eae2591@gateway/web/cgi-irc/kiwiirc.com/ip.94.174.37.145) (Quit: Connection closed) |
| 07:24:01 | hackage | subG 0.2.1.0 - Some extension to the Foldable and Monoid classes. https://hackage.haskell.org/package/subG-0.2.1.0 (OleksandrZhabenko) |
| 07:28:26 | × | aplainzetakind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Ping timeout: 268 seconds) |
| 07:32:12 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Quit: leaving) |
| 07:32:56 | → | codeAlways joins (uid272474@gateway/web/irccloud.com/x-gprgopjmphvaootv) |
| 07:33:40 | → | aplainzetakind joins (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 07:34:45 | × | ajmcmiddlin quits (sid284402@gateway/web/irccloud.com/x-esnyudzmonhtpktj) (Ping timeout: 240 seconds) |
| 07:35:24 | → | ajmcmiddlin joins (sid284402@gateway/web/irccloud.com/x-rzusuwaofduhllmt) |
| 07:35:45 | → | bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) |
| 07:41:19 | → | kritzefitz joins (~kritzefit@fw-front.credativ.com) |
| 07:44:26 | → | dragestil joins (~quassel@185.137.175.104) |
| 07:48:30 | × | dragestil quits (~quassel@185.137.175.104) (Client Quit) |
| 07:48:34 | <dminuoso> | koz_: A rigid type variable is one that is not wobbly... |
| 07:48:57 | <dminuoso> | https://www.microsoft.com/en-us/research/publication/wobbly-types-type-inference-for-generalised-algebraic-data-types/ |
| 07:54:03 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:54:43 | <dminuoso> | dolio: Also, are you sure about your characterization that a rigid will not unify with anything else? Does it not unify with a unificational variable? |
| 07:58:56 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 08:01:22 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 260 seconds) |
| 08:01:29 | × | jespada quits (~jespada@90.254.245.49) (Quit: Leaving) |
| 08:02:06 | → | jespada joins (~jespada@90.254.245.49) |
| 08:02:48 | → | chele joins (~chele@ip5b416ea2.dynamic.kabel-deutschland.de) |
| 08:12:15 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) |
| 08:12:47 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 08:14:51 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 08:15:40 | → | oish joins (~charlie@228.25.169.217.in-addr.arpa) |
| 08:16:41 | → | Aquazi joins (uid312403@gateway/web/irccloud.com/x-dkkwvspwitpqcrse) |
| 08:17:16 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 08:20:13 | → | chaosmasttter joins (~chaosmast@p200300c4a70b2a01fdbe436b20b9f284.dip0.t-ipconnect.de) |
| 08:21:11 | → | Varis joins (~Tadas@unaffiliated/varis) |
| 08:21:27 | → | mananamenos joins (~mananamen@84.122.202.215.dyn.user.ono.com) |
| 08:27:36 | → | dhouthoo joins (~dhouthoo@ptr-eiv6509pb4ifhdr9lsd.18120a2.ip6.access.telenet.be) |
| 08:28:40 | × | infinity0 quits (~infinity0@freenet/developer/infinity0) (Remote host closed the connection) |
| 08:29:40 | → | coot joins (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) |
| 08:30:49 | → | infinity0 joins (~infinity0@freenet/developer/infinity0) |
| 08:31:26 | → | guest111` joins (~user@49.5.6.87) |
| 08:33:33 | → | kuribas joins (~user@ptr-25vy0ia1gi47vc0v7ie.18120a2.ip6.access.telenet.be) |
| 08:37:25 | × | revprez_anzio quits (~revprez_a@pool-108-49-213-40.bstnma.fios.verizon.net) (Ping timeout: 264 seconds) |
| 08:37:49 | → | raichoo joins (~raichoo@dslb-178-001-021-225.178.001.pools.vodafone-ip.de) |
| 08:37:52 | → | revprez_anzio joins (~revprez_a@pool-108-49-213-40.bstnma.fios.verizon.net) |
| 08:37:53 | → | isacl___ joins (uid13263@gateway/web/irccloud.com/x-yofapmbxdjxmgdaw) |
| 08:38:33 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 08:41:07 | × | petersen quits (~petersen@redhat/juhp) (Quit: petersen) |
| 08:41:25 | → | Ariakenom joins (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) |
| 08:41:48 | → | petersen joins (~petersen@redhat/juhp) |
| 08:42:45 | × | coco quits (~coco@212-51-146-87.fiber7.init7.net) (Quit: WeeChat 2.9) |
| 08:45:34 | → | Yumasi joins (~guillaume@2a01cb09b06b29ea21daa97718c35c9f.ipv6.abo.wanadoo.fr) |
| 08:46:36 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 08:46:53 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 08:49:07 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 08:51:12 | × | oish quits (~charlie@228.25.169.217.in-addr.arpa) (Ping timeout: 272 seconds) |
| 08:51:58 | × | ridcully quits (~ridcully@p57b5259e.dip0.t-ipconnect.de) (Quit: update) |
| 08:53:00 | → | ridcully joins (~ridcully@p57b5259e.dip0.t-ipconnect.de) |
| 08:54:16 | × | Sgeo quits (~Sgeo@ool-18b982ad.dyn.optonline.net) (Read error: Connection reset by peer) |
| 08:54:32 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 08:55:11 | → | borne joins (~fritjof@200116b864880600f1dc39039d201adf.dip.versatel-1u1.de) |
| 08:57:37 | → | thc202 joins (~thc202@unaffiliated/thc202) |
| 08:58:40 | → | jakob_ joins (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) |
| 08:59:17 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 09:00:01 | × | forcer1 quits (~forcer@s91904426.blix.com) () |
| 09:00:15 | → | oish joins (~charlie@228.25.169.217.in-addr.arpa) |
| 09:00:31 | → | Boomerang joins (~Boomerang@xd520f68c.cust.hiper.dk) |
| 09:03:45 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 09:06:16 | × | oish quits (~charlie@228.25.169.217.in-addr.arpa) (Ping timeout: 240 seconds) |
| 09:07:16 | × | is_null quits (~jpic@pdpc/supporter/professional/is-null) (Remote host closed the connection) |
| 09:07:40 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Ping timeout: 272 seconds) |
| 09:11:26 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:eb39:3323:4fa4:f361) (Ping timeout: 264 seconds) |
| 09:11:54 | → | acidjnk_new joins (~acidjnk@p200300d0c719ff876dbcfe4d3d96265f.dip0.t-ipconnect.de) |
| 09:14:06 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 09:14:16 | × | nados quits (~dan@69-165-210-185.cable.teksavvy.com) (Ping timeout: 240 seconds) |
| 09:17:33 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 09:23:14 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:bdf6:510e:2b42:888e) |
| 09:25:14 | × | a3Dman quits (~3Dman@unaffiliated/a3dman) (Ping timeout: 246 seconds) |
| 09:25:23 | → | christo joins (~chris@81.96.113.213) |
| 09:26:07 | → | DavidEichmann joins (~david@62.110.198.146.dyn.plus.net) |
| 09:29:06 | → | a3Dman joins (~3Dman@unaffiliated/a3dman) |
| 09:30:18 | × | kqr quits (~kqr@vps.xkqr.org) (Ping timeout: 256 seconds) |
| 09:32:04 | × | nh quits (~NextHendr@unaffiliated/nexthendrix) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 09:32:24 | → | nh joins (~NextHendr@finickitively.co.uk) |
| 09:32:48 | nh | is now known as Guest8782 |
| 09:32:54 | × | hnOsmium0001 quits (uid453710@gateway/web/irccloud.com/x-eaonyjbsdauymoqz) (Quit: Connection closed for inactivity) |
| 09:35:46 | → | kqr joins (~kqr@vps.xkqr.org) |
| 09:35:51 | <tomsmeding> | funny how lambdabot apparently considers '@' to be the line end when reading from hoohle? |
| 09:35:56 | <tomsmeding> | *hoogle |
| 09:36:41 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 09:39:20 | → | ubert joins (~Thunderbi@p200300ecdf1e53c9e6b318fffe838f33.dip0.t-ipconnect.de) |
| 09:41:12 | × | zaquest quits (~notzaques@5.128.210.178) (Quit: Leaving) |
| 09:43:33 | → | jakob_ joins (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) |
| 09:43:38 | × | Axman6 quits (~Axman6@pdpc/supporter/student/Axman6) (Read error: Connection reset by peer) |
| 09:43:42 | → | Axma80880 joins (~Axman6@pdpc/supporter/student/Axman6) |
| 09:43:57 | → | zaquest joins (~notzaques@5.128.210.178) |
| 09:45:26 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 09:46:42 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@ppp-27-55-83-106.revip3.asianet.co.th) |
| 09:47:06 | × | phaazon quits (~phaazon@ns378376.ip-5-196-95.eu) (Quit: WeeChat 2.8) |
| 09:47:44 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Client Quit) |
| 09:49:16 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 09:50:48 | → | phaazon joins (~phaazon@2001:41d0:a:fe76::1) |
| 09:50:54 | × | hereEthereal quits (4913050a@c-73-19-5-10.hsd1.wa.comcast.net) (Ping timeout: 245 seconds) |
| 09:51:41 | × | kritzefitz quits (~kritzefit@fw-front.credativ.com) (Remote host closed the connection) |
| 09:51:54 | × | jlamothe quits (~jlamothe@198.251.55.207) (Ping timeout: 256 seconds) |
| 09:53:02 | Axma80880 | is now known as Axman6 |
| 09:54:12 | AWizzArd_ | is now known as AWizzArd |
| 09:54:26 | × | AWizzArd quits (~code@gehrels.uberspace.de) (Changing host) |
| 09:54:26 | → | AWizzArd joins (~code@unaffiliated/awizzard) |
| 09:55:26 | → | Fiver joins (~Fiver@s91904426.blix.com) |
| 09:56:12 | → | FreeBirdLjj joins (~freebirdl@101.228.42.108) |
| 09:56:20 | × | Guest8782 quits (~NextHendr@finickitively.co.uk) (Changing host) |
| 09:56:20 | → | Guest8782 joins (~NextHendr@unaffiliated/nexthendrix) |
| 09:56:21 | Guest8782 | is now known as nh |
| 09:57:56 | → | Varis joins (~Tadas@unaffiliated/varis) |
| 09:59:17 | → | jakob_ joins (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) |
| 10:00:25 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 10:01:06 | → | kritzefitz joins (~kritzefit@fw-front.credativ.com) |
| 10:01:30 | × | FreeBirdLjj quits (~freebirdl@101.228.42.108) (Ping timeout: 272 seconds) |
| 10:04:34 | → | Rudd0 joins (~Rudd0@185.189.115.103) |
| 10:04:56 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 10:06:15 | → | oish joins (~charlie@228.25.169.217.in-addr.arpa) |
| 10:08:56 | → | graf_blutwurst joins (~user@2001:171b:226e:adc0:bd9e:1b6a:d045:2128) |
| 10:09:05 | → | Franciman joins (~francesco@host-82-56-223-169.retail.telecomitalia.it) |
| 10:11:38 | × | wei2912 quits (~wei2912@unaffiliated/wei2912) (Remote host closed the connection) |
| 10:13:25 | × | alp quits (~alp@2a01:e0a:58b:4920:f15e:f3ed:dd53:300e) (Ping timeout: 272 seconds) |
| 10:17:33 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@ppp-27-55-83-106.revip3.asianet.co.th) (Ping timeout: 256 seconds) |
| 10:18:24 | × | guest111` quits (~user@49.5.6.87) (Quit: ERC (IRC client for Emacs 27.1)) |
| 10:18:36 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 10:21:55 | → | comerijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:22:33 | → | alp joins (~alp@2a01:e0a:58b:4920:6901:cad7:f91c:94b1) |
| 10:23:20 | → | bitmagie joins (~Thunderbi@200116b806bfae005d76ad0c90a5d25b.dip.versatel-1u1.de) |
| 10:23:27 | → | christo joins (~chris@81.96.113.213) |
| 10:25:08 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 10:28:04 | × | bitmagie quits (~Thunderbi@200116b806bfae005d76ad0c90a5d25b.dip.versatel-1u1.de) (Client Quit) |
| 10:28:10 | × | christo quits (~chris@81.96.113.213) (Ping timeout: 256 seconds) |
| 10:40:13 | → | jonatanb joins (~jonatanb@83.24.155.27.ipv4.supernova.orange.pl) |
| 10:47:25 | × | cods quits (~fred@tuxee.net) (Ping timeout: 240 seconds) |
| 10:48:38 | → | cods joins (~fred@tuxee.net) |
| 10:49:22 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 10:53:34 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 10:56:43 | → | jakob_ joins (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) |
| 10:56:58 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 10:57:15 | × | isacl___ quits (uid13263@gateway/web/irccloud.com/x-yofapmbxdjxmgdaw) (Quit: Connection closed for inactivity) |
| 11:01:00 | hackage | subG 0.3.0.0 - Some extension to the Foldable and Monoid classes. https://hackage.haskell.org/package/subG-0.3.0.0 (OleksandrZhabenko) |
| 11:01:27 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 11:01:37 | → | m0rphism joins (~m0rphism@HSI-KBW-095-208-098-207.hsi5.kabel-badenwuerttemberg.de) |
| 11:03:54 | → | CRTified[m] joins (schnecfkru@gateway/shell/matrix.org/x-qudvjaxqzetifqrv) |
| 11:05:21 | → | denisse_ joins (~spaceCat@gateway/tor-sasl/alephzer0) |
| 11:05:23 | × | denisse quits (~spaceCat@gateway/tor-sasl/alephzer0) (Ping timeout: 240 seconds) |
| 11:06:27 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 11:06:45 | → | LKoen joins (~LKoen@169.244.88.92.rev.sfr.net) |
| 11:07:53 | × | madog quits (~madog@163.ip-51-254-203.eu) (Quit: ) |
| 11:09:05 | jokester_ | is now known as jokester |
| 11:09:07 | → | madog joins (~madog@163.ip-51-254-203.eu) |
| 11:09:19 | → | Sk01 joins (~sky3@1aac.wls.metu.edu.tr) |
| 11:09:30 | hackage | http-conduit-downloader 1.1.3 - HTTP downloader tailored for web-crawler needs. https://hackage.haskell.org/package/http-conduit-downloader-1.1.3 (VladimirShabanov) |
| 11:09:31 | × | jokester quits (~mono@unaffiliated/jokester) (Quit: WeeChat 2.9) |
| 11:11:19 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 11:15:40 | → | foursaph joins (~foursaph@dynamic-077-006-006-064.77.6.pool.telefonica.de) |
| 11:17:42 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Remote host closed the connection) |
| 11:17:51 | → | jokester joins (~mono@unaffiliated/jokester) |
| 11:17:54 | → | solonarv joins (~solonarv@astrasbourg-653-1-156-155.w90-6.abo.wanadoo.fr) |
| 11:18:06 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@ppp-223-24-153-25.revip6.asianet.co.th) |
| 11:20:16 | × | comerijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 11:22:00 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:29:38 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:30:39 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:31:26 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:32:27 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:33:32 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:34:34 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:35:01 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:36:03 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:36:38 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:37:58 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:38:40 | × | solonarv quits (~solonarv@astrasbourg-653-1-156-155.w90-6.abo.wanadoo.fr) (Ping timeout: 246 seconds) |
| 11:39:03 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:39:17 | → | ggole joins (~ggole@2001:8003:8119:7200:f828:bf:5160:1d23) |
| 11:40:17 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:40:35 | → | solonarv joins (~solonarv@astrasbourg-653-1-156-4.w90-6.abo.wanadoo.fr) |
| 11:41:09 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:42:11 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:42:37 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:45:55 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:46:51 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:47:43 | × | Martinsos quits (~user@cpe-188-129-116-164.dynamic.amis.hr) (Ping timeout: 260 seconds) |
| 11:48:43 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:49:26 | → | jchia__ joins (~jchia@45.32.62.73) |
| 11:50:29 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
| 11:50:51 | → | jchia__ joins (~jchia@58.32.37.146) |
| 11:51:06 | × | chaosmasttter quits (~chaosmast@p200300c4a70b2a01fdbe436b20b9f284.dip0.t-ipconnect.de) (Quit: WeeChat 2.9) |
| 11:52:13 | × | alp quits (~alp@2a01:e0a:58b:4920:6901:cad7:f91c:94b1) (Ping timeout: 272 seconds) |
| 11:53:25 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@ppp-223-24-153-25.revip6.asianet.co.th) (Ping timeout: 240 seconds) |
| 11:53:29 | × | Yumasi quits (~guillaume@2a01cb09b06b29ea21daa97718c35c9f.ipv6.abo.wanadoo.fr) (Ping timeout: 272 seconds) |
| 11:53:57 | <boxscape> | is there a way to make this type family work? Or alternatively, another way to construct and store a proof that one symbol is less than another? https://gist.github.com/JakobBruenker/7e9cae27d2e7d5ef0f9bf93a640a2a42 |
| 11:54:56 | → | chaosmasttter joins (~chaosmast@p200300c4a70b2a01c0445547f28d17ad.dip0.t-ipconnect.de) |
| 11:56:00 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 256 seconds) |
| 11:57:26 | × | spake quits (~spake@84.39.117.57) (Remote host closed the connection) |
| 11:58:07 | → | kritzefitz_ joins (~kritzefit@fw-front.credativ.com) |
| 11:58:17 | fendor_ | is now known as fendor |
| 11:58:36 | × | kritzefitz quits (~kritzefit@fw-front.credativ.com) (Ping timeout: 240 seconds) |
| 11:59:40 | <nshepperd> | at the type level? proofs have to be values |
| 12:00:01 | × | Fiver quits (~Fiver@s91904426.blix.com) () |
| 12:00:09 | <dminuoso> | boxscape: https://hackage.haskell.org/package/constraints-0.12/docs/Data-Constraint.html#v:withDict |
| 12:00:51 | <boxscape> | I'll take a look at that, thanks |
| 12:02:32 | → | PacoV joins (~pcoves@16.194.31.93.rev.sfr.net) |
| 12:02:35 | <PacoV> | Hi. |
| 12:02:43 | <boxscape> | hi |
| 12:02:45 | <dminuoso> | Mmm, promoted gadts... what are these constraints even? |
| 12:02:54 | <dminuoso> | Does the kind system support constraints too? |
| 12:03:13 | <boxscape> | dminuoso I don't really think so but it's where my path led me |
| 12:03:32 | <dminuoso> | The diagnostic certainly reads strangely |
| 12:04:15 | <dminuoso> | boxscape: Im curious, what are you trying to do here? What is that tyfam supposed to be used for? |
| 12:05:03 | <PacoV> | I'm looking for someone who know the Hakyll library. I'd like to know if it's possible to use a url field to generate a route. I went to #hakyll but it's been dead for hours so I give here a shot. |
| 12:05:05 | <nshepperd> | i don't think promoted GADTs are really a thing |
| 12:05:36 | <boxscape> | dminuoso I'm trying to have an expression type that stores the free variables in that expression at the type level, in an ordered list. So if you combine two expressions, I take the union - and while trying to write that function I had to construct a new proof that one symbol is smaller than another |
| 12:06:01 | <boxscape> | dminuoso though in retrospect maybe I wouldn't be able to construct a type-level value of that type to begin with |
| 12:06:46 | <dminuoso> | % data Foo a where MkFoo Int -> Foo Int |
| 12:06:46 | <yahb> | dminuoso: ; <interactive>:186:24: error: parse error on input `Int' |
| 12:06:50 | <dminuoso> | % data Foo a where MkFoo :: Int -> Foo Int |
| 12:06:50 | <yahb> | dminuoso: |
| 12:07:18 | <nshepperd> | there's no type level equivalent of GADT case expressions so even if you could make that 'proof' it would be impossible to do anything useful with it |
| 12:07:36 | <dminuoso> | % type family TyF (s :: *) :: Foo s |
| 12:07:36 | <yahb> | dminuoso: |
| 12:07:43 | <boxscape> | RIght, that makes sense, I thought that a case expression is basically needed here |
| 12:07:45 | <merijn> | boxscape: RIP your sanity :p |
| 12:08:09 | <dminuoso> | % type instance TyF Int = MkFoo 1 |
| 12:08:10 | <yahb> | dminuoso: ; <interactive>:191:31: error:; * Expected kind `Int', but `1' has kind `GHC.Types.Nat'; * In the first argument of `MkFoo', namely `1'; In the type `MkFoo 1'; In the type instance declaration for `TyF' |
| 12:08:11 | <dminuoso> | Mmm |
| 12:08:18 | <dminuoso> | % data Foo a where MkFoo :: Foo Int |
| 12:08:18 | <yahb> | dminuoso: |
| 12:08:23 | <dminuoso> | % type family TyF (s :: *) :: Foo s |
| 12:08:23 | <yahb> | dminuoso: |
| 12:08:26 | <dminuoso> | % type instance TyF Int = MkFoo |
| 12:08:26 | <yahb> | dminuoso: |
| 12:08:33 | <boxscape> | merijn mind you, I would never use haskell type level machinery I'm not allowed to just give up on at the moment :) |
| 12:08:47 | <boxscape> | for anything I'm not allowed * |
| 12:08:50 | <dminuoso> | nshepperd: At least its liftable... |
| 12:09:30 | <boxscape> | dminuoso is that even a GADS under the hood? |
| 12:09:36 | <boxscape> | GADT, rather |
| 12:09:45 | <boxscape> | or wait |
| 12:09:48 | <boxscape> | yes it is |
| 12:11:13 | <boxscape> | Hmmm maybe I could do it if I were to make my own type-level String type |
| 12:13:06 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Remote host closed the connection) |
| 12:13:21 | → | bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) |
| 12:13:37 | × | johnw quits (~johnw@haskell/developer/johnw) (Ping timeout: 260 seconds) |
| 12:15:38 | → | johnw joins (~johnw@haskell/developer/johnw) |
| 12:16:50 | → | Tario joins (~Tario@201.192.165.173) |
| 12:17:34 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) |
| 12:19:49 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 12:26:42 | → | omega8cc joins (~omega8cc@185.204.1.185) |
| 12:27:40 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Ping timeout: 246 seconds) |
| 12:28:17 | → | bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) |
| 12:28:28 | <boxscape> | Is there an UnsafeCoerce for the type level? |
| 12:28:39 | → | Entertainment joins (~entertain@104.246.132.210) |
| 12:28:47 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 12:29:02 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 12:29:07 | → | todda7 joins (~torstein@2a02:587:d96:adb6:c7fc:9428:5ead:614f) |
| 12:29:17 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Client Quit) |
| 12:29:56 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 240 seconds) |
| 12:36:42 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 12:41:31 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 12:42:34 | → | vacm joins (~vacwm@70.23.92.191) |
| 12:44:02 | tomsmeding | shudders |
| 12:45:37 | → | alp joins (~alp@2a01:e0a:58b:4920:c9d2:961b:b0f5:7405) |
| 12:46:07 | → | jakob_ joins (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) |
| 12:46:15 | × | vacm quits (~vacwm@70.23.92.191) (Client Quit) |
| 12:46:59 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) () |
| 12:48:51 | → | Tario joins (~Tario@201.192.165.173) |
| 12:49:23 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Client Quit) |
| 12:49:47 | → | texasmynsted joins (~texasmyns@212.102.45.121) |
| 12:51:27 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 12:54:39 | × | DavidEichmann quits (~david@62.110.198.146.dyn.plus.net) (Remote host closed the connection) |
| 12:55:40 | → | DavidEichmann joins (~david@62.110.198.146.dyn.plus.net) |
| 12:55:56 | × | servo quits (~servo@41.92.32.131) (Remote host closed the connection) |
| 12:55:57 | <ziman> | is there an (probably associated) type family that would give me the inner type of a newtype? |
| 12:57:57 | <ziman> | `Coercible` helps me only when I know the inner type already |
| 12:59:07 | <idnar> | which crc32 lib do I want? |
| 13:00:30 | <idnar> | ziman: https://hackage.haskell.org/package/lens-4.19.2/docs/Control-Lens-Wrapped.html#t:Unwrapped |
| 13:00:58 | <ziman> | oh, right, generics, thanks! |
| 13:01:17 | <dminuoso> | 13:28:28 boxscape | Is there an UnsafeCoerce for the type level? |
| 13:01:34 | <dminuoso> | You want what? |
| 13:02:05 | <boxscape> | I'm about 5% certain that it could help me out :) |
| 13:02:27 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Ping timeout: 256 seconds) |
| 13:02:28 | Uniaika | cocks her musket |
| 13:03:26 | <hc> | idnar: depends on what you're trying to do |
| 13:04:13 | × | sis7_ quits (~user@2001:15e8:110:473e::1) (Quit: sis7_) |
| 13:04:30 | hackage | haskoin-store 0.38.3 - Storage and index for Bitcoin and Bitcoin Cash https://hackage.haskell.org/package/haskoin-store-0.38.3 (jprupp) |
| 13:05:33 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 13:06:58 | <hc> | idnar: the zip library seems to be using the digest package ( https://hackage.haskell.org/package/digest ) |
| 13:07:30 | <idnar> | hc: I'm implementing this madness: https://docs.kraken.com/websockets/#book-checksum |
| 13:08:12 | <hc> | ah okay, so you specifically need CRC32. Then I'd say what works for the best zip library available for haskell (afaict) might work for you as well :) |
| 13:08:18 | × | danvet_ quits (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453) (Quit: Leaving) |
| 13:10:00 | <dminuoso> | Wait.. CRC32 is used as a poor mans MAC_ |
| 13:10:11 | <dminuoso> | That's gross. |
| 13:10:57 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 13:11:56 | <idnar> | dminuoso: it's more of an actual checksum |
| 13:13:10 | <hc> | dminuoso: "TLS with SNI (Server Name Indication) is required in order to establish a Kraken WebSockets API connection." |
| 13:13:17 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 13:13:28 | <hc> | I'd say one layer of transport security should be enough (though, arguably, tls might not be the best choice;=) |
| 13:14:22 | <dminuoso> | Im honestly a bit unsure what the CRC32 even helps with. |
| 13:14:30 | <hc> | nothing, afaict ;p |
| 13:15:01 | hackage | subG 0.4.0.0 - Some extension to the Foldable and Monoid classes. https://hackage.haskell.org/package/subG-0.4.0.0 (OleksandrZhabenko) |
| 13:17:24 | <dminuoso> | "to verify that your data is correct and up to date" |
| 13:17:46 | <idnar> | there's an incrementally updated data structure shared between server and client, this lets the client detect an incorrectly applied update |
| 13:17:46 | <idnar> | but this whole API is madness |
| 13:17:49 | <dminuoso> | If you feed the CRC32 with bad data, you still get a valid CRC hash... |
| 13:18:24 | <dminuoso> | So the only thing this seems to protect against, is a modification in transport. But like hc pointed out, TLS gives us the guarantee of no modification already. |
| 13:18:42 | × | thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 260 seconds) |
| 13:19:04 | <dminuoso> | 14:17:46 idnar | there's an incrementally updated data structure shared between server and client, this lets the client detect an incorrectly applied update |
| 13:19:06 | <dminuoso> | oh |
| 13:19:10 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 13:19:13 | → | geekosaur joins (82659a09@host154-009.vpn.uakron.edu) |
| 13:19:16 | <dminuoso> | So this is a poor mans merkle tree? |
| 13:19:27 | <dminuoso> | With CRC32 instead of a cryptographic hash? |
| 13:19:35 | <idnar> | sort of |
| 13:19:42 | <dminuoso> | Shameful. They should just dub it "a blockchain" and make that much more money. |
| 13:19:49 | <dminuoso> | And trick investors |
| 13:19:52 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:bdf6:510e:2b42:888e) (Ping timeout: 260 seconds) |
| 13:19:59 | <hc> | lol, true |
| 13:20:21 | <int-e> | cyclic redundancy blockchain? |
| 13:20:22 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 13:20:55 | <dminuoso> | I mean to be absolutely fair, a merkle tree with CRC is a perfectly valid thing to do. |
| 13:21:08 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 13:21:12 | <dminuoso> | It just has a much larger attack surface. |
| 13:21:18 | × | __monty__ quits (~toonn@unaffiliated/toonn) (Ping timeout: 265 seconds) |
| 13:21:26 | <dminuoso> | And it gives less guarantees |
| 13:21:51 | <dminuoso> | If you have a high volume/low latency situation, then it's possible a cryptographic hash might just be too expensive |
| 13:22:19 | × | Sk01 quits (~sky3@1aac.wls.metu.edu.tr) (Quit: WeeChat 2.9) |
| 13:23:00 | <int-e> | secretly you've always wanted mutable Merkle trees |
| 13:23:27 | <hc> | =) |
| 13:23:35 | <dminuoso> | Oh boy. "mutable merkle trees" |
| 13:23:46 | <dminuoso> | int-e: Can I expect a publication from you about this? :> |
| 13:23:46 | <hc> | you might even sell it |
| 13:24:05 | <hc> | too bad the mit paper generator only lets you choose the authors, not title |
| 13:24:10 | <dminuoso> | https://github.com/EdgyEdgemond/mutable_merkle |
| 13:24:13 | <dminuoso> | Good lord. This already exists. |
| 13:24:32 | dminuoso | scratches his head |
| 13:25:15 | <boxscape> | hm, I think I can use the symbols library and 26 individual comparison cases (or 64 for upper and lower case + digits) to get a comparison type I can construct at the type level :) |
| 13:25:23 | <boxscape> | for symbols |
| 13:25:47 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) |
| 13:26:35 | <int-e> | dminuoso: that's just a persistent data structure, I think |
| 13:27:16 | <int-e> | (and every update changes the root hash (with high probability, blah), which is how it's supposed to work) |
| 13:27:24 | <dminuoso> | int-e: I think it's rather sort of like `git rebase -i`, where it just recalculates/resigns the entire tree |
| 13:27:58 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 13:28:12 | <int-e> | dminuoso: But it's a tree and you can still reuse the subtrees that haven't changed. |
| 13:28:47 | → | SanchayanMaity joins (~Sanchayan@106.201.35.233) |
| 13:28:55 | <int-e> | (though hmm, the structure has to be very rigid for this to work; so it will have rewrite the whole tree on occasion at least) |
| 13:29:05 | <int-e> | hve -> have to. |
| 13:29:15 | <dminuoso> | "sub-trees", you partial nodes from above |
| 13:29:23 | <dminuoso> | (or partial sub-trees above the mutation points) |
| 13:29:42 | <dminuoso> | which is pretty much what git rebase does |
| 13:30:16 | <int-e> | Oh, you're looking at the whole repo as a tree, not just the commit objects as a blockchain. |
| 13:30:20 | <dminuoso> | right |
| 13:30:44 | <dminuoso> | (so perhaps rather in the sense of a zipper) |
| 13:30:56 | × | SanchayanMaity quits (~Sanchayan@106.201.35.233) (Client Quit) |
| 13:30:57 | <dminuoso> | We could have zippers for merkle trees I guess |
| 13:31:04 | <int-e> | indeed |
| 13:31:25 | → | thc202 joins (~thc202@unaffiliated/thc202) |
| 13:31:32 | <dminuoso> | It's an interesting thought. Coupled with lazyness, that could have some nice properties |
| 13:31:55 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:53e4:af5e:8890:d6d0) |
| 13:32:00 | <dminuoso> | Could lead to relatively cheap mutations, even closer to the root, if you dont need the hashes on all the leafs all the time |
| 13:32:14 | <dminuoso> | I dont just dont have any problems that require merkle trees, sadly |
| 13:32:34 | <int-e> | I really think the persistent data structure analogy is perfect. The property that is problematic is that they want to ensure that if they have the same key-value map, they also end up with the same root hash, which means they need to have the same underlying tree structure regardless of the history of insertions and deletion. |
| 13:33:01 | <int-e> | (or is it just keys? I didn't pay enough attention) |
| 13:33:45 | <dminuoso> | Well, if the hash differs, they wont have the same "ancestory" |
| 13:33:57 | <dminuoso> | Dunno if merkle trees exist in both directions |
| 13:34:10 | × | Axman6 quits (~Axman6@pdpc/supporter/student/Axman6) (Remote host closed the connection) |
| 13:34:25 | → | Axman6 joins (~Axman6@pdpc/supporter/student/Axman6) |
| 13:34:30 | <dminuoso> | (say where the root of the tree is the cumulative signing of all leafs, or in the other direction where the leafs are the cumulative signing of the entire path from the root) |
| 13:35:58 | <dminuoso> | oh wait, it's just the first |
| 13:36:02 | → | jakob_ joins (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) |
| 13:36:05 | <int-e> | Typeable is based on Merkle trees <-- can't remember seeing it put like that anywhere. |
| 13:36:09 | → | SanchayanMaity joins (~Sanchayan@106.201.35.233) |
| 13:37:13 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 13:37:21 | × | Sanchayan quits (~Sanchayan@106.201.35.233) (Quit: leaving) |
| 13:38:04 | <int-e> | (It's not a pure Merkle tree in that there are several node types, and they have varying degree. And you never look at paths from the root, only at the root identity, so... it's not perfect.) |
| 13:38:22 | → | geekosaur joins (82659a09@host154-009.vpn.uakron.edu) |
| 13:39:04 | × | oish quits (~charlie@228.25.169.217.in-addr.arpa) (Ping timeout: 256 seconds) |
| 13:41:45 | → | Yumasi joins (~guillaume@2a01cb09b06b29ea21daa97718c35c9f.ipv6.abo.wanadoo.fr) |
| 13:43:07 | <int-e> | Hmm, if you make a perfectly size-balanced binary tree (L <= R <= L+1, where L is the size of the left child and R is the size of the right child) then insertions and deletions should take the usual O(log(n)) time, and you get the property that the tree shape is determined by the number of nodes. In other words, you *can* avoid having to update the whole tree for a single insertion or deletion. |
| 13:44:29 | → | vacm joins (~vacwm@70.23.92.191) |
| 13:44:34 | → | dcoutts_ joins (~duncan@33.14.75.194.dyn.plus.net) |
| 13:44:50 | × | vacm quits (~vacwm@70.23.92.191) (Client Quit) |
| 13:46:25 | → | FreeBirdLjj joins (~freebirdl@101.228.42.108) |
| 13:46:31 | hackage | zydiskell 0.1.0.0 - Haskell language binding for the Zydis library, a x86/x86-64 disassembler. https://hackage.haskell.org/package/zydiskell-0.1.0.0 (nerded) |
| 13:47:28 | → | alx741 joins (~alx741@181.196.68.148) |
| 13:48:41 | → | bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) |
| 13:50:27 | × | SanchayanMaity quits (~Sanchayan@106.201.35.233) (Quit: SanchayanMaity) |
| 13:50:34 | → | Sanchayan joins (~Sanchayan@106.201.35.233) |
| 13:51:05 | × | PacoV quits (~pcoves@16.194.31.93.rev.sfr.net) (Ping timeout: 240 seconds) |
| 13:51:16 | → | SanchayanMaity joins (~Sanchayan@106.201.35.233) |
| 13:52:06 | × | Sanchayan quits (~Sanchayan@106.201.35.233) (Client Quit) |
| 13:53:58 | → | urodna joins (~urodna@unaffiliated/urodna) |
| 13:56:21 | × | todda7 quits (~torstein@2a02:587:d96:adb6:c7fc:9428:5ead:614f) (Ping timeout: 272 seconds) |
| 13:57:15 | → | Chi1thangoo joins (~Chi1thang@87.112.60.168) |
| 14:00:15 | × | dftxbs3e quits (~dftxbs3e@unaffiliated/dftxbs3e) (Remote host closed the connection) |
| 14:00:30 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 14:00:34 | × | LKoen quits (~LKoen@169.244.88.92.rev.sfr.net) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 14:02:07 | → | dftxbs3e joins (~dftxbs3e@unaffiliated/dftxbs3e) |
| 14:03:29 | → | jlamothe joins (~jlamothe@198.251.55.207) |
| 14:03:30 | hackage | graphula-core 2.0.0.1 - A declarative library for describing dependencies between data https://hackage.haskell.org/package/graphula-core-2.0.0.1 (PatrickBrisbin) |
| 14:03:35 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 14:06:31 | → | rezajan joins (~rezajan@151.243.221.71) |
| 14:06:50 | × | rezajan quits (~rezajan@151.243.221.71) (Client Quit) |
| 14:08:13 | × | jb55 quits (~jb55@gateway/tor-sasl/jb55) (Remote host closed the connection) |
| 14:08:35 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 14:08:36 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 14:08:38 | → | jb55 joins (~jb55@gateway/tor-sasl/jb55) |
| 14:08:56 | × | supercoven quits (~Supercove@dsl-hkibng31-54fae0-18.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 14:09:06 | × | pie_ quits (~pie_bnc]@unaffiliated/pie-/x-0787662) (Ping timeout: 256 seconds) |
| 14:09:10 | × | vancz quits (~vancz@unaffiliated/vancz) (Ping timeout: 256 seconds) |
| 14:11:09 | → | haskellian joins (565d4710@86-93-71-16.fixed.kpn.net) |
| 14:11:16 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) |
| 14:11:25 | → | vancz joins (~vancz@unaffiliated/vancz) |
| 14:11:25 | → | pie_ joins (~pie_bnc]@unaffiliated/pie-/x-0787662) |
| 14:11:44 | → | mirrorbird joins (~psutcliff@mail.stylishbroker.com) |
| 14:12:30 | × | brisbin quits (~patrick@pool-173-49-158-4.phlapa.fios.verizon.net) (Ping timeout: 256 seconds) |
| 14:13:27 | → | jakob_ joins (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) |
| 14:14:06 | → | brisbin joins (~patrick@199.66.179.204) |
| 14:17:30 | hackage | flashblast 0.0.9.0 - Generate language learning flashcards from video. https://hackage.haskell.org/package/flashblast-0.0.9.0 (locallycompact) |
| 14:17:57 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 14:22:25 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 14:22:55 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:95c1:f982:82e4:2d79) |
| 14:26:04 | × | bitmapper quits (uid464869@gateway/web/irccloud.com/x-asjzblgwwtdcvjsz) (Quit: Connection closed for inactivity) |
| 14:30:16 | × | darjeeling_ quits (~darjeelin@122.245.211.11) (Ping timeout: 240 seconds) |
| 14:31:01 | → | renzhi joins (~renzhi@2607:fa49:655f:e600::28da) |
| 14:35:09 | → | LKoen joins (~LKoen@169.244.88.92.rev.sfr.net) |
| 14:36:24 | → | oish joins (~charlie@228.25.169.217.in-addr.arpa) |
| 14:36:36 | × | dftxbs3e quits (~dftxbs3e@unaffiliated/dftxbs3e) (Remote host closed the connection) |
| 14:37:06 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:95c1:f982:82e4:2d79) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 14:37:08 | sqrt2_ | is now known as sqrt2 |
| 14:43:03 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 14:43:32 | × | acidjnk_new quits (~acidjnk@p200300d0c719ff876dbcfe4d3d96265f.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 14:46:19 | w2gz | is now known as w1gz |
| 14:47:35 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 2.9) |
| 14:50:22 | → | darjeeling_ joins (~darjeelin@122.245.211.11) |
| 14:52:47 | × | haskellian quits (565d4710@86-93-71-16.fixed.kpn.net) (Remote host closed the connection) |
| 14:55:39 | × | oish quits (~charlie@228.25.169.217.in-addr.arpa) (Quit: leaving) |
| 14:55:59 | → | acidjnk_new joins (~acidjnk@p200300d0c719ff57608036dc958592ad.dip0.t-ipconnect.de) |
| 14:57:05 | → | dftxbs3e joins (~dftxbs3e@unaffiliated/dftxbs3e) |
| 15:00:02 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 15:00:04 | × | LKoen quits (~LKoen@169.244.88.92.rev.sfr.net) (Read error: Connection reset by peer) |
| 15:00:39 | → | LKoen joins (~LKoen@169.244.88.92.rev.sfr.net) |
| 15:04:45 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 15:09:49 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 15:11:08 | → | Sgeo joins (~Sgeo@ool-18b982ad.dyn.optonline.net) |
| 15:16:14 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 15:16:47 | × | roconnor quits (~roconnor@host-104-157-230-3.dyn.295.ca) (Ping timeout: 260 seconds) |
| 15:16:51 | → | jakob_ joins (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) |
| 15:18:21 | → | christo joins (~chris@81.96.113.213) |
| 15:18:41 | × | kuribas quits (~user@ptr-25vy0ia1gi47vc0v7ie.18120a2.ip6.access.telenet.be) (Ping timeout: 272 seconds) |
| 15:19:41 | → | Martinsos joins (~user@cpe-188-129-116-164.dynamic.amis.hr) |
| 15:20:55 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Client Quit) |
| 15:22:39 | × | graf_blutwurst quits (~user@2001:171b:226e:adc0:bd9e:1b6a:d045:2128) (Remote host closed the connection) |
| 15:22:50 | → | mirrorbird_ joins (~psutcliff@89.40.182.215) |
| 15:22:52 | × | toorevitimirp quits (~tooreviti@117.182.180.118) (Remote host closed the connection) |
| 15:23:50 | × | sszark quits (~sszark@h-213-180.A392.priv.bahnhof.se) (Quit: Lost terminal) |
| 15:24:56 | × | mirrorbird quits (~psutcliff@mail.stylishbroker.com) (Ping timeout: 240 seconds) |
| 15:25:49 | → | knupfer joins (~Thunderbi@200116b8244bd600704b43fffe5fc0ce.dip.versatel-1u1.de) |
| 15:25:51 | × | knupfer quits (~Thunderbi@200116b8244bd600704b43fffe5fc0ce.dip.versatel-1u1.de) (Client Quit) |
| 15:25:52 | × | borne quits (~fritjof@200116b864880600f1dc39039d201adf.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 15:26:03 | → | knupfer joins (~Thunderbi@200116b8244bd600953b9562e9fc25b9.dip.versatel-1u1.de) |
| 15:27:34 | → | nuncanada joins (~dude@179.235.160.168) |
| 15:28:54 | × | brisbin quits (~patrick@199.66.179.204) (Read error: Connection reset by peer) |
| 15:30:50 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 15:31:07 | × | acidjnk_new quits (~acidjnk@p200300d0c719ff57608036dc958592ad.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 15:31:56 | × | codeAlways quits (uid272474@gateway/web/irccloud.com/x-gprgopjmphvaootv) (Quit: Connection closed for inactivity) |
| 15:31:57 | → | roconnor joins (~roconnor@host-104-157-230-3.dyn.295.ca) |
| 15:34:26 | → | brisbin joins (~patrick@199.66.179.204) |
| 15:39:56 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 15:40:56 | → | christo joins (~chris@81.96.113.213) |
| 15:41:24 | → | cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net) |
| 15:43:24 | × | carlomagno quits (~cararell@148.87.23.12) (Remote host closed the connection) |
| 15:45:04 | <dolio> | dminuoso: No, but I think it's close enough. That kind of thing can never be absolutely the case in GHC's type checking, because it doesn't exactly work by 'unification'. A local constraint could always be introduced that allows you to solve an equation between a rigid variable and something else. |
| 15:45:42 | <dolio> | But it's much longer to say whatever is completely accurate, and is no better for intuition. |
| 15:47:26 | <tomjaguarpaw> | I'm confused what I'm supposed to do when my package has a library and an executable. The executable depends on the library, naturally, but if I put it in build-depends then cabal says The package has an extraneous version range for a dependency on an |
| 15:47:44 | <tomjaguarpaw> | internal library: packagename -any && ==0.0.0.0. ... |
| 15:47:51 | <merijn> | tomjaguarpaw: Yeah, ignore that |
| 15:47:57 | <tomjaguarpaw> | Oh OK |
| 15:48:15 | <tomjaguarpaw> | It's one of those, is it? |
| 15:48:37 | → | carlomagno joins (~cararell@148.87.23.12) |
| 15:48:54 | <merijn> | tomjaguarpaw: Essentially cabal now supports multiple libraries per package too, and one of the (planned, non-existent) features is to allow packages to depend on only *some* libraries of other packages |
| 15:48:55 | × | zephyz quits (~zephyz@4e69715d.skybroadband.com) (Quit: zephyz) |
| 15:49:32 | <merijn> | tomjaguarpaw: A weird interaction between code preparing for that future and the current "simply depending on a library in the same package" triggers that warning |
| 15:50:15 | → | bergey joins (~user@pool-74-108-99-127.nycmny.fios.verizon.net) |
| 15:50:46 | <merijn> | tomjaguarpaw: I think it's something like "the version is fixed by being in the same package, but other code is inferring it as a constraint and then later on those facts result in 'hey, this (inferred) constraint is extraneous!'" |
| 15:53:49 | × | omega8cc quits (~omega8cc@185.204.1.185) (Remote host closed the connection) |
| 15:53:52 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:1c60:9ba4:8bf9:ee34) |
| 15:56:03 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 15:56:22 | <tomjaguarpaw> | Aha, I see, two constraints from different places |
| 15:57:41 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 15:58:06 | → | nados joins (~dan@69-165-210-185.cable.teksavvy.com) |
| 16:01:54 | → | todda7 joins (~torstein@ppp-2-84-17-169.home.otenet.gr) |
| 16:05:55 | <merijn> | Which cabal-install, btw? I think it might be fixed in one of the newest ones |
| 16:06:49 | <merijn> | 3.2 or 3.4 release candidate, but not 100% I remember that correctly |
| 16:08:07 | → | mastarija joins (~mastarija@93-136-96-155.adsl.net.t-com.hr) |
| 16:08:16 | → | ddellacosta joins (dd@gateway/vpn/mullvad/ddellacosta) |
| 16:10:24 | → | ph88 joins (~ph88@ip5f5af6cd.dynamic.kabel-deutschland.de) |
| 16:11:02 | hekkaidekapus_ | is now known as hekkaidekapus |
| 16:11:40 | <hekkaidekapus> | merijn: It is not yet fixed, AFAIR. Paging fgaz ^^^ |
| 16:11:49 | → | the-smug-one joins (~user@h188-122-129-70.cust.a3fiber.se) |
| 16:13:04 | → | luto1 joins (~luto@84.39.117.57) |
| 16:14:02 | <fgaz> | multiple libraries? it pretty much works for source packages |
| 16:14:18 | × | dftxbs3e quits (~dftxbs3e@unaffiliated/dftxbs3e) (Remote host closed the connection) |
| 16:14:58 | × | kritzefitz_ quits (~kritzefit@fw-front.credativ.com) (Remote host closed the connection) |
| 16:14:59 | <merijn> | fgaz: It was about the "extraneous constraint" warning when your executable depends on a library in the same package |
| 16:15:24 | <hekkaidekapus> | <https://github.com/haskell/cabal/issues/5119> and <https://github.com/haskell/cabal/issues/5660> |
| 16:16:07 | → | ClaudiusMaximus joins (~claude@198.123.199.146.dyn.plus.net) |
| 16:16:07 | × | ClaudiusMaximus quits (~claude@198.123.199.146.dyn.plus.net) (Changing host) |
| 16:16:07 | → | ClaudiusMaximus joins (~claude@unaffiliated/claudiusmaximus) |
| 16:16:24 | <fgaz> | hekkaidekapus: afaik those two tickets have nothing to do with each other |
| 16:17:01 | → | dftxbs3e joins (~dftxbs3e@unaffiliated/dftxbs3e) |
| 16:17:26 | <hekkaidekapus> | If an executable depends on a sublib and the warning is emitted, does that not relate to 5660? |
| 16:17:59 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 16:18:12 | <fgaz> | this also happens with the main library I think |
| 16:18:32 | <fgaz> | also 5660 refers to public sublibs |
| 16:18:46 | <fgaz> | that warning gets triggered on any sublib |
| 16:18:59 | <the-smug-one> | Hi, I solved a small toy problem for fun in Haskell and uploaded it to my website. It's very "explicit" (passing around state of visited vertices, etc.) and I want to know if there's obvious ways to make it more idiomatic. The link is here: https://jsjolen.github.io/#/structuraltyping the function is isSubtypeOf I'd really appreciate any eyes on it :-). |
| 16:19:00 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 16:19:18 | <hekkaidekapus> | fgaz: Right. So, the discussion above was merely about 5119. |
| 16:19:30 | <fgaz> | According to one of the first comments in #5119, the cause was https://github.com/haskell/cabal/pull/4383 |
| 16:20:46 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 16:20:58 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 260 seconds) |
| 16:22:45 | × | cads quits (~cads@ip-64-72-99-232.lasvegas.net) (Ping timeout: 240 seconds) |
| 16:24:47 | <fgaz> | merijn hekkaidekapus: I just read your messages more thoroughly, and yes, I see what you mean, sorry, it was indeed in preparation to public sublibraries |
| 16:25:24 | <hekkaidekapus> | No problem. |
| 16:25:27 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 16:26:51 | <hekkaidekapus> | fgaz: I pinged you since you seem to have taken over A. Williams’s work on public sublibs (beside Oleg, of course). |
| 16:27:04 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 16:27:49 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 16:29:32 | × | mastarija quits (~mastarija@93-136-96-155.adsl.net.t-com.hr) (Quit: Leaving) |
| 16:29:50 | × | pavonia quits (~user@unaffiliated/siracusa) (Quit: Bye!) |
| 16:31:20 | → | mirrorb2rd joins (~psutcliff@89.40.182.152) |
| 16:31:24 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 16:31:33 | × | ph88 quits (~ph88@ip5f5af6cd.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 16:32:00 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 16:32:08 | → | p0a joins (~user@unaffiliated/p0a) |
| 16:32:20 | × | FreeBirdLjj quits (~freebirdl@101.228.42.108) (Remote host closed the connection) |
| 16:32:25 | <p0a> | Hello in f >>= g, is it guaranteed that all of the side effects of f will take effect before g's? |
| 16:32:55 | → | FreeBirdLjj joins (~freebirdl@101.228.42.108) |
| 16:33:41 | <p0a> | I'm looking at mapM magic (take 10 [1..]) >>= mapM_ print . takeWhile (< 18) where magic x = print x; return x*2, for example |
| 16:33:50 | <tdammers> | p0a: there are no side effects |
| 16:33:56 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 16:33:56 | → | ph88 joins (~ph88@ip5f5af6cd.dynamic.kabel-deutschland.de) |
| 16:34:00 | → | st8less joins (~st8less@2603:a060:11fd:0:d56c:a5ec:de50:ff91) |
| 16:34:05 | × | mirrorbird_ quits (~psutcliff@89.40.182.215) (Ping timeout: 240 seconds) |
| 16:34:36 | <int-e> | ordering of effects (if any) depends on the monad |
| 16:34:55 | <int-e> | In IO, effects of f will happen before effects of g, with the exception of lazy IO. |
| 16:35:09 | <tdammers> | there is some kind of implied ordering to >>=, but it's a bit more subtle than "happens before/after" |
| 16:35:26 | <int-e> | so your code will print 1..10, then 2,4..16. |
| 16:35:31 | <p0a> | Why is my example not lazy? |
| 16:36:05 | <tdammers> | it could be lazy, depending on how `magic` is implemented |
| 16:36:30 | <p0a> | Why is this magic not lazy then? |
| 16:36:42 | <tdammers> | why do you think it's not? |
| 16:36:56 | <int-e> | It is lazy. It returns an IO value. It has no effect by itself. |
| 16:37:29 | <tdammers> | it could return an IO value that specifies a lazy-IO operation though |
| 16:37:32 | × | FreeBirdLjj quits (~freebirdl@101.228.42.108) (Ping timeout: 265 seconds) |
| 16:37:34 | <int-e> | The effects happen when an IO value is run... either from the main function or from another Haskell thread. And that execution sequentializes IO effects. |
| 16:37:38 | <tdammers> | (lazy IO /= lazy evaluation!) |
| 16:38:19 | <Ariakenom> | lazy IO isnt different from threads in that sense |
| 16:38:23 | <int-e> | lazy IO is based on a dirty hack that suspends an IO action to be run when its result is needed |
| 16:38:46 | <int-e> | :t System.IO.Unsafe.unsafeInterleaveIO |
| 16:38:47 | <lambdabot> | IO a -> IO a |
| 16:39:02 | <Ariakenom> | so its not important to bring up as an exception |
| 16:39:03 | × | nuncanada quits (~dude@179.235.160.168) (Ping timeout: 260 seconds) |
| 16:39:07 | <p0a> | AH, I thought Lazy IO dependent on lazy evaluation or something like that |
| 16:39:10 | <tdammers> | my point is that "lazy IO" and an expression being lazy are two different and somewhat unrelated things |
| 16:39:23 | <p0a> | depended* |
| 16:39:43 | <p0a> | it's a good point tdammers, I didn't know that |
| 16:39:53 | <int-e> | p0a: Oh, it does. Lazy evaluation provides a mechanism to detect when a value is needed. |
| 16:40:09 | <tdammers> | ^ yeah, this is how they are related, hence "somewhat" unrelated |
| 16:40:23 | <p0a> | int-e: so the hack is the suspension? |
| 16:40:29 | <int-e> | yes |
| 16:40:51 | <tdammers> | without lazy evaluation, lazy IO would be completely transparent, because the value would be demanded immediately, and the "suspension" mechanism used in lazy IO would be undone straight away |
| 16:41:02 | <p0a> | lazy IO is not visible in the type system though, right? |
| 16:41:07 | <tdammers> | nope |
| 16:41:14 | <tdammers> | :t Data.Text.readFile |
| 16:41:16 | <lambdabot> | error: |
| 16:41:16 | <lambdabot> | Not in scope: ‘Data.Text.readFile’ |
| 16:41:16 | <lambdabot> | No module named ‘Data.Text’ is imported. |
| 16:41:28 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 16:41:29 | <tdammers> | @let import qualified Data.Text.IO |
| 16:41:31 | <lambdabot> | Defined. |
| 16:41:34 | <tdammers> | @let import qualified Data.Text.Lazy.IO |
| 16:41:36 | <lambdabot> | Defined. |
| 16:41:40 | <tdammers> | :t Data.Text.IO.readFile |
| 16:41:41 | <lambdabot> | FilePath -> IO Data.Text.Internal.Text |
| 16:41:48 | <tdammers> | :t Data.Text.Lazy.IO.readFile |
| 16:41:49 | <lambdabot> | FilePath -> IO Data.Text.Internal.Lazy.Text |
| 16:41:49 | <int-e> | :t T.readFile |
| 16:41:50 | <lambdabot> | error: |
| 16:41:50 | <lambdabot> | Not in scope: ‘T.readFile’ |
| 16:41:50 | <lambdabot> | Perhaps you meant one of these: |
| 16:41:56 | × | lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Ping timeout: 240 seconds) |
| 16:41:57 | → | mananamenos_ joins (~mananamen@84.122.202.215.dyn.user.ono.com) |
| 16:42:09 | <Ariakenom> | lazy IO is not popular, recommended or important. although I think its interesting and I've used it for some things |
| 16:42:30 | <tdammers> | it is important to know that it exists, because you can easily cause some surprising and subtle bugs with it |
| 16:42:31 | hackage | phonetic-languages-general 0.3.0.0 - A generalization of the uniqueness-periods-vector-general functionality. https://hackage.haskell.org/package/phonetic-languages-general-0.3.0.0 (OleksandrZhabenko) |
| 16:42:41 | <p0a> | I'm trying to learn a bit on conduit |
| 16:42:53 | <int-e> | @where L.hs |
| 16:42:53 | <lambdabot> | what lambdabot has in scope is at https://silicon.int-e.eu/lambdabot/State/Pristine.hs |
| 16:43:48 | <int-e> | . o O ( nobody needs text ) |
| 16:44:23 | <dminuoso> | lazy IO tends to be useful for short "Im writing a 30 lines one-off program" |
| 16:44:29 | → | sfvm joins (~sfvm@37.228.215.148) |
| 16:44:40 | <dminuoso> | Especially when all you want is in base, so you dont even need cabal to get access to conduit and friends |
| 16:44:53 | × | mananamenos quits (~mananamen@84.122.202.215.dyn.user.ono.com) (Ping timeout: 260 seconds) |
| 16:44:59 | <p0a> | ah I know, it's mapM that guarantees the sequence |
| 16:45:11 | <p0a> | That's what makes it print 1..10 before going to the doubles |
| 16:45:29 | <int-e> | . o O ( And lazy IO is terrible if you want to read the first 100 bytes of all files in your home directory. ) |
| 16:46:12 | <int-e> | (it's a good way to run out of file descriptors) |
| 16:46:36 | <p0a> | hehe maybe the kernel is lazy too int-e |
| 16:46:50 | <Ariakenom> | dminuoso: yeah, like the upcoming #adventofcode |
| 16:47:46 | <dminuoso> | Ariakenom: Right. If you want to beat those "solution within 30 seconds" folks, then you can't afford to spend a second on creating a cabal project or managing build-depends. |
| 16:48:38 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 16:48:43 | <int-e> | main = interact $ ... is the way to go for rapid one-time-tool development ;) |
| 16:49:18 | <Ariakenom> | int-e: indeed. the beginning of almost all of my advent coding |
| 16:49:32 | → | justsomeguy joins (~justsomeg@216.186.218.241) |
| 16:49:32 | × | justsomeguy quits (~justsomeg@216.186.218.241) (Changing host) |
| 16:49:32 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 16:50:01 | → | adamwespiser joins (~adamwespi@107.181.19.30) |
| 16:50:09 | <int-e> | Ariakenom: right... main = interact $ unlines . return . show . solve . lines |
| 16:50:42 | <Ariakenom> | ex. interact (show.sum.map read.map words) |
| 16:50:43 | <int-e> | Ariakenom: (most common `main` from my AoC solutions last year) |
| 16:51:00 | <int-e> | s/map// |
| 16:51:03 | <int-e> | err |
| 16:51:07 | <int-e> | the second, not the first |
| 16:51:31 | <int-e> | And not having spaces around . is ugly. |
| 16:51:36 | <boxscape> | Do all haskell packages that are used within a project have to be compiled with the same version of ghc? More specifically, I was wondering if the cached nix haskell binaries are separate for each ghc version |
| 16:51:41 | <Ariakenom> | for me not because its fast but because its easy dminuoso |
| 16:51:55 | <Ariakenom> | int-e: both true |
| 16:51:57 | → | lagothrix joins (~lagothrix@unaffiliated/lagothrix) |
| 16:52:27 | <int-e> | (I don't feel strongly about $ ... vs. (...)) |
| 16:53:08 | <boxscape> | With multiline expressions I strongly prefer $ |
| 16:53:32 | <tdammers> | not having spaces around . isn't just ugly, it's also a potential source of bugs |
| 16:54:01 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 16:54:08 | <hekkaidekapus> | (Which will be disallowed in future GHC releases.) |
| 16:54:11 | <dminuoso> | boxscape: Yes |
| 16:54:14 | <tdammers> | because foo.bar parses as "foo compose bar", but Foo.bar parses as "identifier bar in namespace Foo" |
| 16:54:17 | <maralorn> | boxscape: Yes and yes |
| 16:54:21 | <dminuoso> | boxscape: The ABI is unstable |
| 16:54:22 | <boxscape> | okay, thanks |
| 16:54:27 | <int-e> | Ariakenom: https://paste.debian.net/1173010/ :-) |
| 16:54:28 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Client Quit) |
| 16:54:47 | <texasmynsted> | This might be bike-shedding but I have created haskell templates and noticed that sometimes I have the main files start with a capital and sometimes with a lower case character. |
| 16:54:57 | <dminuoso> | boxscape: You can find some of the reasons here https://wiki.haskell.org/Shared_libraries_and_GHC |
| 16:55:05 | <maralorn> | And even if the former wouldn‘t be true in some specific circumstances, the later i.e. nix builds would probably always depend on the used ghc version. |
| 16:55:06 | <boxscape> | thanks |
| 16:55:16 | × | Yumasi quits (~guillaume@2a01cb09b06b29ea21daa97718c35c9f.ipv6.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 16:55:22 | <texasmynsted> | The modules are always stared with an upper case. What is more common? |
| 16:55:31 | → | jwynn6 joins (~jwynn6@050-088-122-078.res.spectrum.com) |
| 16:55:35 | × | alp quits (~alp@2a01:e0a:58b:4920:c9d2:961b:b0f5:7405) (Ping timeout: 272 seconds) |
| 16:55:45 | <texasmynsted> | and why? |
| 16:55:57 | <dminuoso> | texasmynsted: It's more common that the files/directories follow the casing used in the modules. |
| 16:56:06 | <hekkaidekapus> | tdammers: foo.bar might also mean field bar of record bar in RecordDotStuff… |
| 16:56:15 | <dminuoso> | I cant speak for why people do it, perhaps its just consistency |
| 16:56:31 | <texasmynsted> | So start with an upper case character then? |
| 16:56:36 | <p0a> | texasmynsted: afiak there's OSes where capital and lowercase make no difference, and it was even proposed for the linux kernel |
| 16:56:45 | <p0a> | talking about filenames |
| 16:56:58 | <texasmynsted> | I am talking specifically about file names. |
| 16:56:59 | <tdammers> | I like to use lowercase filenames for main, to emphasize the fact that they are not intended to be imported |
| 16:57:13 | <sm[m]> | I thought all files except the main one had to be capitalised, like the module name |
| 16:57:21 | <dolio> | That depends on the filesystem, not the OS. |
| 16:57:22 | → | hnOsmium0001 joins (uid453710@gateway/web/irccloud.com/x-rpvaqdolaahudqno) |
| 16:57:23 | <texasmynsted> | tdammers: Ah perfect! Thank you. |
| 16:57:25 | × | LKoen quits (~LKoen@169.244.88.92.rev.sfr.net) (Remote host closed the connection) |
| 16:57:30 | <sm[m]> | except on case-vague filesystems, of course |
| 16:57:34 | <p0a> | dolio: thanks, I misspoke |
| 16:58:15 | <texasmynsted> | I care more that I write the file name deliberately rather than care how the filesystem sees it. |
| 16:58:22 | <Ariakenom> | int-e: return!? let me show my reaction with a smiley (:[]) |
| 16:58:51 | <int-e> | Ariakenom: I expected you to suggest `pure` |
| 16:58:56 | <Ariakenom> | but that's very consistent :D |
| 16:59:08 | <Ariakenom> | yeah but the smiley is funnier |
| 16:59:19 | <texasmynsted> | tdammers: So is your test suite main file also lower case for the same reason? |
| 16:59:26 | <sm[m]> | texasmynsted: capitalise all files except main ones |
| 16:59:30 | <int-e> | Ariakenom: it's hard to type :P |
| 16:59:48 | <maerwald> | I saw a job posting of a company transitioning from haskell to Go... it made me wonder what happened there. :D |
| 16:59:50 | <int-e> | while `return` vs. `pure` is a sign of age |
| 17:00:04 | <texasmynsted> | Okay then the same would go for test "main" files. |
| 17:00:12 | <sm[m]> | yep |
| 17:00:16 | <texasmynsted> | :-) |
| 17:00:17 | <texasmynsted> | Thank you. |
| 17:00:23 | <sm[m]> | if you look at projects you'll see that's the pattern |
| 17:00:45 | <tdammers> | int-e: I oscillate back and forth between religiously using 'pure' and consistently using 'return' for things that are monads and reserving 'pure' for non-monad functors |
| 17:01:07 | → | Yumasi joins (~guillaume@2a01cb09b06b29ea21daa97718c35c9f.ipv6.abo.wanadoo.fr) |
| 17:01:14 | <p0a> | I think allowing for bugs is a feature that helps prop development, which may explain why some shy away from haskell |
| 17:01:25 | <p0a> | not that haskell code can't have bugs |
| 17:01:25 | → | idhugo joins (~idhugo@80-62-116-101-mobile.dk.customer.tdc.net) |
| 17:01:43 | <texasmynsted> | tdammers: why not use pure everywhere it applies. It makes more sense. |
| 17:01:52 | <int-e> | > fix error -- is it bad that this still amuses me? |
| 17:01:53 | <boxscape> | p0a -fdefer-type-errors :) |
| 17:01:54 | <lambdabot> | "*Exception: *Exception: *Exception: *Exception: *Exception: *Exception: *Ex... |
| 17:01:58 | <tdammers> | texasmynsted: I do that too, but I go through phases. |
| 17:02:07 | <texasmynsted> | Hehh I understand |
| 17:02:37 | × | stree_ quits (~stree@50-108-91-191.adr01.mskg.mi.frontiernet.net) (Ping timeout: 264 seconds) |
| 17:02:46 | <maerwald> | p0a: was that in response to me? |
| 17:03:01 | <Ariakenom> | my first instinct in do-notation is to type return, but I always use pure |
| 17:03:04 | → | LKoen joins (~LKoen@169.244.88.92.rev.sfr.net) |
| 17:03:05 | <p0a> | maerwald: yeah |
| 17:03:35 | <int-e> | tdammers: yeah I tend to use `return` for monads, but I think that if I had learned Haskell 10 years later I'd be in the pure `pure` camp. |
| 17:03:41 | <maerwald> | the only thing I can think of is that they have some low-latency requriements, which GHCs GC cannot deliver |
| 17:04:29 | → | conal_ joins (~conal@64.71.133.70) |
| 17:04:51 | <tdammers> | maerwald: it can, just not consistently :P |
| 17:05:20 | → | stree joins (~stree@50-108-97-52.adr01.mskg.mi.frontiernet.net) |
| 17:05:25 | <maerwald> | I remember this is a problem in "real-time" ads bidding I think |
| 17:05:40 | → | nuncanada joins (~dude@179.235.160.168) |
| 17:05:41 | <tdammers> | oh yes |
| 17:05:42 | <p0a> | maerwald: my opinion is not molded by experience or shapen by facts, just something I conjured out of thin air. :P |
| 17:05:53 | <tdammers> | I definitely wouldn't use Haskell for the tight parts of that |
| 17:06:16 | <tdammers> | although the parallel GC could probably do it just fine, but it's still kind of icky that reasoning about perf in Haskell is so bloody hard |
| 17:06:26 | <maerwald> | tdammers: could write it in rust, make a nice C interface and use it in haskell |
| 17:06:42 | <tdammers> | yeah, write it in whatever performs well enough, and then orchestrate it from Haskell |
| 17:06:50 | <tdammers> | C, C++, rust, golang, whatever |
| 17:07:04 | <maerwald> | but a more reasonable assumption might be: their CTO fled the country :p |
| 17:07:10 | <tdammers> | yeah |
| 17:07:18 | <tdammers> | IME, it's usually unreasonable expectations |
| 17:07:21 | <maerwald> | and they were left with an esoteric haskell stack and one junior dev |
| 17:07:36 | <boxscape> | oh no I upgraded to ghc 8.10 and now the type level code I spent today writing doesn't work anymore |
| 17:07:38 | <tdammers> | yep. the "unreasonably enthusiastic junior dev" problem |
| 17:08:00 | hackage | array-chunks 0.1.2.0 - Lists of chunks https://hackage.haskell.org/package/array-chunks-0.1.2.0 (andrewthad) |
| 17:08:25 | <idnar> | is there something like `take` that takes from the end? |
| 17:08:38 | → | alp joins (~alp@88.126.45.36) |
| 17:08:41 | <maerwald> | not lazily |
| 17:08:42 | <maerwald> | :p |
| 17:08:54 | <merijn> | :t \n -> reverse . take n . reverse -- *ducks* |
| 17:08:55 | <lambdabot> | error: |
| 17:08:55 | <lambdabot> | Ambiguous occurrence ‘reverse’ |
| 17:08:55 | <lambdabot> | It could refer to |
| 17:09:03 | <merijn> | wut |
| 17:09:05 | <merijn> | @undefine |
| 17:09:05 | <lambdabot> | Undefined. |
| 17:09:09 | <merijn> | :t \n -> reverse . take n . reverse -- *ducks* |
| 17:09:11 | <lambdabot> | Int -> [a] -> [a] |
| 17:09:30 | <maerwald> | that's probably fine for small lists |
| 17:09:37 | <tdammers> | https://hackage.haskell.org/package/extra-1.7.8/docs/Data-List-Extra.html#v:takeEnd |
| 17:09:52 | <merijn> | maerwald: For big ones to if you do it infrequently enough :p |
| 17:10:05 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 17:10:15 | <tdammers> | for very big ones, "infrequently enough" means "once per universe" |
| 17:10:42 | <boxscape> | not even that if you're dealing with [0..] |
| 17:10:49 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 17:10:55 | <boxscape> | unless you count a non-terminating evaluation as "once" |
| 17:11:20 | <tdammers> | right yeah, if you don't need it to terminate, then you can spawn as many of these as you want |
| 17:11:44 | <maerwald> | You add RAM as you go |
| 17:12:24 | <p0a> | that's what scalable means |
| 17:12:37 | <idnar> | oh I need it reversed anyway and I'm starting with a Map so toDescList + take |
| 17:13:03 | <hekkaidekapus> | If the list is finite, see also Data.Sequence. |
| 17:13:08 | <p0a> | What is an example of a simple monad transformer? |
| 17:13:24 | <maerwald> | p0a: none |
| 17:13:30 | <idnar> | IdentityT :P |
| 17:13:44 | <maerwald> | but there are plenty examples of non-simple transformers :p |
| 17:13:49 | <p0a> | are monad transformers like natural transformations? |
| 17:13:58 | <tdammers> | there's this concept of theoretical size of information, I don't remember the details, but the idea is to calculate how small you could theoretically make a data store for a given amount of information until you hit the limitations of the speed of light (or quantum physics? it's been a while) |
| 17:14:14 | × | st8less quits (~st8less@2603:a060:11fd:0:d56c:a5ec:de50:ff91) (Quit: WeeChat 2.9) |
| 17:14:17 | <tdammers> | which implies that the amount of information that can be stored in a finite universe is also finite |
| 17:14:48 | <koz_> | Something something Bekenstein bound. |
| 17:14:54 | <maerwald> | p0a: check out ExceptT, most other transformers are non-sense anyway |
| 17:14:55 | × | ggole quits (~ggole@2001:8003:8119:7200:f828:bf:5160:1d23) (Quit: Leaving) |
| 17:15:23 | <p0a> | maerwald: thank you |
| 17:16:01 | hackage | json-syntax 0.1.2.0 - High-performance JSON parser and encoder https://hackage.haskell.org/package/json-syntax-0.1.2.0 (andrewthad) |
| 17:16:08 | <tdammers> | maerwald: ExceptT Dynamic RWST Dynamic Dynamic Dynamic IO, a.k.a. the "I give up" monad |
| 17:16:16 | → | jakob_ joins (~textual@p200300f49f162200855785b1c0c4761c.dip0.t-ipconnect.de) |
| 17:16:38 | → | ubert1 joins (~Thunderbi@p200300ecdf1e53a7e6b318fffe838f33.dip0.t-ipconnect.de) |
| 17:17:01 | hackage | say-my-name 0.1.0.0 - Require explicit type application for some type variables. https://hackage.haskell.org/package/say-my-name-0.1.0.0 (mnoonan) |
| 17:18:07 | × | ubert quits (~Thunderbi@p200300ecdf1e53c9e6b318fffe838f33.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 17:18:08 | ubert1 | is now known as ubert |
| 17:18:18 | <maerwald> | at least we can say that the design space of monads has been exhaustively researched in haskell |
| 17:18:57 | <maerwald> | many tears have been shed, but it is what it is |
| 17:20:12 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:53e4:af5e:8890:d6d0) (Ping timeout: 260 seconds) |
| 17:20:47 | <koz_> | maerwald: Press F in chat for monads. |
| 17:22:05 | × | ubert quits (~Thunderbi@p200300ecdf1e53a7e6b318fffe838f33.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 17:23:29 | → | ubert joins (~Thunderbi@p200300ecdf1e53a7e6b318fffe838f33.dip0.t-ipconnect.de) |
| 17:24:05 | <int-e> | > let ekat n xs = last $ zipWith const (replicate n xs ++ tails xs) (tails xs) in map (ekat 3) ["", "ab", "abc", "abcd"] |
| 17:24:07 | <lambdabot> | ["","ab","abc","bcd"] |
| 17:24:49 | <int-e> | . o O ( cotake ) |
| 17:25:00 | hackage | array-builder 0.1.1.0 - Builders for arrays https://hackage.haskell.org/package/array-builder-0.1.1.0 (andrewthad) |
| 17:25:47 | → | Tario joins (~Tario@201.192.165.173) |
| 17:25:48 | → | random joins (~random@46.254.129.126) |
| 17:25:50 | → | geekosaur joins (82659a09@host154-009.vpn.uakron.edu) |
| 17:26:00 | <random> | hey guys |
| 17:26:20 | <random> | is there a way to get all types used by a Servant API? |
| 17:26:23 | <random> | like, a ready made library or something? |
| 17:27:39 | × | Ariakenom quits (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 17:28:18 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 17:28:19 | × | knupfer quits (~Thunderbi@200116b8244bd600953b9562e9fc25b9.dip.versatel-1u1.de) (Remote host closed the connection) |
| 17:28:27 | → | knupfer joins (~Thunderbi@200116b8244bd600859a1b799407ebc4.dip.versatel-1u1.de) |
| 17:30:14 | <texasmynsted> | Could with write what you can in Haskell and what you must, in C/Rust. |
| 17:30:28 | <texasmynsted> | oh yikes. I missed much scrollback |
| 17:31:20 | <maerwald> | Yeah, I think exploring rust and haskell in a single stack is interesting. |
| 17:31:22 | <idnar> | does `Scientific` preserve trailing zeroes? |
| 17:31:36 | → | cgfuh joins (~cgfuh@181.167.191.58) |
| 17:32:06 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:b570:65da:9eeb:ab03) |
| 17:33:07 | <texasmynsted> | Yes, that is my plan at least |
| 17:33:18 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 17:33:25 | → | AlterEgo- joins (~ladew@124-198-158-163.dynamic.caiway.nl) |
| 17:33:49 | → | Ariakenom joins (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) |
| 17:35:30 | <texasmynsted> | I tried two almost the same projects. One in Haskell and one in Rust. Just to see how they feel and compare. Rust feels verbose and awkward when encountering complexity. |
| 17:35:33 | <merijn> | idnar: Probably not |
| 17:36:23 | <texasmynsted> | But when getting closer to the metal language options shrink dramatically. |
| 17:37:02 | × | Boomerang quits (~Boomerang@xd520f68c.cust.hiper.dk) (Remote host closed the connection) |
| 17:37:13 | × | cgfuh quits (~cgfuh@181.167.191.58) (Quit: WeeChat 2.9) |
| 17:37:26 | → | cgfuh joins (~cgfuh@181.167.191.58) |
| 17:38:14 | × | jonatanb quits (~jonatanb@83.24.155.27.ipv4.supernova.orange.pl) (Quit: Leaving...) |
| 17:40:08 | <merijn> | Pet peeve "C is not close to the metal" |
| 17:40:30 | hackage | spake2 0.4.3 - Implementation of the SPAKE2 Password-Authenticated Key Exchange algorithm https://hackage.haskell.org/package/spake2-0.4.3 (rkrishnan) |
| 17:41:39 | <dolio> | What do you mean? It allows perfectly for my 128-bit machine characters. |
| 17:42:38 | <merijn> | dolio: Sure, but that wasn't even what I was getting at |
| 17:42:49 | <dolio> | Yeah, I know. |
| 17:43:03 | <hekkaidekapus> | |> coefficient (scientific 010 2) |
| 17:43:08 | × | the-smug-one quits (~user@h188-122-129-70.cust.a3fiber.se) (Remote host closed the connection) |
| 17:43:14 | <hekkaidekapus> | |> 10 -- idnar |
| 17:43:23 | <merijn> | C is close to the metal...as long as you don't acknowledge your "metal" changed into a superscalar, deeply pipelined, out of order, speculatively executing CPU about 2 decades ago :p |
| 17:43:37 | <texasmynsted> | merijn: What do you use for close to the metal projects? Mostly I see C an assembly. |
| 17:44:10 | <int-e> | vhdl? |
| 17:44:16 | <merijn> | What I use is C or C++, but don't go around those are much closer to the metal than Haskell or Rust |
| 17:44:32 | <dolio> | C is heavily-optimized-for. |
| 17:44:40 | <merijn> | texasmynsted: See also: https://queue.acm.org/detail.cfm?id=3212479 |
| 17:44:51 | <merijn> | Which is conveniently titled "C Is Not a Low-level Language" ;) |
| 17:44:56 | <texasmynsted> | I have found C++ is too bulky and difficult to control. |
| 17:45:05 | → | cads joins (~cads@ip-64-72-99-232.lasvegas.net) |
| 17:45:17 | <merijn> | texasmynsted: In my experience there are two C's |
| 17:45:26 | <texasmynsted> | okay. I am listening |
| 17:46:00 | <merijn> | texasmynsted: 1) C, the language that 90% of C programmers *think* they are writing, and 2) C the actual language as defined by the spec and that compilers attempt to implement |
| 17:46:13 | <merijn> | These two things are, surprisingly *massively* different |
| 17:46:50 | <merijn> | But you don't notice those difference and if no one ever told you anything about modern CPU design *nor* modern compilers, then I can understand how you might imagine that 2 is like 1 |
| 17:46:58 | <p0a> | the interface with the metal is the compiler, not the language |
| 17:47:28 | <int-e> | . o O ( 2) is the thing that turns every C program into a puzzle whether it contains undefined behavior or not ) |
| 17:47:32 | <texasmynsted> | p0a +1 |
| 17:48:10 | <merijn> | p0a: Right, but that just means it becomes impossible to know what code does without also knowing which *exact* version of which *exact* compiler people were using |
| 17:48:16 | <int-e> | . o O ( or, more realistically, into a puzzle to figure out *why* it contains undefined behavior ) |
| 17:48:29 | <merijn> | The point of having a spec is that you can write code and know what it does *without* error prone trial and error |
| 17:48:33 | <dolio> | Yeah, the answer is almost always, "it does," no? :) |
| 17:48:45 | <texasmynsted> | what p0a says aligns with my experience. Typically a manufactured chip has a compiler that will compile a "subset" of C for the chip. |
| 17:48:49 | <merijn> | dolio: Some cases are super fun, though |
| 17:48:59 | <merijn> | dolio: Like "whether this code is undefined is implementation defined" |
| 17:49:04 | <merijn> | dolio: No joke! |
| 17:49:29 | <dolio> | Really? I didn't notice that when I was reading, but I didn't think too hard. |
| 17:49:35 | <merijn> | texasmynsted: Right, but then you're not writing C, you're writing a custom ad hoc underspecified DSL that happens to resemble C |
| 17:49:36 | × | alp quits (~alp@88.126.45.36) (Ping timeout: 256 seconds) |
| 17:49:47 | <texasmynsted> | yes. I understand your point now. |
| 17:49:48 | × | conal_ quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 17:49:57 | <merijn> | dolio: Signed integer overflow is UB, right? |
| 17:50:03 | <dolio> | Yeah. |
| 17:50:15 | <merijn> | dolio: Fun fact: the signedness of "char" is implementation defined :) |
| 17:50:20 | <dolio> | Oh, and you don't know how big they are. |
| 17:50:24 | → | bitmapper joins (uid464869@gateway/web/irccloud.com/x-xpsufctbszodgohs) |
| 17:50:47 | <merijn> | dolio: So you can construct code the is signed overflow if char is signed, but whether it is, is implementation defined |
| 17:50:53 | <texasmynsted> | most things are "implementation defined". The sizes are defined by the chipset |
| 17:51:02 | <merijn> | texasmynsted: I wish |
| 17:51:07 | <dolio> | Ah, yeah. |
| 17:51:20 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 17:51:22 | → | conal joins (~conal@64.71.133.70) |
| 17:51:24 | <merijn> | If we took the C spec as-is and said "all undefined behaviour is implementation defined" we'd be massively better off |
| 17:51:43 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 17:51:44 | <int-e> | implementations with sufficient fire-proofing use unsinged characters |
| 17:51:45 | <texasmynsted> | Or turn it around. |
| 17:52:09 | <texasmynsted> | Okay. I am all in. What language do you propose? |
| 17:52:24 | <merijn> | int-e: That's massively inconsistent, though, because all other integers without a sign specifier default to signed |
| 17:52:27 | <texasmynsted> | Because it will not be C and it will not be Rust and it will not be Haskell. |
| 17:52:31 | <int-e> | ("unsinged" may be my most common typo when writing C) |
| 17:52:36 | <merijn> | texasmynsted: For what purpose? |
| 17:53:19 | × | jb55 quits (~jb55@gateway/tor-sasl/jb55) (Remote host closed the connection) |
| 17:53:21 | <int-e> | merijn: Yes, I agree that was an awful choice. |
| 17:53:32 | <texasmynsted> | Firmware development. Close enough to the metal that the only code running on the chip is what it specifically written. |
| 17:53:40 | → | jb55 joins (~jb55@gateway/tor-sasl/jb55) |
| 17:53:42 | <merijn> | texasmynsted: Ivory? :) |
| 17:53:43 | <geekosaur> | I think I made my editor autofix that one |
| 17:53:47 | <int-e> | 5 compiler writers in a room, all trying to ensure that their own compiler is standards-compliant. |
| 17:53:51 | <merijn> | texasmynsted: Haskell based DSL that generates C |
| 17:53:52 | <dolio> | I think the point was not, "don't use C," but, "don't perpetuate myths about C." |
| 17:54:07 | <merijn> | dolio++ |
| 17:54:31 | texasmynsted | facepalm |
| 17:55:05 | <Chousuke> | I don't see why you couldn't use Rust for firmware development. People seem to be rather interested in doing just that. |
| 17:55:08 | <dolio> | Because the myths are part of what keep people from developing viable alternatives to C. |
| 17:55:09 | <texasmynsted> | I have never heard of Ivory. I need to check this out. |
| 17:55:11 | <merijn> | texasmynsted: dolio: Well, to be fair "don't perpetuate myths" was the mainpoint, but "don't handwrite C whenever you can possibly help it" was a solid 2nd point |
| 17:55:21 | <texasmynsted> | Is it strict? |
| 17:55:21 | × | jakob_ quits (~textual@p200300f49f162200855785b1c0c4761c.dip0.t-ipconnect.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 17:55:42 | <merijn> | texasmynsted: It was developed specifically for embedded/systems stuff where you want statically validated properties, but the tooling requires C |
| 17:56:06 | <srk> | only ivory-backend-c |
| 17:56:14 | <merijn> | texasmynsted: https://ivorylang.org/ivory-concepts.html |
| 17:56:16 | <srk> | which uses language-c |
| 17:56:26 | → | nut joins (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 17:56:29 | <srk> | there are other backends for verification purposes |
| 17:56:33 | → | jakob_ joins (~textual@p200300f49f1622000c6d85cd02bcc449.dip0.t-ipconnect.de) |
| 17:56:39 | <texasmynsted> | Soooo you are writing in a "different" C DSL. |
| 17:56:46 | <Chousuke> | I mean, the fact that often you *have* to use C for firmware development doesn't mean C is particularly well suited for the task. That's just how it happens to be, for mostly historical reasons. :/ |
| 17:56:52 | <texasmynsted> | that compiles to a C DSL |
| 17:57:01 | <merijn> | texasmynsted: No, you are writing in *Haskell* DSL :) |
| 17:57:08 | ← | gecko_ parts (~gecko@2001:19f0:5:10f4:5400:3ff:fe0f:15cb) () |
| 17:57:25 | × | dcoutts_ quits (~duncan@33.14.75.194.dyn.plus.net) (Ping timeout: 240 seconds) |
| 17:57:26 | <texasmynsted> | Okay. You are writing in a Haskell DSL that compiles to a C DSL. |
| 17:57:30 | hackage | zydiskell 0.1.0.1 - Haskell language binding for the Zydis library, a x86/x86-64 disassembler. https://hackage.haskell.org/package/zydiskell-0.1.0.1 (nerded) |
| 17:57:33 | <srk> | compiles to C |
| 17:57:34 | <merijn> | texasmynsted: Developed by a company that develops tools specifically for crypto/embedded stuff |
| 17:57:36 | <texasmynsted> | And this is better why? |
| 17:57:41 | <srk> | safe |
| 17:57:56 | <srk> | and.. embedded in Haskell! :) |
| 17:58:03 | <maerwald> | why is it safe? |
| 17:58:04 | × | brisbin quits (~patrick@199.66.179.204) (Read error: Connection reset by peer) |
| 17:58:06 | <merijn> | texasmynsted: Because that compiler and the people who wrote it are better at C than you are |
| 17:58:13 | <srk> | (bunch of other things as well) |
| 17:58:23 | <texasmynsted> | Because if this can sell, the F*** Rust. |
| 17:58:23 | <merijn> | maerwald: No null pointers (or really heap allocation, tbh) |
| 17:58:39 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 17:58:40 | <p0a> | is there heap allocation in firmware? |
| 17:58:42 | <texasmynsted> | s/the/then/ |
| 17:58:43 | <maerwald> | that's not much to throw around "safe" |
| 17:58:51 | <p0a> | I have never programmed anything like firmware, I don't even know what it is |
| 17:58:52 | <merijn> | maerwald: Define "safe" |
| 17:59:00 | <srk> | p0a: yup, ivory-tower uses heap for FreeRTOS tasks |
| 17:59:06 | <merijn> | maerwald: Definitely safer than hand-written C |
| 17:59:09 | <maerwald> | merijn: formally verified at least |
| 17:59:11 | <merijn> | maerwald: Sure, that's not a high bar |
| 17:59:27 | <merijn> | maerwald: It plugs into formal verification tools as possible backends, that's one of the points/goals :p |
| 17:59:39 | <texasmynsted> | Example: I have written firmware to control the hardware in a water meter and let the water meter communicate over radio. |
| 17:59:46 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-xcriusnvhpaknzlz) |
| 17:59:51 | <merijn> | maerwald: Per the Ivory webpage: "The C language backend supports rendering Ivory assertions for static checking with the CBMC model checker. The SMACCMPilot project build system includes integration for CBMC verification of the SMACCMPilot source code." |
| 17:59:55 | <merijn> | We also provide our own symbolic simulator for verifying Ivory assertions using CVC4. |
| 18:00:09 | <texasmynsted> | I have written code for the head unit in automobiles |
| 18:00:18 | <maerwald> | ok, you're all hired :p |
| 18:00:18 | <p0a> | srk: I had no idea how 'large' firmware can be. I didn't know OSes run on them. I know very little about it :P |
| 18:00:27 | <texasmynsted> | That is what I mean by firmware |
| 18:00:37 | → | Klobbinger joins (543b08ef@dslb-084-059-008-239.084.059.pools.vodafone-ip.de) |
| 18:00:42 | × | motherfsck quits (~motherfsc@unaffiliated/motherfsck) (Remote host closed the connection) |
| 18:00:51 | <merijn> | texasmynsted: Iirc Ivory was originally developed for crypto/firmware applications for DARPA/US Dept of Defense |
| 18:01:24 | <merijn> | texasmynsted: So it's *very* much intended for stuff like "car firmware" |
| 18:01:31 | <texasmynsted> | maerwald: Excellent. What are we building? |
| 18:01:41 | × | Klobbinger quits (543b08ef@dslb-084-059-008-239.084.059.pools.vodafone-ip.de) (Remote host closed the connection) |
| 18:01:42 | <maerwald> | a stupid backend :D |
| 18:01:50 | → | crdrost joins (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) |
| 18:01:50 | <p0a> | nice! |
| 18:01:53 | <merijn> | Oh, that's easy |
| 18:01:57 | <merijn> | I've build tons of those |
| 18:02:18 | <srk> | p0a: depends, I'm typically using STM32 MCUs ranging from 8kb to 512kb SRAM (64kb - 1/2Mb flash) |
| 18:02:26 | <texasmynsted> | maerwald: More specifically please. That pretty much describes everything.] |
| 18:02:45 | → | motherfsck joins (~motherfsc@unaffiliated/motherfsck) |
| 18:02:47 | <maerwald> | I dunno... is there anything other than backends out there? |
| 18:02:47 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 18:02:54 | <merijn> | p0a: It depends on your chip too |
| 18:03:12 | <monochrom> | merijn: Do you happen to know why they chose the name Ivory? Is it about "yes this is from the ivory power, bite me"? :) |
| 18:03:15 | <merijn> | p0a: Embedded chips powerful enough to run regular linux or pretty cheap |
| 18:03:21 | <merijn> | monochrom: Probably? |
| 18:03:27 | <srk> | it's explained in one of the papers |
| 18:03:43 | <merijn> | monochrom: Considering there's an associated language mentioned on their website called "tower"... |
| 18:03:44 | <srk> | something like 'to bring embedded development down from ivory tower' |
| 18:03:52 | <monochrom> | hahaha neat |
| 18:03:58 | → | Klobbinger joins (543b08ef@dslb-084-059-008-239.084.059.pools.vodafone-ip.de) |
| 18:04:01 | → | brisbin joins (~patrick@pool-173-49-158-4.phlapa.fios.verizon.net) |
| 18:04:03 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 18:04:04 | <monochrom> | thanks merijn and srk |
| 18:04:25 | × | nut quits (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 18:04:48 | <merijn> | monochrom: That's why the clash people had to figure out something else to name clash ;) |
| 18:04:58 | <merijn> | (statement not actually based in facts) |
| 18:05:08 | <monochrom> | hahahahaha name clash |
| 18:05:55 | <texasmynsted> | Hmm. I would love to see people describe their experience with various commodity chips. |
| 18:06:17 | <merijn> | I'm just sad Habit died |
| 18:06:40 | <monochrom> | In other news, today I showed my students the fibonacci joke "This Fibonacci joke is as bad as the last two you heard combined." and the originating tweet URL https://twitter.com/sigfpe/status/776420034419658752 |
| 18:06:46 | × | jakob_ quits (~textual@p200300f49f1622000c6d85cd02bcc449.dip0.t-ipconnect.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 18:08:17 | <merijn> | heh, so according to reddit Haskell job openings it's "hard to find people with 5+ years experience", so clearly I need to start demanding rockstar salary by now >.> |
| 18:09:04 | <Ariakenom> | texasmynsted: A colleague had an awesome patch for an avr8. It just rearranged members in a struct. |
| 18:09:38 | <texasmynsted> | merijn: You should. |
| 18:10:01 | <Ariakenom> | the compiled code was smaller because the members were in nicer locations. he find out where to place them by trying all of them in a script |
| 18:10:12 | <texasmynsted> | Where do you work? |
| 18:10:16 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Quit: cosimone) |
| 18:10:41 | <Ariakenom> | we needed that because we were running out of flash storage on them |
| 18:10:44 | <merijn> | texasmynsted: Well currently I don't write Haskell to begin with, or rather, at least not officially :p |
| 18:10:52 | <texasmynsted> | What? |
| 18:10:55 | <texasmynsted> | That is crazy |
| 18:11:01 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 18:11:03 | <texasmynsted> | What do you write? |
| 18:11:37 | <maerwald> | IRC |
| 18:11:42 | <texasmynsted> | So like many of us Haskell is your guilty pleasure? |
| 18:11:42 | <maerwald> | look at his IRC stats |
| 18:11:44 | <maerwald> | :p |
| 18:11:45 | <merijn> | maerwald: shush |
| 18:11:46 | <texasmynsted> | LOLOL |
| 18:11:47 | → | conal joins (~conal@64.71.133.70) |
| 18:11:51 | <p0a> | Ariakenom: can't you just pack a struct? |
| 18:12:04 | <merijn> | maerwald: dminuoso is still in first because (thank god) Chris Done's ircbrowse stats got lost |
| 18:12:23 | tomsmeding | . o O ( it will grow over time ) |
| 18:12:28 | <texasmynsted> | I think you could argue you are promoting your haskell mentoring |
| 18:12:39 | <Ariakenom> | p0a: it wasnt to reduce memory. it was to reduce code size :D |
| 18:13:04 | <merijn> | texasmynsted: Currently C, C++, Fortran90, Python, within the organisation probably "basically everything besides, like, PHP and perl" :p |
| 18:13:10 | <texasmynsted> | His handle must not be chrisdone |
| 18:13:34 | <texasmynsted> | Fortran90. Interesting. |
| 18:13:37 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 18:13:50 | <merijn> | texasmynsted: That's for the lucky people not dealing with Fortran77 :p |
| 18:14:11 | <p0a> | Ariakenom: I'm confused, but I believe you :) |
| 18:14:20 | <texasmynsted> | I am trying to determine where you work where Fortran90 would be used. . . |
| 18:14:32 | <merijn> | texasmynsted: Oh, I still write Haskell stuff at work, because no one's around to tell me no :p |
| 18:16:32 | → | valdyn joins (~valdyn@host-88-217-143-53.customer.m-online.net) |
| 18:16:35 | <texasmynsted> | Well it sound interesting |
| 18:18:37 | <texasmynsted> | I like how some people say they use Haskell for "prototyping" |
| 18:19:07 | × | knupfer quits (~Thunderbi@200116b8244bd600859a1b799407ebc4.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 18:20:04 | <dolio> | Haskell is too mainstream for prototyping. |
| 18:20:12 | <dolio> | Prototype your Haskell stuff in Agda. |
| 18:20:33 | <texasmynsted> | or Idris |
| 18:20:57 | <dolio> | Yeah. Although if you prototype in Idris you might find you can just use the prototype. :þ |
| 18:21:35 | <texasmynsted> | yes. That is the point. A Haskell prototype likely works better and is more maintainable than the target language |
| 18:21:55 | → | jedai42 joins (~jedai@lfbn-dij-1-708-251.w90-100.abo.wanadoo.fr) |
| 18:22:00 | <monochrom> | Programmers seldom grow out of their prototypes. |
| 18:22:09 | <merijn> | Prototype in Haskell, because we all know prototypes become production and never stop, so now they gotta hire more haskellers to support it |
| 18:22:14 | <merijn> | Boom. Haskell shop |
| 18:22:15 | × | chele quits (~chele@ip5b416ea2.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 18:22:22 | <monochrom> | Especially, a lot of FOSS software is intentionally forever in beta. |
| 18:22:28 | → | Lycurgus joins (~niemand@cpe-45-46-142-188.buffalo.res.rr.com) |
| 18:22:51 | <texasmynsted> | If only I could think of an app to write. |
| 18:22:51 | <merijn> | monochrom: My FOSS isn't in beta. It's "free as in puppies" |
| 18:23:05 | <texasmynsted> | If I could ever think of one I would do it. |
| 18:23:18 | <geekosaur> | does it breed like them, too? |
| 18:23:22 | <merijn> | monochrom: You can pick it up for free, but you'll have to pay to get it fixed ;) |
| 18:23:27 | <monochrom> | Namely, those who follows ESR's bazaar model. The bazaar model is euphemism for intentional perpetual beta. |
| 18:23:32 | <dolio> | Commercial software doesn't really seem that different from the inside. |
| 18:23:46 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 18:23:56 | <dolio> | You only believe it's not still in beta because you bought it. |
| 18:24:08 | <texasmynsted> | The difference is in that you paid for it. |
| 18:24:10 | <geekosaur> | there is that, isn't there? |
| 18:25:25 | × | jedai quits (~jedai@lfbn-dij-1-708-251.w90-100.abo.wanadoo.fr) (Ping timeout: 240 seconds) |
| 18:26:08 | → | alp joins (~alp@2a01:e0a:58b:4920:61ca:7518:9e8a:5ce1) |
| 18:26:35 | <dolio> | I guess people pay for beta commercial software these days, too. |
| 18:26:43 | <merijn> | monochrom: You might like PHK's take: https://queue.acm.org/detail.cfm?id=2349257 :) |
| 18:26:48 | <monochrom> | Right, I don't contend that. |
| 18:27:18 | <dolio> | At least video games. Lots of people buying perpetual beta games. :) |
| 18:27:44 | → | jakob_ joins (~textual@p200300f49f1622000c29800dbc05d17e.dip0.t-ipconnect.de) |
| 18:29:00 | <texasmynsted> | I buy books from manning that are not even to alpha stage yet |
| 18:29:50 | × | darjeeling_ quits (~darjeelin@122.245.211.11) (Ping timeout: 256 seconds) |
| 18:30:17 | → | ishutin joins (~Ishutin@92-249-179-45.pool.digikabel.hu) |
| 18:33:25 | × | ishutin_ quits (~Ishutin@91-83-11-228.pool.digikabel.hu) (Ping timeout: 246 seconds) |
| 18:34:04 | × | fraktor quits (~walt@129.93.191.18) (Quit: WeeChat 2.8) |
| 18:34:05 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed) |
| 18:34:24 | → | u0_a298 joins (~user@47.206.148.226) |
| 18:34:47 | × | jakob_ quits (~textual@p200300f49f1622000c29800dbc05d17e.dip0.t-ipconnect.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 18:37:36 | × | u0_a298 quits (~user@47.206.148.226) (Read error: Connection reset by peer) |
| 18:37:50 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 18:38:00 | <maerwald> | video games is a brutal industry anyway |
| 18:38:01 | → | u0_a298 joins (~user@47.206.148.226) |
| 18:38:36 | <texasmynsted> | video game industry is a gold rush |
| 18:39:51 | → | knupfer joins (~Thunderbi@200116b8244bd600d8ff78fffe37ebfb.dip.versatel-1u1.de) |
| 18:40:17 | × | knupfer quits (~Thunderbi@200116b8244bd600d8ff78fffe37ebfb.dip.versatel-1u1.de) (Remote host closed the connection) |
| 18:40:25 | → | knupfer joins (~Thunderbi@200116b8244bd6009cdc066a89cb8c22.dip.versatel-1u1.de) |
| 18:42:18 | Lord_of_Life_ | is now known as Lord_of_Life |
| 18:42:37 | <idnar> | hekkaidekapus: aha |
| 18:43:06 | × | Ariakenom quits (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) (Quit: Leaving) |
| 18:44:53 | → | darjeeling_ joins (~darjeelin@122.245.211.11) |
| 18:45:03 | <hekkaidekapus> | idnar: Are you parsing stuff? I’m wondering whether you are actually after Data.Fixed. |
| 18:46:58 | <idnar> | hekkaidekapus: JSON numbers, kinda |
| 18:47:21 | <hekkaidekapus> | Parsing it is, then. |
| 18:47:39 | → | Ariakenom joins (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) |
| 18:48:56 | → | conal joins (~conal@64.71.133.70) |
| 18:49:07 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Ping timeout: 260 seconds) |
| 18:51:00 | <hekkaidekapus> | @hackage scientific-notation <== idnar: Check out that. |
| 18:51:00 | <lambdabot> | https://hackage.haskell.org/package/scientific-notation <== idnar: Check out that. |
| 18:51:05 | <idnar> | hekkaidekapus: I'm implementing this madness: https://docs.kraken.com/websockets/#book-checksum |
| 18:51:33 | × | SanchayanMaity quits (~Sanchayan@106.201.35.233) (Quit: SanchayanMaity) |
| 18:52:25 | × | jespada quits (~jespada@90.254.245.49) (Quit: Leaving) |
| 18:52:34 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Ping timeout: 245 seconds) |
| 18:52:38 | <idnar> | hekkaidekapus: ooh this is handy |
| 18:52:44 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:1c60:9ba4:8bf9:ee34) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 18:53:01 | → | jespada joins (~jespada@90.254.245.49) |
| 18:54:12 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:1c60:9ba4:8bf9:ee34) |
| 18:55:22 | <idnar> | hekkaidekapus: thanks! |
| 18:56:07 | × | knupfer quits (~Thunderbi@200116b8244bd6009cdc066a89cb8c22.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 18:56:20 | <dminuoso> | idnar: You could also look at https://hackage.haskell.org/package/scientific-0.3.6.2/docs/Data-Scientific.html which is what aeson uses |
| 18:56:30 | <hekkaidekapus> | You’re welcome. That Kraken thing has speed requirements. You will appreciate this line: “The scientific-notation parser outperforms the scientific parser that ships with aeson by a factor of five on small numbers.” |
| 18:56:59 | <hekkaidekapus> | dminuoso: Raced :) ^^^ |
| 18:57:37 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 19:00:02 | × | u0_a298 quits (~user@47.206.148.226) (Read error: Connection reset by peer) |
| 19:00:19 | → | u0_a298 joins (~user@47.206.148.226) |
| 19:02:36 | × | u0_a298 quits (~user@47.206.148.226) (Read error: Connection reset by peer) |
| 19:02:41 | <idnar> | hekkaidekapus: yeah, for what I'm doing, it's very useful to have a fast parse to something I can do trivial ops on; I need a more complicated conversion after that, but the converted values often go unused so I don't have to pay |
| 19:02:51 | → | u0_a298 joins (~user@47.206.148.226) |
| 19:03:24 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 19:03:42 | × | berberman_ quits (~berberman@unaffiliated/berberman) (Ping timeout: 260 seconds) |
| 19:03:56 | <idnar> | dminuoso: I am currently parsing to that :) |
| 19:06:13 | × | u0_a298 quits (~user@47.206.148.226) (Read error: Connection reset by peer) |
| 19:06:30 | → | u0_a298 joins (~user@47.206.148.226) |
| 19:07:15 | → | dragestil joins (~quassel@185.137.175.104) |
| 19:07:20 | <idnar> | hekkaidekapus: blah, I could do with an Ord instance though |
| 19:08:47 | <hekkaidekapus> | The parsed numbers are not meant to be used as such. Refer to the ‘Consume’ section of haddocks instead. |
| 19:10:00 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 19:10:39 | → | wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) |
| 19:11:39 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 19:11:52 | × | nados quits (~dan@69-165-210-185.cable.teksavvy.com) (Quit: Leaving) |
| 19:12:57 | × | texasmynsted quits (~texasmyns@212.102.45.121) (Remote host closed the connection) |
| 19:13:32 | → | texasmynsted joins (~texasmyns@212.102.45.121) |
| 19:14:11 | → | geekosaur joins (82659a09@host154-009.vpn.uakron.edu) |
| 19:14:48 | × | dragestil quits (~quassel@185.137.175.104) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 19:16:52 | × | ubert quits (~Thunderbi@p200300ecdf1e53a7e6b318fffe838f33.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 19:17:52 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 19:19:08 | × | texasmynsted quits (~texasmyns@212.102.45.121) (Ping timeout: 256 seconds) |
| 19:20:44 | × | Jonno_FTW quits (~come@api.carswap.me) (Ping timeout: 272 seconds) |
| 19:21:46 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) |
| 19:22:28 | → | knupfer joins (~Thunderbi@200116b8244bd6003ce66efffe6f5e29.dip.versatel-1u1.de) |
| 19:22:29 | × | knupfer quits (~Thunderbi@200116b8244bd6003ce66efffe6f5e29.dip.versatel-1u1.de) (Client Quit) |
| 19:22:43 | → | mastarija joins (~mastarija@93-136-96-155.adsl.net.t-com.hr) |
| 19:22:45 | → | knupfer joins (~Thunderbi@i5E86B4DB.versanet.de) |
| 19:23:36 | <mastarija> | I'm having some trouble writing instances for generics. |
| 19:23:40 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Ping timeout: 256 seconds) |
| 19:23:56 | <mastarija> | I have these two instances |
| 19:23:58 | <mastarija> | instance {-# OVERLAPPABLE #-} EncOpaque' v => EncOpaque' ( S1 s v ) where |
| 19:24:05 | <mastarija> | instance EncOpaque' v => EncOpaque' ( S1 ('MetaSel ( 'Just f ) x y z ) v ) where |
| 19:24:31 | <mastarija> | problem is that in the second I want to get name of the field 'f' |
| 19:24:43 | <mastarija> | for that I have to use Selector class |
| 19:24:53 | <mastarija> | if I do something like this: |
| 19:25:15 | <mastarija> | instance ( Selector s , EncOpaque' v ) => EncOpaque' ( S1 s v ) where |
| 19:25:47 | <mastarija> | then i can't match instance to specific case where s is 'MetaSel ( 'Just f ) x y z |
| 19:25:58 | <jle`> | i would recommend trying to avoid overlappable instances if possible |
| 19:26:10 | <jle`> | but in your case it looks like you just need a Selector ('MetaSel ('Just f) x y z) constraint |
| 19:26:23 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 19:26:28 | <mastarija> | oh |
| 19:26:31 | <mastarija> | I'm an idiot |
| 19:26:50 | <mastarija> | I was trying things like ( Selector s , s ~ ( 'MetaSel ( 'Just f ) x y z ) , EncOpaque' v ) |
| 19:26:51 | <glguy> | You could avoid the overlap by expanding the other instance to match on Nothing |
| 19:27:01 | → | acidjnk_new joins (~acidjnk@p200300d0c719ff57608036dc958592ad.dip0.t-ipconnect.de) |
| 19:27:05 | <jle`> | yeah, or enumerate whatever you would want to exclude |
| 19:27:24 | <mastarija> | glguy, yes that was the next step but I had a brain freeze on this problem |
| 19:27:30 | <mastarija> | thanks |
| 19:27:36 | → | Jonno_FTW joins (~come@api.carswap.me) |
| 19:28:03 | <jle`> | np :) |
| 19:28:19 | <jle`> | hm, why is there no type family to compare Type's :'( |
| 19:28:24 | <jle`> | there is an Ord instance for TypeRep |
| 19:28:27 | <jle`> | so it should be possible |
| 19:29:30 | hackage | bank-holidays-england 0.2.0.6 - Calculation of bank holidays in England and Wales https://hackage.haskell.org/package/bank-holidays-england-0.2.0.6 (dten) |
| 19:30:01 | × | Lycurgus quits (~niemand@cpe-45-46-142-188.buffalo.res.rr.com) (Quit: Exeunt) |
| 19:30:07 | × | Yumasi quits (~guillaume@2a01cb09b06b29ea21daa97718c35c9f.ipv6.abo.wanadoo.fr) (Ping timeout: 272 seconds) |
| 19:30:13 | → | cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net) |
| 19:31:12 | → | justan0theruser joins (~justanoth@unaffiliated/justanotheruser) |
| 19:31:39 | <mastarija> | jle`, quick question, with your suggested solution I'm getting a simplifiable constraint warning |
| 19:32:23 | <jle`> | what's the warning? |
| 19:32:30 | <mastarija> | The constraint `Selector ('MetaSel ('Just f) x y z)' matches instance (SingI mn, SingI su, SingI ss, SingI ds) => Selector ('MetaSel mn su ss ds |
| 19:32:54 | <mastarija> | jle`, SingI is not exported from Generics module so I can't use it |
| 19:33:04 | <jle`> | hm, that's interseting. i guess it's saying that you can use those constraints instead of Selector |
| 19:33:08 | <jle`> | is it from the singletons library, maybe? |
| 19:33:17 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 272 seconds) |
| 19:33:22 | <mastarija> | No, I think it's something ad hoc from Generics module |
| 19:33:47 | <mastarija> | I also thought it's from singletons, but generics defines its own SingI class |
| 19:33:49 | <jle`> | whoops |
| 19:33:57 | <jle`> | then yeah, you can't really do anything about that |
| 19:34:02 | <jle`> | that i know of |
| 19:34:05 | <mastarija> | :D |
| 19:34:12 | <mastarija> | thanks anyway |
| 19:34:31 | <jle`> | np D: |
| 19:36:42 | <glguy> | mastarija: just merge the two instances into one |
| 19:36:43 | <mastarija> | jle`, when I enable GADTs (and MonoLocalBinds) the warning goes away |
| 19:36:46 | → | st8less joins (~st8less@2603:a060:11fd:0:9539:fd10:c1ca:1d78) |
| 19:36:52 | <jle`> | oh nice |
| 19:37:09 | <glguy> | Check if selName is "" and branch on that |
| 19:37:57 | <mastarija> | glguy, I was thinking about it, but it kind of seemed messy and I'd had to do a lot of extra work in other instances |
| 19:38:03 | <mastarija> | Dunno, will think about it |
| 19:38:10 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 246 seconds) |
| 19:38:40 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 19:38:57 | → | texasmynsted joins (~texasmyns@212.102.45.121) |
| 19:39:13 | → | codecaveman joins (58deaa27@88.222.170.39) |
| 19:40:05 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 19:40:15 | × | alp quits (~alp@2a01:e0a:58b:4920:61ca:7518:9e8a:5ce1) (Ping timeout: 272 seconds) |
| 19:40:46 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 19:41:20 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Quit: cosimone) |
| 19:42:06 | → | borne joins (~fritjof@200116b864880600f1dc39039d201adf.dip.versatel-1u1.de) |
| 19:42:25 | → | conal_ joins (~conal@64.71.133.70) |
| 19:42:46 | → | jakob_ joins (~textual@p200300f49f162200756a589588d5c172.dip0.t-ipconnect.de) |
| 19:44:37 | <gehmehgeh> | Am I correct in that Data.Map doesn't have a function to see whether or not a Data.Map is empty? Meaning, you *have* to compare with an empty Data.Map? |
| 19:44:46 | <merijn> | It does |
| 19:44:55 | <gehmehgeh> | ah? |
| 19:44:57 | × | raichoo quits (~raichoo@dslb-178-001-021-225.178.001.pools.vodafone-ip.de) (Quit: Lost terminal) |
| 19:44:58 | <merijn> | Probably "null"? |
| 19:45:01 | <merijn> | :t M.null |
| 19:45:06 | <lambdabot> | M.Map k a -> Bool |
| 19:45:08 | <gehmehgeh> | ah! |
| 19:45:11 | <gehmehgeh> | Thank you! |
| 19:45:18 | <gehmehgeh> | (Sorry, I was a bit confused) |
| 19:45:48 | <gehmehgeh> | I *did* look at https://hackage.haskell.org/package/containers-0.3.0.0/docs/Data-Map.html, but missed it somehow.. |
| 19:45:53 | <gehmehgeh> | Thanks :) |
| 19:45:56 | <davean> | gehmehgeh: Is there something that could have made that more obvious? |
| 19:45:59 | → | Guest42 joins (56ca6780@gateway/web/cgi-irc/kiwiirc.com/ip.86.202.103.128) |
| 19:46:01 | × | conal_ quits (~conal@64.71.133.70) (Client Quit) |
| 19:46:03 | <merijn> | gehmehgeh: Note the "module Data.Map.Lazy" line there |
| 19:46:15 | <merijn> | gehmehgeh: That indicates a re-export of stuff from Data.Map.Lazy |
| 19:46:37 | <merijn> | gehmehgeh: There's some work in haddock to make re-exports more obvious, but it's not done yet, I think? |
| 19:47:05 | <merijn> | gehmehgeh: So most of the actualy API of Map is Data.Map.Lazy and Data.Map.Strict |
| 19:47:12 | <gehmehgeh> | davean: no, it was my fault. I simply overlooked the word "empty" in one instance of the website. THis normally doesn't happen to me ;) |
| 19:47:35 | → | kritzefitz_ joins (~kritzefit@212.86.56.80) |
| 19:47:35 | → | SanchayanMaity joins (~Sanchayan@106.201.35.233) |
| 19:47:56 | <gehmehgeh> | It even says: "O(1). Is the map empty?" |
| 19:48:22 | <merijn> | gehmehgeh: Comparing with == would be bad, because that doesn't work if your values aren't an instance of Eq :) |
| 19:48:23 | <glguy> | davean: naming it isEmpty instead of null could help |
| 19:48:31 | <gehmehgeh> | merijn: That's exactly right. |
| 19:48:38 | <gehmehgeh> | merijn: This is actually why I asked. |
| 19:48:55 | <merijn> | glguy: On the one hand, yes. On the other hand "null" is consistent across a whole bunch of packages and Foldable currently |
| 19:49:05 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Ping timeout: 240 seconds) |
| 19:49:36 | <glguy> | Yeah, it's a shame we got stuck with that name due to inertia |
| 19:49:43 | × | codecaveman quits (58deaa27@88.222.170.39) (Remote host closed the connection) |
| 19:49:53 | <merijn> | It's a shame that we're stuck with lots of things due to inertia :) |
| 19:50:12 | <monochrom> | One of the rare instances when Scheme is admirable because it allows the name to be "null?" |
| 19:50:40 | <dolio> | Yeah, I wish we could put question marks in names. |
| 19:50:50 | <merijn> | Braindead specification of Enum, god awful Enum instance for Double, lack of API for safely handling over-/underflow in numerical conversions |
| 19:51:09 | <dminuoso> | Given `f :: a -> (Word32 -> P -> b) -> b`, I wanted to move `(Word32 -> P -> b) -> b` into a type alias, but that suddenly requires RankNTypes, is there a different route without demanding that extension everywhere? |
| 19:51:14 | <davean> | ∅? |
| 19:51:16 | <merijn> | The inability to mix qualified imports and import lists |
| 19:51:18 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 19:51:40 | <merijn> | dminuoso: "add a type variable to the alias"? |
| 19:51:40 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Read error: Connection reset by peer) |
| 19:51:45 | <dolio> | You can mix those, I think. |
| 19:51:48 | → | mananamenos joins (~mananamen@84.122.202.215.dyn.user.ono.com) |
| 19:51:58 | <merijn> | dolio: You can, but what that does is dumb as hell |
| 19:52:09 | <davean> | merijn: So I REALLY don't like our numerical tower. |
| 19:52:11 | <merijn> | dolio: That just means you only import those names qualified |
| 19:52:20 | <dolio> | Oh, I see what you mean. |
| 19:52:21 | <merijn> | davean: I don't like it, but fixing that is less obvious |
| 19:52:25 | × | mananamenos_ quits (~mananamen@84.122.202.215.dyn.user.ono.com) (Ping timeout: 264 seconds) |
| 19:52:28 | <merijn> | davean: So I'm willing to firgive that |
| 19:52:34 | <monochrom> | merijn: Are we listing a few warts of Haskell now? |
| 19:52:36 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 19:53:02 | <merijn> | dolio: Haskell would be so much better if I could write "import qualified Data.Map as M (Map)" and having "Map" imported unqualified :( |
| 19:53:11 | <davean> | merijn: I think theres a few obvious ones. It depends on if you're willing to evolve it (it doesn't seem we are) or insist on jumping to a perfect solution. |
| 19:53:33 | <merijn> | davean: I haven't seen any "improvements" that were "strictly better" |
| 19:53:33 | <monochrom> | I just have one to gripe about, all the others I really don't mind. This one: The tendency of the community to pretend that it is a dependently typed language. |
| 19:53:36 | <dolio> | I think most of the 'perfect solutions' are probably actually not that good. |
| 19:53:43 | <merijn> | monochrom: Oh, definitely |
| 19:53:47 | <merijn> | dolio++ |
| 19:54:04 | <davean> | merijn: well making it so most Num instances don't have undefineds ... |
| 19:54:05 | <dminuoso> | merijn: Mmm, I dont like that either. |
| 19:54:18 | <dolio> | They generally assume that borrowing dozens of mathematical classificationsn is good. |
| 19:54:19 | <monochrom> | Ah yeah that would be a nice feature merijn. |
| 19:54:19 | <merijn> | I don't want "mathematically accurate" I want "useful for practical things in the real world" :p |
| 19:54:26 | <dminuoso> | Ah, perhaps I can just stick it in a newtype, that would only require RankNTypes on the definition site |
| 19:54:55 | <merijn> | Who gives a fuck that double operations aren't associative? Just let me safely turn Int64 into Int32 in a remotely safe and sane way... |
| 19:55:30 | <monochrom> | But I think I have a better syntax. Here is the full form, and you can omit various parts: import Data.Map (Map, (!)) qualified as M (null, insert) |
| 19:55:49 | <merijn> | monochrom: That would require a change to the parser, etc. |
| 19:55:58 | <monochrom> | likewise for hiding, e.g., import Data.Map hiding (null) qualified as M hiding (insert) |
| 19:56:19 | <monochrom> | Yeah I know, but it is both more complete and less ambiguous |
| 19:56:20 | <merijn> | Qualified re-exports would be a killer feature too, tbh |
| 19:56:34 | <monochrom> | I mean s/less ambiguous/more guessable/ |
| 19:56:36 | <geekosaur> | but it's not an incompatible change |
| 19:56:40 | → | falafel joins (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) |
| 19:56:52 | <geekosaur> | I think qualified re-exports require help from the linker though |
| 19:56:54 | <merijn> | geekosaur: Which one? |
| 19:57:20 | <geekosaur> | monochrom's suggested import syntax |
| 19:57:31 | <merijn> | monochrom: Actually, I have a major objection to your proposed syntax |
| 19:58:11 | × | mananamenos quits (~mananamen@84.122.202.215.dyn.user.ono.com) (Ping timeout: 260 seconds) |
| 19:58:46 | <merijn> | monochrom: You violated the key principle (that IMO should be a core value in syntax design) of "accommodate a non-awkward way of linewrapping this when import lists get long..." |
| 19:58:49 | → | mananamenos joins (~mananamen@84.122.202.215.dyn.user.ono.com) |
| 19:58:59 | <dolio> | Didn't one of the recent versions add an option for 'qualified' later in the import? |
| 19:59:05 | <merijn> | Haskell's current syntax fails that horribly too |
| 19:59:27 | <merijn> | dolio: All that does is let you write "import Data.Map qualified" instead of "import qualified Data.Map" |
| 19:59:33 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:1c60:9ba4:8bf9:ee34) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 19:59:34 | <dolio> | Right, okay. |
| 19:59:35 | <davean> | merijn: Don't like int-cast? |
| 19:59:36 | <merijn> | gratuitously breaking all haskell source/parse thigns |
| 20:00:14 | <monochrom> | I think my proposal respects that principle. |
| 20:00:15 | <merijn> | davean: The fact that it's not built into Num is gross negligence |
| 20:00:39 | <merijn> | monochrom: How do you line wrap when the import list becomes, like, 10 entries long? |
| 20:00:55 | <davean> | merijn: but we don't have to build it into Num, and I don't think it makes sense to. A lot don't have sensible conversions? |
| 20:01:11 | <merijn> | davean: Also, no, int-cast's intCastMaybe isn't good enough |
| 20:01:47 | <merijn> | Ideally you have "intCastDynamic :: (Integral a, Integral b) => a -> Either (a, b) b" |
| 20:01:58 | <merijn> | i.e. don't just fail, give me the max possible value + remainder |
| 20:02:14 | <merijn> | That's much more useful |
| 20:02:28 | × | mastarija quits (~mastarija@93-136-96-155.adsl.net.t-com.hr) (Ping timeout: 265 seconds) |
| 20:02:39 | <monochrom> | https://paste.tomsmeding.com/Fxc7LZRQ |
| 20:02:51 | <merijn> | davean: We have fromIntegral in Num |
| 20:02:54 | <davean> | monochrom: its built in to https://hackage.haskell.org/package/base-4.13.0.0/docs/Data-Bits.html Because thats where it makes some sense. |
| 20:03:15 | <merijn> | eh, fromInteger, I mean |
| 20:03:32 | <merijn> | Why is having only an unsafe fromInteger better/more sensible then a checking variant? |
| 20:03:55 | <merijn> | monochrom: Yeah, that's a super ugly and awkward way to line wrap :p |
| 20:04:24 | <monochrom> | OK, what is a nicer way to line-wrap? |
| 20:04:29 | <davean> | merijn: why is "negate" there too? Because Num is broken. |
| 20:04:33 | <merijn> | I haven't thought of one yet |
| 20:04:52 | <merijn> | davean: Didn't you *just* say that "it's broken" wasn't a reason to not improve things? :p |
| 20:05:18 | <monochrom> | What is super ugly and awkward about it? |
| 20:05:23 | <davean> | merijn: yes, but you asked why "fromInteger" is there, I think "Num wasn't thought out, and is fundimentally broken" is the reason. |
| 20:05:42 | <merijn> | davean: "to convert numerical literals" is why |
| 20:05:55 | <merijn> | But converting numerical literals in a silently corrupting way is bad |
| 20:05:57 | <juri_> | davean: try looking at Rational sometime. |
| 20:05:57 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:d091:432d:3cee:b0b2) |
| 20:06:02 | <davean> | juri_: Trust me I have |
| 20:06:13 | <merijn> | Actually, what we *really* need is https://hackage.haskell.org/package/validated-literals built into base |
| 20:06:15 | <davean> | MOST of my problems programming Haskell these days come from our Numeric classes being wrong. |
| 20:06:23 | <merijn> | or rather, GHC |
| 20:06:27 | <davean> | You simply can't be generic in your number type with Haskell's tower. |
| 20:06:30 | → | unfixpoint joins (1f0a965a@31-10-150-90.cgn.dynamic.upc.ch) |
| 20:06:33 | <davean> | Because all the classes are just lies. |
| 20:06:34 | × | mirrorb2rd quits (~psutcliff@89.40.182.152) (Quit: Leaving) |
| 20:07:27 | <unfixpoint> | I'm having problems with some data type that uses RankNTypes.. I'm trying to abstract the way I connect to a database with holding `(Connection -> IO a) -> IO a` in a reader thing. |
| 20:07:39 | <unfixpoint> | I condensed the problem to this: https://pastebin.com/raw/geEHaeFk |
| 20:08:05 | <merijn> | unfixpoint: That's not a RankNType, that's an existential |
| 20:08:13 | × | SanchayanMaity quits (~Sanchayan@106.201.35.233) (Quit: SanchayanMaity) |
| 20:08:18 | <merijn> | Which means the forall is in the wrong place |
| 20:08:32 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 20:08:36 | <merijn> | Because it's current location already has an implicit one in haskell |
| 20:08:46 | <monochrom> | I'm pretty sure all you need is exposing the "a" as a type parameter. |
| 20:08:47 | <unfixpoint> | Though the errors slightly changed, now it says '(Connection -> IO a1) -> IO a1' cannot be matched with '(forall a. (Connection -> IO a) -> IO a)' but in the actual problem it is 'a' cannot matched 'a0' |
| 20:09:08 | <monochrom> | data R a = R ((Connection -> IO a) -> IO a) |
| 20:09:15 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 20:09:45 | <koz_> | Am I the only person who mis-spells Data.Vector's (!?) as (?!) all the time? |
| 20:10:12 | <monochrom> | Heh. Yesterday I kept misspelling "dictionary" as "directory". |
| 20:10:28 | × | dxld quits (~dxld@rush.pub.dxld.at) (Quit: Bye) |
| 20:10:30 | <koz_> | monochrom: Lol... some similarities there for sure. |
| 20:10:50 | <merijn> | unfixpoint: Anyway, RankN isn't what you want here, you either want existential quantification or just a parametric 'R' as monochrom suggests |
| 20:10:52 | <unfixpoint> | monochrom: Not sure if it will work? |
| 20:11:29 | <unfixpoint> | But when I write it GHC yelled at me I should be using RankN. Is Existential implied by RankN |
| 20:11:31 | <unfixpoint> | ? |
| 20:11:59 | <merijn> | No, they're different things |
| 20:12:06 | → | gumbish joins (4913050a@c-73-19-5-10.hsd1.wa.comcast.net) |
| 20:12:25 | <merijn> | unfixpoint: "GHC tells you to enable extension X" is only loosely correlated with "actually needing/wanting X" |
| 20:12:31 | <monochrom> | That's an XY problem. |
| 20:12:48 | <merijn> | unfixpoint: GHC guess you need RankN from what you *wrote*, not from what you *want* |
| 20:13:00 | <monochrom> | Are you an expert? Because GHC suggestions assume you're an expert and you merely made a typo. |
| 20:13:11 | → | dxld joins (~dxld@80-109-136-248.cable.dynamic.surfer.at) |
| 20:13:25 | <gumbish> | XY problem? |
| 20:13:29 | → | Boomerang joins (~Boomerang@xd520f68c.cust.hiper.dk) |
| 20:13:37 | <tomjaguarpaw> | I think that's a YX problem. |
| 20:13:39 | → | rekahsoft joins (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) |
| 20:13:42 | <monochrom> | It never realizes that 99% of these errors are because you made a wrong design and you tried an overkill. |
| 20:13:45 | <merijn> | gumbish: https://xyproblem.info/ |
| 20:13:48 | <unfixpoint> | monochrom: I'm not trying to argue this, not an expert |
| 20:14:15 | <unfixpoint> | tomjaguarpaw: What do I actually want to do? |
| 20:14:17 | <geekosaur> | ghc has to guess what you intended from what you wrote. In this case its guess was wrong |
| 20:14:22 | × | AlterEgo- quits (~ladew@124-198-158-163.dynamic.caiway.nl) (Quit: Leaving) |
| 20:15:37 | <merijn> | unfixpoint: That depends what your intention for 'R' is |
| 20:15:38 | <geekosaur> | It doesn't try very hard because it can't really know what you intended, it just went by what would make what you wrote syntactically correct. But only syntactically, not semantically |
| 20:16:54 | <unfixpoint> | The 'R' basically holds information how to connect among other things (ie. has other fields as well) |
| 20:17:31 | <merijn> | unfixpoint: Right, but why does the 'a' have to be hidden? Why does monochrom's suggestion of just writing 'R a' not work? |
| 20:17:43 | <unfixpoint> | I could in theory have a `data R = R { connectInfo :: (Host,Port,Creds) , ... }` actually |
| 20:18:01 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 2.9) |
| 20:18:31 | hackage | haveibeenpwned 0.2.0.0 - Library for checking for weak/compromised passwords. https://hackage.haskell.org/package/haveibeenpwned-0.2.0.0 (abrar) |
| 20:18:50 | → | AlterEgo- joins (~ladew@124-198-158-163.dynamic.caiway.nl) |
| 20:18:54 | <unfixpoint> | It was a question, I'm not sure whether it will work. |
| 20:19:33 | × | idhugo quits (~idhugo@80-62-116-101-mobile.dk.customer.tdc.net) (Ping timeout: 260 seconds) |
| 20:19:36 | <merijn> | unfixpoint: You can certainly do *that*, because I have, but that sounds more like something where you'll want existentials, depending on the exact design |
| 20:19:50 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 20:20:22 | <unfixpoint> | geekosaur: I'm sure someone meant well with those error messages (probably a lot of work), but maybe it should only try what is possible or make sure that the error is actually what it says. |
| 20:20:28 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 20:20:44 | <merijn> | the error is what it is, the suggested fix isn't always |
| 20:20:50 | <unfixpoint> | merijn: I see, I'll try where I get from here. |
| 20:21:07 | <monochrom> | This is why IMO such "helpful" hints are evil. |
| 20:21:11 | <merijn> | unfixpoint: I like to call that "OO" Haskell |
| 20:21:26 | <monochrom> | And I say that the poeple who promoted those hints are do-gooders. |
| 20:21:30 | hackage | haveibeenpwned 0.2.0.1 - Library for checking for weak/compromised passwords. https://hackage.haskell.org/package/haveibeenpwned-0.2.0.1 (abrar) |
| 20:21:31 | <unfixpoint> | Wait, why OO-Haskell? |
| 20:21:33 | <merijn> | unfixpoint: persistent uses it, so maybe you wanna have a alook at what they do |
| 20:22:08 | <merijn> | unfixpoint: Because having a datatype that exposes abstract API that you can use without knowing its internals is basically just OO interfaces? :) |
| 20:22:32 | <dminuoso> | Unsure what that has to do with "object oriented" though |
| 20:22:40 | <dminuoso> | That's just encapsulation. :) |
| 20:22:44 | → | Deide joins (~Deide@217.155.19.23) |
| 20:22:46 | <unfixpoint> | I guess that's true, yeah. I always considered typeclasses as that |
| 20:23:00 | × | rekahsoft quits (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Remote host closed the connection) |
| 20:23:30 | <merijn> | unfixpoint: I find typeclass rather "entirely unlike OO" the more you consider them :) |
| 20:23:43 | <merijn> | unfixpoint: You might wanna look at this and the code that uses it to get inspiration? https://github.com/yesodweb/persistent/blob/a819276a883b89ac898bf61ff7a1cc8a8bf3cd50/persistent/Database/Persist/Sql/Types/Internal.hs#L79-L181 |
| 20:23:59 | <unfixpoint> | The interface part though. |
| 20:24:06 | <dminuoso> | merijn: Arguably, the core theme that makes OO OO, is one of two things. It's either smalltalk-esque message passing, or its subtyping. Or a combination of both. The "methods" and "internals/externals" is just language ergonomics that has nothing to do with object orientation. |
| 20:24:23 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 20:24:24 | <unfixpoint> | merijn: ty! |
| 20:24:36 | <merijn> | unfixpoint: And how it gets used: https://github.com/yesodweb/persistent/blob/master/persistent-sqlite/Database/Persist/Sqlite.hs#L222-L278 |
| 20:24:44 | → | rekahsoft joins (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) |
| 20:25:00 | <dminuoso> | That is, whether you write `f->g()`, `f.g()`, `f(g)`, `g f` these are just visual considerations, trying to nudge your thinking into one direction |
| 20:25:10 | <boxscape> | it's weird, sometimes programming with type families actually feels more convenient than with regular functions, because they already support visible dependent as well as relevant quantification without Singletons |
| 20:25:50 | <boxscape> | Though I imagine I'll lose that feeling once I actually start writing term-level functions that use these type families .... |
| 20:25:50 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) |
| 20:27:16 | × | knupfer quits (~Thunderbi@i5E86B4DB.versanet.de) (Ping timeout: 240 seconds) |
| 20:28:09 | <unfixpoint> | Not sure if he's right (he was kind of arrogant) but my prof claimed the invention of *information hiding* and his language (Eiffel) sure was/is OO |
| 20:28:41 | <unfixpoint> | Then again just because an XY-language introduces a feature doesn't mean it's inherent to XY-languages |
| 20:28:47 | <boxscape> | OO means many different things to different people, especially the person who came up with the term |
| 20:28:49 | <ski> | abstract data types is also about "information hiding" (and is different from OO) |
| 20:29:11 | <dminuoso> | unfixpoint: information hiding can appear at many different levels. it can happen across systems, architecturally, across libraries, modules |
| 20:30:07 | × | luto1 quits (~luto@84.39.117.57) (Ping timeout: 256 seconds) |
| 20:30:17 | <ski> | with parametric polymorphism and type classes, you can say `maximum :: Ord a => [a] -> a'. you can't really say that, with OO |
| 20:30:37 | <dminuoso> | Well.. you can.. |
| 20:31:00 | <dminuoso> | elixir protocols explore that mixture |
| 20:31:30 | <ski> | with bounded polymorphism, you can say something akin to that. but that's assuming you also have (bounded) parametric polymorphism |
| 20:31:39 | <unfixpoint> | interface Ordering<X> { maximum :: List<X> -> X } or something. I haven't OO'ed for a while |
| 20:31:45 | × | AlterEgo- quits (~ladew@124-198-158-163.dynamic.caiway.nl) (Quit: Leaving) |
| 20:31:57 | <ski> | right, the `<X>' there implies parametric polymorphism |
| 20:32:28 | <unfixpoint> | Lol true, so which OO-language doesn't have parametric polymorphism then? |
| 20:32:40 | <dminuoso> | C++ for starters |
| 20:32:43 | <merijn> | unfixpoint: Some do (in some forms) |
| 20:32:56 | <monochrom> | The <X> was definitely alien to OO. |
| 20:32:58 | <merijn> | unfixpoint: Java/C# generics are (basically) parametric polymorphism |
| 20:32:59 | <dminuoso> | The existence of template specializations puts a nail into that coffin. |
| 20:33:28 | <merijn> | oh, wait, the question was "which doesn't" |
| 20:33:36 | <merijn> | Python :p |
| 20:33:50 | <dolio> | Java didn't have it until version 5. |
| 20:34:19 | <monochrom> | Java learned <X> from Wadler's Pizza. Not even from C++. |
| 20:34:20 | <boxscape> | seems kind of weird to even ask the question of whether a language without static typing has parametric polymorphism |
| 20:34:35 | <ski> | OO bundles methods with an object. type classes doesn't do that |
| 20:34:38 | <boxscape> | It's quite possible that the correct answer is "no" but it almost feels to me like it should be "undefined" |
| 20:34:39 | <monochrom> | perhaps apart from borrowing the notation |
| 20:35:30 | <monochrom> | A dynamically typed language has maximum polymorphism and non-existent parametric. |
| 20:35:42 | <boxscape> | I see |
| 20:36:00 | <monochrom> | (To remind you that there are many different, conflicting polymorphisms, too.) |
| 20:36:09 | <dminuoso> | unfixpoint: Also recall, there's two different notions of "object-oriented". One is the heritage ranging all the way back to smalltalk, and the other with simula (they both have possibly more ancient ancestors) |
| 20:36:28 | <ski> | @where on-understanding |
| 20:36:28 | <lambdabot> | "On Understanding Types, Data Abstraction, and Polymorphism" by Luca Cardelli,Peter Wegner in 1985-12 at <http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf> |
| 20:37:16 | <dminuoso> | Often nowadays people understand it as the second, as class with inheritance and everything that belongs to it, though the original idea largely influenced by Alan Kay and others is more about message passing. |
| 20:38:11 | <dminuoso> | Very broadly where program parts are conceptual objects with internal state, exchanging messages and thus interacting with each other |
| 20:38:32 | <dminuoso> | A style certainly not respected by Java enthusiasts as much |
| 20:38:34 | <boxscape> | https://i.imgur.com/iag7eoN.png |
| 20:38:36 | <unfixpoint> | I understand it as the latter then, message passing is separate to me. But I'm young it seems (certainly did I never program in Java 5) |
| 20:40:29 | <ski> | given `interface Counter { int tick(); void reset(); }' in Java, the object type `Counter' corresponds in Haskell to `exists a. Counter a *> a', assuming `class Counter a where tick :: a -> IO Int; reset :: a -> IO ()', alternatively corresponds to `exists a. (a,a -> IO Int,a -> IO ())' |
| 20:40:30 | × | kritzefitz_ quits (~kritzefit@212.86.56.80) (Read error: Connection reset by peer) |
| 20:40:35 | → | knupfer joins (~Thunderbi@200116b8244bd600401750fffecef6b8.dip.versatel-1u1.de) |
| 20:40:53 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 20:40:54 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Client Quit) |
| 20:41:00 | <dolio> | You can tell most OO folks don't care about the smalltalk perspective, because if they did, they'd be all about proper tail calls. |
| 20:41:02 | × | knupfer quits (~Thunderbi@200116b8244bd600401750fffecef6b8.dip.versatel-1u1.de) (Remote host closed the connection) |
| 20:41:05 | × | rekahsoft quits (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Ping timeout: 240 seconds) |
| 20:41:08 | × | nuncanada quits (~dude@179.235.160.168) (Ping timeout: 260 seconds) |
| 20:41:14 | <dolio> | Instead they use loops they borrowed from C. |
| 20:41:15 | → | knupfer joins (~Thunderbi@200116b8244bd600690e470b1c9f0b95.dip.versatel-1u1.de) |
| 20:42:11 | <ski> | `exists a. Counter a *> a' expresses "bundling methods with object state". but in Haskell, we can also express e.g. `exists a. (Ord a,Widget a) *> [a]' where we bundle not an individual object with methods, but rather attach them to a whole collection of objects |
| 20:44:09 | <ski> | (in the case of `exists a. (a,a -> IO Int,a -> IO ())', a shorter way (normally implemented by closures) to express this is `(IO Int,IO ())' .. but this method of removing the existential doesn't always work, e.g. if some method take multiple `a's as input (so-called "binary methods", like a comparision. also see "clone methods")) |
| 20:45:05 | <unfixpoint> | Why *> instead of =>? Never used the singletons but in this case is it not the same? |
| 20:45:19 | <ski> | not at all the same, rather the "opposite" |
| 20:46:20 | <boxscape> | does it actually have to do with singletons? |
| 20:46:21 | <unfixpoint> | So given [a] we can Ord and Widget it? Instead of Given that we can Ord, Widget an a we have [a]? Wat? |
| 20:47:01 | <unfixpoint> | Idk, I didn't know (*>) as type operator so I looked it up on Hoogle |
| 20:47:09 | <dminuoso> | unfixpoint: It's not, it's pseudo haskell |
| 20:47:26 | <ski> | if you have `foo :: Blah => ...', then the caller/consumer/user of `foo' must provide evidence of `Blah', before being able to call/use `foo' (with type `...'). and the callee/implementor/producer of `foo' can simply take the evidence of `Blah' for granted, can e.g. call methods (and other operations relying on those methods) from `Blah' |
| 20:47:30 | <boxscape> | (the singletons version is just the lifted version of Applicative's *>) |
| 20:47:37 | <dminuoso> | If we had exists in addition to forall, then it'd make sense to have a *> variant of => instead |
| 20:48:05 | <dminuoso> | Not even sure who introduced the syntax of *>, but I wouldn't be surprised if it was ski themselves. :) |
| 20:48:17 | <monochrom> | It's related to: "for all positive x, P(x)" = "for all x, positive x implies P(x)", but "for some positive x, P(x)" = "for some x, positive x and P(x)" |
| 20:48:44 | <monochrom> | You simply don't use "implies" in the existential version. |
| 20:48:45 | → | conal joins (~conal@64.71.133.70) |
| 20:49:22 | <ski> | if you have `foo :: Blah *> ...', then the callee/producer/implementor of `foo' can simply take the evidence of `Blah' for granted (and also use the value of type `...'). but the caller/user/consumer of `foo' must produce evidence of `Blah' (together with constructing a value of type `...') |
| 20:49:27 | <ski> | dminuoso : yes |
| 20:49:50 | × | falafel quits (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) (Ping timeout: 264 seconds) |
| 20:50:18 | <monochrom> | So given that "and" is somewhat analogous to multiplication, and it would be nice to keep the ">" part, some of us chose the pseudocode *> notation. |
| 20:50:30 | × | Franciman quits (~francesco@host-82-56-223-169.retail.telecomitalia.it) (Quit: Leaving) |
| 20:50:43 | <ski> | the distinction `Blah => ...' vs. `Blah *> ...' is similar to the distinction `T -> U' vs. `(T,U)', and the distinction `forall a. ..a..' vs. `exists a. ..a..' |
| 20:51:06 | <boxscape> | can you encode *> analogously to how you can encode exists? |
| 20:51:20 | <ski> | and yes, this `*>' is just pseudo-code that some of us sometimes use to express this "dual" concept to `=>' |
| 20:51:31 | hackage | phonetic-languages-examples 0.6.1.0 - A generalization of the uniqueness-periods-vector-examples functionality. https://hackage.haskell.org/package/phonetic-languages-examples-0.6.1.0 (OleksandrZhabenko) |
| 20:51:55 | <dminuoso> | boxscape: Sure, as we can encode exists with forall. |
| 20:52:06 | <boxscape> | okay, neat |
| 20:52:07 | <dminuoso> | boxscape: So in that encoding => takes the role of *> |
| 20:52:16 | <boxscape> | oh, that's pretty straightforward |
| 20:52:21 | → | dragestil joins (~quassel@fsf/member/dragestil) |
| 20:53:07 | <ski> | yes, you can write `data cxt *> a = cxt => Provide a' alternatively `data cxt *> a where Provide :: cxt => a -> cxt *> a' |
| 20:53:12 | <monochrom> | Like this? "data X = forall a. Show a => X [a]" becomes "forall a. Show a => ([a] -> c) -> c" |
| 20:53:22 | <ski> | (compare `Provide' with `(,) :: a -> b -> (a,b)') |
| 20:53:26 | × | crdrost quits (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) (Quit: This computer has gone to sleep) |
| 20:53:32 | <monochrom> | Now, allow me to replace => by ->. Hell, there was a GHC version that did this by mistake. >:) |
| 20:53:55 | <monochrom> | "forall a. Show a -> ([a] -> c) -> c |
| 20:54:14 | <monochrom> | "forall a. (Show a, [a] -> c) -> c" |
| 20:54:28 | <ski> | a value of type `cxt *> a' is like a pair of evidence for (a "dictrionary"/"vtable" for) `cxt', together (bundled) with a value of type `a' |
| 20:55:19 | → | pavonia joins (~user@unaffiliated/siracusa) |
| 20:55:27 | <boxscape> | monochrom do you mean this (timestamped) video rae uploaded a few days ago where it happened or a much older ghc version? https://youtu.be/l5veKgGxXd4?t=262 |
| 20:55:45 | <boxscape> | or, let's say, the bug in this video or a bug from an older ghc version |
| 20:55:46 | <dminuoso> | boxscape: Note, the above things are mashed into the library `constraints` with slightly altered ergonomics |
| 20:55:52 | <geekosaur> | much older version |
| 20:55:55 | <ski> | unfixpoint : makes any sense ? |
| 20:55:55 | <boxscape> | ah, that library keeps coming up |
| 20:56:09 | <boxscape> | geekosaur I see |
| 20:56:33 | <unfixpoint> | Not yet |
| 20:56:36 | <monochrom> | Yeah, a few years ago. |
| 20:56:41 | <unfixpoint> | I'll re-read |
| 20:56:59 | × | Aquazi quits (uid312403@gateway/web/irccloud.com/x-dkkwvspwitpqcrse) (Quit: Connection closed for inactivity) |
| 20:57:14 | <monochrom> | I don't know whether that video uses the GHC version I have in mind. Too lazy to check. |
| 20:57:31 | <dminuoso> | boxscape: Roughly, constraints just gives you a bare data: Dict :: Constraint -> * where Dict :: a => Dict a |
| 20:57:39 | <boxscape> | monochrom it uses something pretty close to HEAD so you've answered the question with your previous comment :) |
| 20:57:42 | <monochrom> | But certainly not >= 8.6 when I noticed it. |
| 20:57:51 | <dminuoso> | (So it comes with *just* the constraint, not the value ski used above) |
| 20:58:12 | <boxscape> | dminuoso I see |
| 20:58:31 | <dminuoso> | And it turns out GHC has this cool behavior that when you pattern match on that, the dictionary is brought into scope and it can be used to discharge obligations for it |
| 20:58:58 | <boxscape> | right, that's what we talked about earlier today when I wasn't able to do it in a type class :) |
| 20:59:04 | <boxscape> | type family |
| 20:59:04 | <boxscape> | rather |
| 20:59:16 | <ski> | unfixpoint : `forall' vs. `exists' flips the rôle of caller/user/consumer and the rôle of callee/implementor/producer. with `forall a. ..a..', the caller picks the type to use in place of `a', while the callee have to make do with whatever choise was made (can't even know, in general, which choice was made). with `exists a. ..a..' the callee picks the concrete type that is forgotten, hidden by `a', |
| 20:59:22 | <ski> | and the caller has to be prepared for any choice (and can't know which was chosen, in general) |
| 21:00:23 | <dminuoso> | boxscape: The old version has this cool and mindboggingly simple implementation of: |
| 21:00:32 | <dminuoso> | withDict :: Dict a -> (a => r) -> r; withDict d r = case d of Dict -> r |
| 21:00:33 | <unfixpoint> | It makes sense but why does one end up needing a library like `constraints` |
| 21:00:55 | <dminuoso> | Which might look like magic at first glance. :) |
| 21:01:14 | <boxscape> | does look fairly strange, yeah |
| 21:01:42 | <boxscape> | but I think it makes sense to me |
| 21:02:01 | <ski> | unfixpoint : similarly, `cxt => a' vs. `cxt *> a' also flips that rôle, wrt how `cxt' is treated. with `=>', the caller has to provide evidence of `cxt', and the callee can just assume the evidence will be provided to it. with `*>', the callee has to provide the evidence for `cxt', while the caller can rely on it being given / handed to it, along with the value |
| 21:02:27 | <unfixpoint> | I imagine these are ad-hoc solutions to the crappy module system? |
| 21:03:20 | <dminuoso> | It's quite surprising that constraints has *that* many downloads.. |
| 21:03:47 | <ski> | @where on-understanding-revisited |
| 21:03:47 | <lambdabot> | "On Understanding Data Abstraction, Revisited" by William R. Cook in 2009-10 at <http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf> |
| 21:04:15 | <ski> | has a discussion on OO vs. Abstract Data Types (and mentions relation of both to existentials), iirc |
| 21:05:52 | → | moth joins (~moth@s91904426.blix.com) |
| 21:06:12 | <p0a> | I was told to look into ExceptT |
| 21:06:14 | <ski> | unfixpoint : "So given [a] we can Ord and Widget it? Instead of Given that we can Ord, Widget an a we have [a]? Wat?" -- having a value of type `exists a. (Ord a,Widget a) *> [a]' means that you have a list of values of some (common) unknown/forgotten/hidden type `a', about which you only know that it's an instance of `Ord' and `Widget' (so you can only really process the values in the list, by passing them |
| 21:06:20 | <ski> | to the methods of those two type classes) |
| 21:06:26 | <p0a> | is it from mtl or transformers? |
| 21:07:16 | <dminuoso> | p0a: mtl provides Monad* typeclasses, transformers provides *T type constructors. |
| 21:07:21 | <dminuoso> | Though mtl re-exports some of transformers. |
| 21:07:25 | <ski> | unfixpoint : otoh, `exists a. (Ord a,Widget a) => [a]' would be very different. you'd still have a list of values of a (common) unknown type, but now, to be able to access them, you must now magically somehow conjure up `Ord' and `Widget' instances (for this type `a' that you know nothing about) .. i hope you can see that this is fairly useless |
| 21:07:36 | <p0a> | dminuoso: got it, thank you |
| 21:08:07 | → | crdrost joins (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) |
| 21:08:29 | → | boxscape59 joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 21:09:09 | <hekkaidekapus> | idnar: Now that I got a real machine handy, take a look at this: <https://paste.tomsmeding.com/llmymcm4>. |
| 21:10:06 | → | Franciman joins (~francesco@host-82-56-223-169.retail.telecomitalia.it) |
| 21:10:14 | × | Klobbinger quits (543b08ef@dslb-084-059-008-239.084.059.pools.vodafone-ip.de) (Remote host closed the connection) |
| 21:10:30 | <unfixpoint> | Yeah, I wouldn't know when I'd need that |
| 21:11:50 | <ski> | `*>' typically goes with `exists', like `=>' typically goes with `forall' |
| 21:12:46 | <unfixpoint> | By typically you mean freenode#haskell or in general (eg. research)? |
| 21:12:49 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Ping timeout: 264 seconds) |
| 21:13:01 | × | crdrost quits (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) (Quit: This computer has gone to sleep) |
| 21:13:18 | <dminuoso> | Mmm, how many other languages have type systems involving quantification and constraints? |
| 21:13:56 | <ski> | Clean,Mercury |
| 21:14:40 | <dminuoso> | unfixpoint: Note, this exists and *> is not even Haskell. It's just a pseudo haskell some of us pretend existed. |
| 21:15:08 | <ski> | unfixpoint : by "typically", i mean that, in practice, most of the times you'd want to express `*>', is in direct conjunction with expressing `exists'; and most of the times you want `=>', it's in direct conjunction with `forall' |
| 21:15:30 | hackage | graphula 2.0.0.1 - A declarative library for describing dependencies between data https://hackage.haskell.org/package/graphula-2.0.0.1 (PatrickBrisbin) |
| 21:15:40 | <dminuoso> | ski: Mm, can you actually express the `exists a. (Ord a,Widget a) => [a]` confusion with a forall encoding? |
| 21:15:48 | <dminuoso> | (that is the forall continuation encoding) |
| 21:16:01 | <dminuoso> | Ah I think you should be able to |
| 21:16:28 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 21:16:33 | <dminuoso> | presumably it'd be: (forall a. [(Ord a, Widget a) => a] -> b) -> b |
| 21:16:33 | <ski> | and yes, `exists' and `*>' are not valid Haskell (even with extensions) (maybe we'll get `exists', some day. there was another Haskell implementation which had limited support for it). regardless, imho, it's useful to reason in terms of `exists' and `*>', in pseudo-Haskell code, before getting to encoding it (in one of two main ways), in Haskell (with extensions) |
| 21:16:38 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 21:16:54 | <dminuoso> | or... no that doesnt look quite right |
| 21:17:00 | × | dhouthoo quits (~dhouthoo@ptr-eiv6509pb4ifhdr9lsd.18120a2.ip6.access.telenet.be) (Quit: WeeChat 2.9) |
| 21:17:04 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 21:17:14 | <ski> | dminuoso : not sure what you mean by "express the [..] confusion" |
| 21:17:27 | <dminuoso> | ski: `exists a. (Ord a,Widget a) => [a]` |
| 21:17:42 | <ski> | what is the confusion that you want to express ? |
| 21:17:50 | <dminuoso> | ski: Can you express that term in haskell with forall |
| 21:17:58 | <ski> | (or do you just mean to express that type, in Haskell with extensions ?) |
| 21:18:01 | <dminuoso> | Right |
| 21:18:09 | <dminuoso> | All extensions allowed. |
| 21:18:13 | <ski> | exists a. (Ord a,Widget a) => [a] |
| 21:18:30 | × | unfixpoint quits (1f0a965a@31-10-150-90.cgn.dynamic.upc.ch) (Remote host closed the connection) |
| 21:18:30 | <ski> | = forall o. ((exists a. (Ord a,Widget a) => [a]) -> o) -> o |
| 21:18:46 | <ski> | = forall o. (forall a. ((Ord a,Widget a) => [a]) -> o) -> o |
| 21:19:12 | <ski> | (that's using `RankNTypes') |
| 21:19:13 | <dminuoso> | Ah indeed. |
| 21:19:33 | → | dcoutts_ joins (~duncan@33.14.75.194.dyn.plus.net) |
| 21:19:36 | → | unfixpoint joins (1f0a965a@31-10-150-90.cgn.dynamic.upc.ch) |
| 21:19:48 | <dminuoso> | Oh! And thus answering a question that arised over a year ago, for which I never got a satisfactory answer |
| 21:19:54 | <ski> | oh ? |
| 21:20:56 | <dminuoso> | Don't even know the context, but I was wondering about the meaning of `forall a. (ctxt ... => ...)` as opposed to `forall a. ctxt ... => ...` |
| 21:22:12 | <dexterfoo> | foldr (\i m -> Map.insert i "value" m) Map.empty [1..100] |
| 21:22:13 | <dexterfoo> | Should i use foldr or foldl'? The Map is strict |
| 21:22:48 | × | boxscape59 quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed) |
| 21:22:55 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 21:23:02 | <ski> | dminuoso : er, the precedence i'm using, those two should be the same thing |
| 21:23:11 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 21:23:37 | <Guest42> | Hi, I have a lambda calucus question. I have to show that if s ⇒βi |
| 21:23:37 | <Guest42> | s' and s' is in head normal form then s is also in head normal form. Can someone help ? |
| 21:23:44 | <ski> | ("quantifiers extend/scopes as far right as possible") |
| 21:25:34 | <ski> | ⌜⇒βi⌝ being ? |
| 21:26:29 | <dminuoso> | ski: Mmm. Im having a hard time remembering it might have been 2 years ago in fact, my logs dont reach that far back. |
| 21:27:32 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:b570:65da:9eeb:ab03) (Ping timeout: 260 seconds) |
| 21:27:55 | × | borne quits (~fritjof@200116b864880600f1dc39039d201adf.dip.versatel-1u1.de) (Ping timeout: 272 seconds) |
| 21:28:15 | <boxscape> | dminuoso do you remember if ctxt is supposed to depend on a? |
| 21:28:17 | <dminuoso> | Roughly, I was looking into where forall and => could go, and there were some combinations I just couldn't make sense of |
| 21:28:31 | <dminuoso> | Similar to, but not quite like: withDict :: HasDict c e => e -> (c => r) -> r |
| 21:28:54 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 21:29:32 | <ski> | ok |
| 21:29:51 | <ski> | (boxscape : presumably ?) |
| 21:29:56 | <Guest42> | =>βi is the smallet relation that is reflexive and s.t if s => s' then λx.s ⇒β λx.s |
| 21:29:56 | <Guest42> | , |
| 21:30:03 | <Guest42> | and if |
| 21:30:27 | <boxscape> | I was thinking maaaybe it could have been forall a . ctxt ... => ... vs cxt => forall a . ..., but of course that wouldn't make sense in that case |
| 21:30:34 | <dminuoso> | It arised from the question whether: (Show a => a -> IO ()) -> IO () was the same as forall a. (Show a => a -> IO ()) -> IO () |
| 21:30:39 | <Guest42> | s ⇒β s |
| 21:30:39 | <Guest42> | and t ⇒β t |
| 21:30:40 | <Guest42> | alors s t ⇒β s |
| 21:30:40 | <Guest42> | 0 |
| 21:30:41 | <Guest42> | t |
| 21:30:41 | <dminuoso> | That was the story, and my logs do reach that far. :) |
| 21:30:41 | <Guest42> | 0 |
| 21:30:42 | <Guest42> | et (λx.s)t ⇒β s |
| 21:30:42 | <Guest42> | 0 |
| 21:30:43 | <Guest42> | [t |
| 21:30:43 | <Guest42> | 0/x |
| 21:30:45 | × | cads quits (~cads@ip-64-72-99-232.lasvegas.net) (Ping timeout: 256 seconds) |
| 21:30:57 | <dminuoso> | Guest42: please use a pasting service, you can find one linked in the topic |
| 21:31:06 | <tomsmeding> | copying from a pdf? ;) |
| 21:31:06 | → | borne joins (~fritjof@200116b864880600f1dc39039d201adf.dip.versatel-1u1.de) |
| 21:31:12 | <Guest42> | yeah |
| 21:31:13 | <ski> | dminuoso : definitely not the same |
| 21:32:00 | hackage | phonetic-languages-examples 0.6.2.0 - A generalization of the uniqueness-periods-vector-examples functionality. https://hackage.haskell.org/package/phonetic-languages-examples-0.6.2.0 (OleksandrZhabenko) |
| 21:32:50 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Quit: cosimone) |
| 21:32:51 | → | nuncanada joins (~dude@179.235.160.168) |
| 21:32:51 | <boxscape> | % testing42 :: (Show a => a -> IO ()) -> IO (); testing42 = undefined |
| 21:32:52 | <yahb> | boxscape: |
| 21:32:54 | <boxscape> | % :t +v testing42 |
| 21:32:54 | <yahb> | boxscape: forall a. (Show a => a -> IO ()) -> IO () |
| 21:32:59 | <boxscape> | is that not the second one? |
| 21:33:17 | <boxscape> | seems like ghc infers them to be the same? |
| 21:33:29 | <boxscape> | s/infer/does something to them |
| 21:33:52 | <ski> | Guest42 : hm, so beta-reducing some number of parallel subexpressions (including reducing under lambda) |
| 21:34:55 | <ski> | boxscape : in that context, the former is interpreted to have an implicit/elided `forall', and so is equivalent to the latter (with some caveats like `ScopedTypeVariables' ..) |
| 21:35:22 | <boxscape> | ski so that means the context in dminuoso's question was implied to be different? |
| 21:35:44 | <ski> | boxscape : but consider `data Foo a = MkFoo {testing42 :: (Show a => a -> IO ()) -> IO ()}' vs. `data Foo a = MkFoo {testing42 :: forall a. (Show a => a -> IO ()) -> IO ()}' -- these are not the same |
| 21:35:53 | <boxscape> | ah, that's fair |
| 21:35:53 | <unfixpoint> | I will never understand how ScopedTypeVariables is not default |
| 21:35:59 | → | alp joins (~alp@2a01:e0a:58b:4920:7462:8d66:154:f167) |
| 21:36:03 | <koz_> | unfixpoint: Because Haskell2010 doesn't have it. |
| 21:36:06 | <dminuoso> | unfixpoint: historical reasons. |
| 21:36:09 | <dolio> | dminuoso: Those types are the same. |
| 21:36:13 | <unfixpoint> | Yeah, I know.. but wtf |
| 21:36:16 | <koz_> | dminuoso: Was about to say 'hysterical raisins'. |
| 21:36:17 | <ski> | `(Show a => a -> IO ()) -> IO ()' is a type expression with a free (type) variable. `forall a. (Show a => a -> IO ()) -> IO ()' isn't |
| 21:36:19 | → | cads joins (~cads@ip-64-72-99-232.lasvegas.net) |
| 21:36:31 | <dminuoso> | dolio: I know |
| 21:36:32 | <koz_> | unfixpoint: Hysterical raisins is an explanation of many wtf phenomena, Haskell or otherwise. |
| 21:36:39 | <dolio> | Oh, okay. |
| 21:36:43 | <boxscape> | apparently there's some infelicities with ScopedTypeVariables that, if the stars align just right, might be fixed before something like it becomes standard, but I don't quite remember what they were |
| 21:36:44 | <Guest42> | => is the beta parrallell reduction |
| 21:36:49 | <ski> | imho, the behaviour of `ScopedTypeVariables' is the opposite of what it ought to be .. |
| 21:36:56 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Ping timeout: 240 seconds) |
| 21:37:00 | <dminuoso> | dolio: I copied the line that, roughly, was at the starting point of all of this. |
| 21:37:08 | <dminuoso> | % foo :: forall a. (Show a => a -> IO ()) -> IO (); foo = undefined |
| 21:37:08 | <yahb> | dminuoso: |
| 21:37:10 | <ski> | Guest42 : single-parallel-step, yes |
| 21:37:14 | <dminuoso> | % bar :: (forall a. Show a => a -> IO ()) -> IO (); bar = undefined |
| 21:37:14 | <yahb> | dminuoso: |
| 21:37:25 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 21:37:38 | <Guest42> | ski: i think the i notes how many steps |
| 21:37:42 | <unfixpoint> | At least it makes me crack up everytime because I always misspell it. So it will suggest me NoScopedTypevariables too. I don't even play video games but I know about no scoping >.> |
| 21:37:45 | <Guest42> | but i'm not sure |
| 21:38:30 | <dexterfoo> | any help with my question about foldr/foldl'? |
| 21:38:36 | <ski> | Guest42 : hm, just noticed the ⌜i⌝ isn't there in what you wrote after "the smallet relation that" |
| 21:39:02 | <Guest42> | yeah beause I think I made a mistake |
| 21:39:21 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:8c9:42ac:c0f6:8508) |
| 21:39:38 | × | knupfer quits (~Thunderbi@200116b8244bd600690e470b1c9f0b95.dip.versatel-1u1.de) (Ping timeout: 264 seconds) |
| 21:40:23 | <Guest42> | I have to write what it is in a paste website thing. I'll send the link once I'm finished |
| 21:41:02 | <unfixpoint> | Use foldl' as you want to fold everything, but you could also just use fromList I think. |
| 21:41:16 | <ski> | boxscape : imho, with `foo :: forall a. ..a..; foo = ...', the `a' bound by `forall a.' in the signature ought not to be in scope in the body `...'; while with `foo :: ..a..; foo = ...' (and an extension), it could make sense for `a' to be in scope in `...' |
| 21:41:51 | <dminuoso> | dexterfoo: hard to say in general without knowing the details |
| 21:41:59 | <c_wraith> | dexterfoo: foldl', for two reasons. 1) there's no meaningful result from evaluating just some of the list. 2) The result is a single value that you want to not have referring to previous versions of itself |
| 21:42:27 | <dminuoso> | dexterfoo: Roughly, foldr is a good and safe default (because of how it plays with lazyness), foldl' is more rarely a better choice unless you know you will force the entire structure anyway. |
| 21:42:55 | <dexterfoo> | dminuoso: thank you. i pasted a line of code that builds a Strict Map |
| 21:42:59 | <c_wraith> | dexterfoo: and FWIW, in that case the fact that it's Data.Map.Strict is irrelevant. It will do the exact same thing with Data.Map.Lazy |
| 21:43:03 | <dminuoso> | dexterfoo: the example seems contrived. |
| 21:43:09 | <ski> | (should there be two versions of `TypeApplications', one only allowing it with values which have been given a type with explicit `forall's ?) |
| 21:43:45 | <dminuoso> | ski: There's an accepted proposal to provide value level binders. |
| 21:44:21 | <dminuoso> | With a syntax like `f @a x = ...` |
| 21:44:23 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 21:44:23 | <ski> | i recall hearing about it, i think, but it not being finished then |
| 21:44:43 | <unfixpoint> | TIL `id @(forall a. a -> a) 101` won't work |
| 21:45:09 | × | coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 21:45:28 | <unfixpoint> | dminuoso: Can you not have `f (x :: a) = ...`, does it not bind `a`? |
| 21:45:32 | <dminuoso> | dexterfoo: but yeah, for inserting into a map, a foldl' is likely the better candidate |
| 21:45:37 | <ski> | yea, makes sense (apart from it appearing confusingly similar to as-patterns). so `foo :: forall a. ..a..; foo @a = ..a..' would make sense, but those would be two different `a' type variables |
| 21:45:40 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 21:46:46 | <ski> | % id @(forall a. a -> a) id 101 |
| 21:46:46 | <yahb> | ski: 101 |
| 21:47:00 | <dexterfoo> | thank you unfixpoint dminuoso c_wraith |
| 21:47:09 | <ski> | % id @(forall a. a -> a) False |
| 21:47:10 | <yahb> | ski: ; <interactive>:211:24: error:; * Couldn't match expected type `a1 -> a1' with actual type `Bool'; * In the second argument of `id', namely `False'; In the expression: id @(forall a. a -> a) False; In an equation for `it': it = id @(forall a. a -> a) False |
| 21:47:22 | <unfixpoint> | TypeApplication is meant to apply though, what is the proposal? |
| 21:47:37 | <dminuoso> | https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0155-type-lambda.rst |
| 21:47:50 | <unfixpoint> | Binding with `::` is good enough :S |
| 21:48:31 | <ski> | unfixpoint : doesn't specify ordering too clearly |
| 21:50:05 | ski | . o O ( `(map _) [] = []; map_f@(map f) ((f -> y):(map_f -> ys)) = y:ys' ) |
| 21:50:08 | <Guest42> | we define an internal parralel reduction rule inductively by with the following rules: https://imgur.com/a/heRxIIw Intuitively it the parralel reduction we forbid to reduce the redex in head. Show that if s => s' and s' in normal head form then s is in normal head form. |
| 21:50:29 | × | gumbish quits (4913050a@c-73-19-5-10.hsd1.wa.comcast.net) (Ping timeout: 245 seconds) |
| 21:50:47 | × | stree quits (~stree@50-108-97-52.adr01.mskg.mi.frontiernet.net) (Quit: Caught exception) |
| 21:51:02 | <Guest42> | Intuitively it is the parrallel reduction where we forbid* |
| 21:51:02 | <dminuoso> | unfixpoint: GHC uses a variant of System F as its intermediate language, which essentially provides binders for type variables. So rather than `\x.x` you'd write `/\t.\x^t.x`. TypeApplications exist both to elaborate programs during type checking, as well as providing a more convenient and explicit way to do this on the Haskell level. |
| 21:51:08 | → | stree joins (~stree@50-108-97-52.adr01.mskg.mi.frontiernet.net) |
| 21:51:25 | <hekkaidekapus> | ski: Bring back PatternSignatures? |
| 21:51:28 | → | brodie_ joins (~brodie@207.53.253.137) |
| 21:51:28 | <dminuoso> | unfixpoint: The above proposal just brings this to a conclusion and makes the TypeApplications consistent with that. |
| 21:52:17 | → | mbomba joins (~mbomba@bras-base-toroon2719w-grc-49-142-114-9-241.dsl.bell.ca) |
| 21:52:20 | <ski> | hekkaidekapus : yea, i'd like being able to say `map (f :: a -> b) (xs :: [a]) :: [b] = ...' (including result ascription) |
| 21:52:48 | <dminuoso> | Also, the pattern type signatures of ScopedTypeVariables is relatively noisy because it adds an unnecessary dimension |
| 21:52:55 | <hekkaidekapus> | ski: I agree. That sentence is the title of a proposal, IIRC. |
| 21:52:57 | → | falafel joins (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) |
| 21:53:03 | <ski> | (or `map @a @b (f :: a -> b) (xs :: [a]) :: [b] = ...', if combined with the above proposal) |
| 21:53:16 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 21:53:19 | × | Ariakenom quits (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) (Quit: Leaving) |
| 21:53:33 | <hekkaidekapus> | (But I was rejected I don’t recall for what reasons.) |
| 21:53:38 | × | brodie_ quits (~brodie@207.53.253.137) (Client Quit) |
| 21:54:07 | <dminuoso> | unfixpoint: In the lambda cube, we say that polymorphism gives us terms binding types. So why not provide proper binders for what we semantically already have. :) |
| 21:54:21 | <dolio> | At the very least, there needs to be another way of accomplishing that, because that syntax is awful. |
| 21:54:25 | <unfixpoint> | Wait how did you get `id @(forall a . a -> a ) id 101` to work? |
| 21:54:45 | <unfixpoint> | Do I need newer GHC than 8.4.4? |
| 21:54:57 | × | Franciman quits (~francesco@host-82-56-223-169.retail.telecomitalia.it) (Quit: Leaving) |
| 21:55:08 | <hekkaidekapus> | ski: Result ascription has another proposal, dunno its state. |
| 21:55:25 | <unfixpoint> | why is my GHC so old.. |
| 21:55:29 | <ski> | Guest42 : hm, so no beta at top-level (nor in operator position, if top-level is an application, continuing heriditarily) |
| 21:55:33 | <dminuoso> | hekkaidekapus: Is result ascriptions akin to how we ascript tyfams? |
| 21:55:57 | <ski> | unfixpoint : you forgot to pass `id' as argument |
| 21:55:59 | <dminuoso> | (also, can we get separate type family kind signatures?) |
| 21:56:01 | <hekkaidekapus> | dminuoso: See ski’s example. |
| 21:56:14 | <dminuoso> | hekkaidekapus: Ah indeed it looks like it. |
| 21:56:46 | <ski> | (the MLs have result ascriptions) |
| 21:57:25 | <hekkaidekapus> | dminuoso: Isn’t TF kind signatures realised by StandaloneKindSigs? |
| 21:57:33 | <unfixpoint> | Yeah, but even so. It gives "GHC doesn't yet support impredicative polymorphism" for me |
| 21:57:37 | <dminuoso> | unfixpoint: You just need to flip on ImpredicativeTypes |
| 21:57:49 | <boxscape> | just pretend it supports them |
| 21:57:51 | <dminuoso> | A notoriously buggy extension |
| 21:58:04 | <dminuoso> | It crashes GHC, or your program, or who knows. |
| 21:58:10 | <p0a> | Guest42: This channel is about Haskell... |
| 21:58:11 | <boxscape> | though HEAD now has a new implementation, so that's nice |
| 21:58:14 | <unfixpoint> | I'd rather not enable something that is "extremely flaky support" |
| 21:58:20 | <ski> | iirc, there was a new idea for how to implement it, recently |
| 21:58:40 | <dolio> | I don't think ImpredicativeTypes crashes anything. |
| 21:58:45 | <dolio> | It just doesn't work very well. |
| 21:58:48 | <unfixpoint> | Aaanyway, I should focus on other things for now. Thanks for all the help and interesting discussions |
| 21:59:03 | <boxscape> | ski https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3220 |
| 21:59:09 | <unfixpoint> | Thanks for the papers too, I'll check them later |
| 21:59:23 | <chkno> | Is there a better way to do a lint-style check for partial function usage than egrep -wr '!!|fromJust|head|init|last|maximum|minimum|read|tail' ? |
| 22:00:01 | <dminuoso> | chkno: You could also use a different prelude I guess. |
| 22:00:06 | → | rprije joins (~rprije@124.148.131.132) |
| 22:00:22 | <unfixpoint> | Solve Halting problem first |
| 22:00:28 | × | seanparsons quits (~sean@cpc145088-gill21-2-0-cust281.20-1.cable.virginm.net) (Quit: ZNC 1.8.1 - https://znc.in) |
| 22:00:30 | × | Varis quits (~Tadas@unaffiliated/varis) (Read error: Connection reset by peer) |
| 22:00:50 | <dminuoso> | chkno: You also forgot `throw` btw :) |
| 22:00:56 | <ski> | Guest42 : how do you define "normal head form" ? |
| 22:01:18 | <unfixpoint> | And `read` ;) |
| 22:01:26 | → | seanparsons joins (~sean@cpc145088-gill21-2-0-cust281.20-1.cable.virginm.net) |
| 22:01:35 | <unfixpoint> | It's there haha |
| 22:01:39 | <unfixpoint> | I go |
| 22:01:44 | <Guest42> | head normal form is a λ-term that has a top-level abstraction where the body does not have λ-subterms that can have β-reductions applied to them. |
| 22:02:36 | <justsomeguy> | Is that like weak head normal form? |
| 22:03:27 | <dolio> | It is like it, but not the same. |
| 22:03:40 | <ski> | that definition is a bit unclear, to me |
| 22:03:41 | <boxscape> | is there a way to have ghc warn you about missing equations in type families? |
| 22:03:57 | <boxscape> | (closed type families) |
| 22:03:58 | × | ulidtko quits (~ulidtko@193.111.48.79) (Read error: Connection reset by peer) |
| 22:04:04 | <ski> | does it mean that ⌜x⌝ is not in head normal form (since it's not a λ-abstraction) ? |
| 22:04:06 | → | Varis joins (~Tadas@unaffiliated/varis) |
| 22:04:25 | → | ulidtko joins (~ulidtko@193.111.48.79) |
| 22:04:33 | <Guest42> | i think so |
| 22:04:37 | → | abhixec joins (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) |
| 22:04:39 | <dminuoso> | dolio: Dunno, issues like this are not reassuring https://gitlab.haskell.org/ghc/ghc/-/issues/17332 |
| 22:04:55 | <ski> | (is there a more formal definition available ?) |
| 22:05:22 | <boxscape> | dminuoso that was before quick look though |
| 22:05:28 | <dminuoso> | boxscape: Sure. |
| 22:05:44 | × | Boomerang quits (~Boomerang@xd520f68c.cust.hiper.dk) (Ping timeout: 256 seconds) |
| 22:06:20 | <dolio> | dminuoso: Ah, that's pretty weird. I'm not exactly sure what some of those types even mean. |
| 22:06:31 | <ski> | is ⌜λ x ↦ x (λ y ↦ (λ z ↦ z) y)⌝ not in head normal form (since the body does contain a β-redex) ? |
| 22:07:32 | <Guest42> | A head normal form is a term that does not contain a beta redex in head position, i.e. that cannot be further reduced bya head reduction a head reduction |
| 22:08:22 | <Guest42> | yeah I think |
| 22:08:41 | <Guest42> | at least thats what I understand from the definition |
| 22:09:01 | <dminuoso> | dolio: They are just things out of `constraints` |
| 22:09:19 | <dolio> | No, those aren't the parts I'm confused about. :) |
| 22:10:29 | <dolio> | I guess the `forall a. a` has `a :: Constraint`, but I'm not sure why GHC thinks it has one of those. |
| 22:11:10 | <dminuoso> | data Dict c = c => Dict |
| 22:11:12 | <dolio> | It seems like the Bottom declaration doesn't actually need it to be a superclass, either, because it's never given an instance. |
| 22:11:51 | <dminuoso> | Well that's the point of it. |
| 22:12:13 | <ski> | Guest42 : does that mean it's the union of all abstractions ⌜λ x ↦ M⌝, with the smallest subset of λ-terms that contain all variables ⌜x⌝; and all applications ⌜M N⌝, provided ⌜M⌝ is already in this subset ? |
| 22:12:26 | <dminuoso> | Think the more recent version uses Any instead of forall a. a as a superclass |
| 22:12:31 | × | unfixpoint quits (1f0a965a@31-10-150-90.cgn.dynamic.upc.ch) (Remote host closed the connection) |
| 22:12:51 | <dminuoso> | Without that superclass, you could write instances for it |
| 22:12:57 | <boxscape> | hmm so the case expression with (forall a . a) means that now every possible constraint is fulfilled in that scope? |
| 22:13:36 | <boxscape> | I guess there's no case expression |
| 22:13:38 | <boxscape> | pattern guard |
| 22:14:11 | <dminuoso> | Or.. mmm. |
| 22:14:19 | <boxscape> | ..so therefore, the Bottom constraints is part of the set of all constraints and therefore you can call "no"? |
| 22:14:32 | <dolio> | Yeah. |
| 22:14:38 | <boxscape> | ok |
| 22:15:56 | × | u0_a298 quits (~user@47.206.148.226) (Ping timeout: 256 seconds) |
| 22:17:40 | <ski> | (hm, shouldn't it require `aux :: (forall a. a) => Dict (forall a. a)', if anything ?) |
| 22:18:29 | <dolio> | Presumably. For some reason it thinks it just has such an instance in that case, though. |
| 22:18:43 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Ping timeout: 240 seconds) |
| 22:19:00 | <dolio> | But I guess not when trying to define instances for Bottom. |
| 22:19:54 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 22:20:14 | <dolio> | Or, who knows what's going on. I guess ImpredicativeTypes was enabling some code path that makes no sense. |
| 22:21:40 | × | darjeeling_ quits (~darjeelin@122.245.211.11) (Ping timeout: 265 seconds) |
| 22:21:51 | <ski> | mm |
| 22:23:11 | <dolio> | I guess it wouldn't be too surprising if it's just a bunch of checks sprinkled throughout the code that no one has bothered thinking about in conjunction with other developments (like quantified constraints). |
| 22:24:16 | → | iqubic joins (~user@2601:602:9500:4870:18b7:5f73:2db2:1881) |
| 22:26:28 | → | anon1252 joins (5ec1fe17@5ec1fe17.skybroadband.com) |
| 22:26:35 | → | hexfive joins (~hexfive@50-47-142-195.evrt.wa.frontiernet.net) |
| 22:27:02 | × | yogani quits (sid42623@gateway/web/irccloud.com/x-rolajygghowodpbd) (Ping timeout: 260 seconds) |
| 22:27:02 | × | PoliticsII______ quits (sid193551@gateway/web/irccloud.com/x-ykrgnddgnwhyshpo) (Ping timeout: 260 seconds) |
| 22:27:02 | × | benl23 quits (sid284234@gateway/web/irccloud.com/x-zcormuhggyweibpr) (Ping timeout: 260 seconds) |
| 22:27:02 | × | benwr____ quits (sid372383@gateway/web/irccloud.com/x-wqbchwbubajgshwl) (Ping timeout: 260 seconds) |
| 22:27:02 | × | edwinb quits (sid69486@gateway/web/irccloud.com/x-ucpbbzlyfldprgqw) (Ping timeout: 260 seconds) |
| 22:27:06 | × | ulidtko quits (~ulidtko@193.111.48.79) (Remote host closed the connection) |
| 22:27:09 | → | yogani joins (sid42623@gateway/web/irccloud.com/x-xwocvhxoqauihzue) |
| 22:27:24 | → | ulidtko joins (~ulidtko@193.111.48.79) |
| 22:27:37 | × | aristid quits (sid1599@gateway/web/irccloud.com/x-ieumvqzkylmookgw) (Ping timeout: 260 seconds) |
| 22:27:37 | × | psydruid quits (psydruidma@gateway/shell/matrix.org/x-onpwsguylfwyjnoj) (Ping timeout: 260 seconds) |
| 22:27:37 | × | aizen_s quits (sid462968@gateway/web/irccloud.com/x-rpdggkhwylxxzxar) (Ping timeout: 260 seconds) |
| 22:27:48 | → | benl23 joins (sid284234@gateway/web/irccloud.com/x-hgqgnkygwwcwddwc) |
| 22:28:05 | <hekkaidekapus> | dolio: Is the awful syntax you were talking about earlier this one: `foo :: F = bar`? |
| 22:28:12 | × | Amras quits (~Amras@unaffiliated/amras0000) (Ping timeout: 260 seconds) |
| 22:28:12 | × | rednaZ[m] quits (r3dnazmatr@gateway/shell/matrix.org/x-gpnsxbbsvkfpdeul) (Ping timeout: 260 seconds) |
| 22:28:12 | × | jesser[m] quits (jessermatr@gateway/shell/matrix.org/x-goezqreqcnfmgjgv) (Ping timeout: 260 seconds) |
| 22:28:12 | × | tersetears[m] quits (tersetears@gateway/shell/matrix.org/x-wmhwjlekxzvfgxue) (Ping timeout: 260 seconds) |
| 22:28:12 | × | kaychaks_riot quits (kaychaksma@gateway/shell/matrix.org/x-csnlnomioxxbbnnm) (Ping timeout: 260 seconds) |
| 22:28:12 | × | srid quits (sridmatrix@gateway/shell/matrix.org/x-vidxbchrzjfqulmd) (Ping timeout: 260 seconds) |
| 22:28:34 | → | edwinb joins (sid69486@gateway/web/irccloud.com/x-ttfxxggsnhwcnlbe) |
| 22:28:40 | → | tinwood_ joins (~tinwood@general.default.akavanagh.uk0.bigv.io) |
| 22:28:43 | → | aristid joins (sid1599@gateway/web/irccloud.com/x-hkziwpbxvyapwndr) |
| 22:28:47 | × | tinwood quits (~tinwood@general.default.akavanagh.uk0.bigv.io) (Ping timeout: 260 seconds) |
| 22:28:47 | → | benwr____ joins (sid372383@gateway/web/irccloud.com/x-zroyfovbhqhiqzax) |
| 22:28:47 | × | chaosmasttter quits (~chaosmast@p200300c4a70b2a01c0445547f28d17ad.dip0.t-ipconnect.de) (Quit: WeeChat 2.9) |
| 22:28:51 | <iqubic> | So, I'm trying to compile a haskell project using Cabal and GHC 8.8.4 I have this cabal file: https://dpaste.com/H5CTS2V6R |
| 22:28:52 | <dolio> | hekkaidekapus: The one where you put all the types on the same line as the arguments. It eats way too much horizontal space. |
| 22:29:00 | hackage | rosebud 0.1.0.0 - Common rose tree/forest functions https://hackage.haskell.org/package/rosebud-0.1.0.0 (jship) |
| 22:29:03 | → | PoliticsII______ joins (sid193551@gateway/web/irccloud.com/x-ifhtanwghthhvmbn) |
| 22:29:03 | → | aizen_s joins (sid462968@gateway/web/irccloud.com/x-ighywpehicgiourx) |
| 22:29:07 | <iqubic> | Here's the error I'm getting: https://dpaste.com/4JTTNNPTC |
| 22:29:30 | <iqubic> | Anyone know what the issue is here? |
| 22:29:42 | → | tersetears[m] joins (tersetears@gateway/shell/matrix.org/x-sudqunulnrivtufh) |
| 22:29:56 | <hekkaidekapus> | dolio: So, it turns out the proposal is accepted but not yet implemented, including ascribing arguments. |
| 22:29:57 | → | Amras joins (~Amras@unaffiliated/amras0000) |
| 22:30:03 | → | jesser[m] joins (jessermatr@gateway/shell/matrix.org/x-fnrjbdbcxycnmdhs) |
| 22:30:08 | → | rednaZ[m] joins (r3dnazmatr@gateway/shell/matrix.org/x-uudppykggjqnwgdt) |
| 22:30:21 | <dolio> | I don't care if it's an option. I just want another option, because I'll never use that one. :) |
| 22:30:34 | <hekkaidekapus> | ski: One pet peeve down: <https://github.com/ghc-proposals/ghc-proposals/pull/228> |
| 22:30:40 | → | srid joins (sridmatrix@gateway/shell/matrix.org/x-wcquiejsxgjdmcxb) |
| 22:30:40 | × | mananamenos quits (~mananamen@84.122.202.215.dyn.user.ono.com) (Ping timeout: 256 seconds) |
| 22:30:43 | <anon1252> | iqubic: Slightly offtopic but what font is that? |
| 22:31:23 | × | jedws quits (~jedws@101.184.175.183) (Ping timeout: 260 seconds) |
| 22:31:56 | → | kaychaks_riot joins (kaychaksma@gateway/shell/matrix.org/x-mkllmseyzgoebiyk) |
| 22:32:04 | <hekkaidekapus> | dolio: If I’m getting what you want, annotating the result if okay, but ugly for arguments. |
| 22:32:06 | <iqubic> | What font is what? |
| 22:32:30 | → | psydruid joins (psydruidma@gateway/shell/matrix.org/x-tkomzubgcyrydslv) |
| 22:32:35 | <anon1252> | iqubic: Sorry, nevermind, I thought it was a screenshot but it's not so I've got it. |
| 22:32:50 | <iqubic> | anon1252: I posted a total of 0 images, so whatever font it is must be coming from your computer. |
| 22:32:50 | <dolio> | I just don't want any other feature to require you to use this sort of annotation. |
| 22:32:58 | <hekkaidekapus> | heh |
| 22:32:59 | <iqubic> | I have no idea what font your computer is using. |
| 22:33:07 | <dolio> | I want to be able to write signatures on their own line. |
| 22:33:44 | <iqubic> | So, anyone know why my thing won't compile? |
| 22:34:32 | <hekkaidekapus> | Euh, haven’t re-read the full proposal but I don’t think there is another feature requiring to use the new syntax. It’s just an option. |
| 22:34:48 | → | jedws joins (~jedws@101.184.175.183) |
| 22:35:19 | <dolio> | Yeah, that's fine. |
| 22:35:20 | <koz_> | iqubic: 4.12 is 8.6. |
| 22:35:22 | <koz_> | Not 8.8. |
| 22:38:45 | × | nuncanada quits (~dude@179.235.160.168) (Ping timeout: 240 seconds) |
| 22:40:02 | × | avn quits (~avn@78-56-108-78.static.zebra.lt) (Ping timeout: 265 seconds) |
| 22:40:34 | <hekkaidekapus> | @where boot-libs-versions -- iqubic |
| 22:40:34 | <lambdabot> | <https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/libraries/version-history> |
| 22:40:43 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 22:41:01 | <iqubic> | koz_: How shall I change my cabal file? |
| 22:41:04 | × | falafel quits (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) (Remote host closed the connection) |
| 22:41:09 | <koz_> | iqubic: Change your base pin. |
| 22:41:22 | <koz_> | To match the version that comes with GHC 8.8.4. |
| 22:42:03 | <iqubic> | I don't know how to do that. Can you teach me? |
| 22:42:45 | <koz_> | iqubic: Your version of base is set by '^>= 4.12.0.0' in your cabal file. It should be ^>= 4.13.0.0. |
| 22:42:54 | <iqubic> | Thanks. |
| 22:43:31 | <boxscape> | ^>= 4.12.0.0 matches anything below 4.13? or anything below 5? |
| 22:43:35 | <ski> | hekkaidekapus : one down ? |
| 22:43:39 | <koz_> | boxscape: Neither of these. |
| 22:43:42 | <boxscape> | oh |
| 22:44:09 | <koz_> | The exact meaning of ^>=-style bounds is explained in the Cabal docs. |
| 22:44:19 | → | nut joins (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 22:44:22 | <boxscape> | (I meant at least 4.12.0.0 and below x, but I'll check the docs) |
| 22:44:32 | <hekkaidekapus> | ski: Isn’t the ML-style annotations question resolved by that proposal? |
| 22:45:42 | × | foursaph quits (~foursaph@dynamic-077-006-006-064.77.6.pool.telefonica.de) (Quit: leaving) |
| 22:45:46 | <hekkaidekapus> | And even the PatternSignatures one? |
| 22:46:07 | <boxscape> | "^>= x.y.z.u == >= x.y.z.u && < x.(y+1)" |
| 22:46:18 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 22:46:35 | → | olligobber joins (olligobber@gateway/vpn/privateinternetaccess/olligobber) |
| 22:46:45 | <boxscape> | so... ^>= 4.12.0.0 == >= 4.12.0.0 && < 4.13 |
| 22:47:09 | <hekkaidekapus> | boxscape: Yeah, basically the version after ^>= means it will not break PVP. |
| 22:47:16 | <boxscape> | ok |
| 22:48:11 | <hekkaidekapus> | iqubic: For future fixes, you could bookmark the URL I pasted above. |
| 22:48:17 | <koz_> | I keep misreading PVP as 'player-versus-player', rofl. |
| 22:48:35 | <koz_> | Haskell has the Battle Royale approach to package versioning, clearly. |
| 22:49:00 | <ski> | hekkaidekapus : oh. yes, i think so. i was just thinking you meant you commented or added something to that discussion, but couldn't find a recent addition |
| 22:49:26 | <hekkaidekapus> | Nope, I don’t do GitHub comments ;) |
| 22:49:56 | <hekkaidekapus> | The remaining task is to scale down STV. |
| 22:50:26 | × | nek0 quits (~nek0@mail.nek0.eu) (Remote host closed the connection) |
| 22:50:28 | <ski> | (preferably flipping when it binds tyvars over the body, and when it doesn't) |
| 22:51:27 | × | forell quits (~forell@unaffiliated/forell) (Quit: ZNC - https://znc.in) |
| 22:51:28 | <hekkaidekapus> | Aye. But that would be nearly impossible given its wide adoption. |
| 22:51:31 | <ski> | (i think i remember, when i first read about it, i was thinking they must've made a mistake in the docs, meaning the opposite of what was written .. until i tested it) |
| 22:51:49 | → | forell joins (~forell@unaffiliated/forell) |
| 22:52:01 | → | nek0 joins (~nek0@mail.nek0.eu) |
| 22:52:07 | <ski> | yes. so an alternative extension with the opposite behavious would be what one might reasonably hope for, i think |
| 22:52:50 | ← | nut parts (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) ("ERC (IRC client for Emacs 26.3)") |
| 22:53:05 | <hekkaidekapus> | Absolutely. And then set in motion a decade-long process to deprecate STV :D |
| 22:53:29 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 22:53:30 | → | cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net) |
| 22:53:31 | <ski> | well, how long have we had STV, now ? |
| 22:53:34 | ski | can't recall |
| 22:53:43 | <hekkaidekapus> | Me, neither. |
| 22:53:52 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 22:54:00 | <ski> | anyway, better late, than never |
| 22:54:07 | × | __monty__ quits (~toonn@unaffiliated/toonn) (Quit: leaving) |
| 22:54:59 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 22:54:59 | <hekkaidekapus> | In the Users’ Guide, STV is there since 6.8.1. |
| 22:55:07 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 22:56:35 | → | avn joins (~avn@78-56-108-78.static.zebra.lt) |
| 22:58:00 | hekkaidekapus | sees where ski got the confusion: “But I was rejected I don’t recall for what reasons.” s/I was/ It was/ |
| 22:58:14 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Client Quit) |
| 22:58:17 | ← | anon1252 parts (5ec1fe17@5ec1fe17.skybroadband.com) () |
| 22:59:14 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 22:59:20 | <ski> | (no. i noted that at the time, and internally typo-corrected it as you indicate) |
| 23:00:02 | <hekkaidekapus> | Ah, ok. |
| 23:00:23 | <ski> | (for some reason, i've noticed that i, unnervingly often, write "i" when i mean "it") |
| 23:01:15 | <hekkaidekapus> | heh Those pesky keyboards :d |
| 23:02:12 | <ski> | (.. and some other annoying typos, like the "the the" class of typos (you pause after writing a word, to think, and then when you continue, you repeat the last word). also, sometimes, when thinking ahead about how to formulate myself, i write out a later planned word, in place of the current one that i intended) |
| 23:02:30 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 23:04:00 | <ski> | (and no, i don't think i'm simply failing to press the "t" key in the "it". it may be related to another class of typos, where i write another word, that, when pronounced, sounds more or less similar to the intended word) |
| 23:05:33 | <ski> | (.. some kind of mess-up, in the internal sentence-structure to keypress serialization) |
| 23:05:34 | <hekkaidekapus> | Maybe it’s the cerebral chemistry being quicker than the bio-mechanical anatomy. By the time a typo is spotted, some other body part has already initiated an irreversible action. |
| 23:05:39 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 23:06:39 | <hpc> | i wonder if they make joke keyboards that don't have a backspace or delete key |
| 23:07:11 | <ski> | it's interesting to read a transcript of what someone has spoken, including "er"s, half-formed sentences, changing midway through, &c. |
| 23:08:22 | <ski> | hm. perhaps they could brand those keyboards "Dijkstra" |
| 23:09:14 | <justsomeguy> | ski: I do a lot of that, too. My worst sin is writing in inconsistent tense (past, present, future), because I've rephrased my comment in the chat box five or six times before sending. |
| 23:09:22 | <ski> | (another example of an annoying typo is writing "now" in place of "not" (or vice versa)) |
| 23:09:34 | × | random quits (~random@46.254.129.126) (Ping timeout: 246 seconds) |
| 23:10:10 | <ski> | yea, rephrasing (incompletely/inconsistently) is dangerous |
| 23:10:38 | × | abhixec quits (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 23:11:02 | justsomeguy | also sometimes habitually replaces English words with similar sounding command names since he's more used to typing them, which is hilarious. |
| 23:11:21 | <ski> | hm, yea. i've noticed that too |
| 23:11:33 | <ski> | e.g. writing "type" in place of "typo" |
| 23:11:58 | <ski> | partly a muscle-memory thing, i'd guess |
| 23:11:58 | × | Tourist quits (~tourist@unaffiliated/tourist) (Ping timeout: 256 seconds) |
| 23:12:00 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 23:12:04 | × | Flonk quits (~Flonk@ec2-52-40-29-25.us-west-2.compute.amazonaws.com) (Ping timeout: 240 seconds) |
| 23:12:06 | × | digia quits (~digia@unaffiliated/digia) (Remote host closed the connection) |
| 23:12:08 | × | bsima quits (~bsima@simatime.com) (Quit: ZNC 1.7.5 - https://znc.in) |
| 23:12:09 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 23:12:19 | → | digia joins (~digia@unaffiliated/digia) |
| 23:12:31 | → | bsima joins (~bsima@simatime.com) |
| 23:12:36 | <boxscape> | any idea why `Fam alt MkR = alt` here doesn't produce an error? (using ghc 8.10) https://gist.github.com/JakobBruenker/a1b8c66abcb1c05e9bf4ff55e73fa6c8 |
| 23:12:43 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds) |
| 23:12:44 | × | bobbytables quits (~bobbytabl@ec2-44-224-191-138.us-west-2.compute.amazonaws.com) (Ping timeout: 240 seconds) |
| 23:12:53 | → | orcus- joins (~orcus@unaffiliated/orcus) |
| 23:13:03 | × | jb55 quits (~jb55@gateway/tor-sasl/jb55) (Ping timeout: 240 seconds) |
| 23:13:07 | → | conal joins (~conal@64.71.133.70) |
| 23:13:08 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 23:13:09 | <ski> | (or, writing an english (usually short) word in place of a similar-looking swedish one) |
| 23:13:16 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 23:13:18 | → | mastarija joins (~mastarija@93-136-63-196.adsl.net.t-com.hr) |
| 23:13:23 | × | Inoperable quits (~PLAYER_1@fancydata.science) (Ping timeout: 260 seconds) |
| 23:13:25 | × | cheers quits (user@unaffiliated/cheers) (Ping timeout: 240 seconds) |
| 23:13:25 | × | Madars quits (~null@unaffiliated/madars) (Ping timeout: 240 seconds) |
| 23:13:48 | × | rotty quits (rotty@ghost.xx.vu) (Ping timeout: 272 seconds) |
| 23:13:59 | → | conal joins (~conal@64.71.133.70) |
| 23:14:20 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Max SendQ exceeded) |
| 23:14:24 | × | siraben quits (sirabenmat@gateway/shell/matrix.org/x-ayxhmamsaxhvcaxs) (Ping timeout: 240 seconds) |
| 23:14:39 | <ski> | boxscape : hm, i'd guess it's interpreted as `Fam @a @b @b alt MkR = alt' ? |
| 23:14:50 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 23:14:56 | → | bobbytables joins (~bobbytabl@ec2-44-224-191-138.us-west-2.compute.amazonaws.com) |
| 23:14:57 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 23:15:04 | × | maralorn quits (maralornma@gateway/shell/matrix.org/x-dbfnqoxrhdjljtko) (Ping timeout: 240 seconds) |
| 23:15:13 | <boxscape> | oh, hm, I suppose that makes sense |
| 23:15:25 | <ski> | so, in that case, that `MkR' has kind `Relation b b' |
| 23:15:27 | → | cheers joins (user@unaffiliated/cheers) |
| 23:15:44 | × | iinuwa quits (iinuwamatr@gateway/shell/matrix.org/x-jxshhrkktrqfnuqi) (Ping timeout: 240 seconds) |
| 23:15:44 | × | orcus quits (~orcus@unaffiliated/orcus) (Ping timeout: 240 seconds) |
| 23:15:54 | <boxscape> | I think I only considered that the pattern matching could influence what the invisible args are, and forgot that the result could as well |
| 23:15:57 | → | rotty joins (rotty@ghost.xx.vu) |
| 23:16:00 | <boxscape> | thanks |
| 23:17:04 | → | maralorn joins (maralornma@gateway/shell/matrix.org/x-qdyphvplrxcjzfoq) |
| 23:17:39 | → | abhixec joins (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) |
| 23:18:22 | → | In0perable joins (~PLAYER_1@fancydata.science) |
| 23:18:54 | <ski> | well, well, `alt :: Relation a c' is consistent with `alt :: Relation a b',`MkR :: Relation b c', if `b = c' |
| 23:19:09 | → | Flonk joins (~Flonk@ec2-52-40-29-25.us-west-2.compute.amazonaws.com) |
| 23:19:25 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 23:19:26 | <boxscape> | right, that makes sense |
| 23:20:02 | → | conal joins (~conal@64.71.133.70) |
| 23:20:12 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 23:20:16 | → | siraben joins (sirabenmat@gateway/shell/matrix.org/x-moaedtsqvaqtshxu) |
| 23:20:29 | <ski> | (that "well, well, " being an (inadvertent) example of the "the the" class of typos mentioned above) |
| 23:20:30 | hackage | th-lift-instances 0.1.18 - Lift instances for template-haskell for common data types. https://hackage.haskell.org/package/th-lift-instances-0.1.18 (BennoFuenfstueck) |
| 23:20:52 | × | aoei quits (~aoei@240.223.246.35.bc.googleusercontent.com) (Remote host closed the connection) |
| 23:22:03 | → | crdrost joins (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) |
| 23:22:04 | → | aoei joins (~aoei@240.223.246.35.bc.googleusercontent.com) |
| 23:22:15 | <boxscape> | What apparently also confused me is that I encountered this in a situation where MkR was slightly different and made b ~ c impossible, but not in a way that was obvious to the type checker |
| 23:23:33 | <boxscape> | (specifically, MkR took a proof that b < c) |
| 23:23:49 | × | danvet quits (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) (Ping timeout: 272 seconds) |
| 23:23:55 | × | abhixec quits (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 23:25:22 | × | rotty quits (rotty@ghost.xx.vu) (Ping timeout: 260 seconds) |
| 23:26:00 | → | jb55 joins (~jb55@gateway/tor-sasl/jb55) |
| 23:27:03 | → | rotty joins (rotty@ghost.xx.vu) |
| 23:27:42 | × | shutdown_-h_now quits (~arjan@2001:1c06:2d0b:2312:190f:5fcb:2d71:58b) (Ping timeout: 260 seconds) |
| 23:27:56 | <ski> | hmm, it's curious that a polymorphic type family isn't blind in the `forall' |
| 23:28:07 | → | Madars joins (~null@unaffiliated/madars) |
| 23:28:22 | <boxscape> | what do you mean by "blind" here? |
| 23:29:07 | × | ystael quits (~ystael@209.6.50.55) (Ping timeout: 260 seconds) |
| 23:29:19 | <ski> | not being able to match on the kind bound by the `forall' |
| 23:29:56 | <boxscape> | I think that's what Richard Eisenberg et al call "relevant" vs "irrelevant"? |
| 23:30:06 | <ski> | you can't write `notId :: forall a. a -> a; notId @Int n = n + 1; notId x = x' |
| 23:30:13 | <boxscape> | he's complained before that the "forall" on the kind level really should be called "foreach" to match up with the value level plans |
| 23:30:41 | <ski> | in relation to type (and `data') families, specifically ? |
| 23:31:25 | <boxscape> | Well, I'm fairly certain that relevancy is a concept applicable to type families, I'm less certain if I saw Richard complain about it in that context |
| 23:32:17 | <ski> | (since i'd think parametricity would also sensibly apply to polymorphic types) |
| 23:32:23 | → | conal joins (~conal@64.71.133.70) |
| 23:32:30 | <ski> | mhm |
| 23:32:51 | <boxscape> | Yeah, hm, I suppose relevancy can break parametricity |
| 23:32:57 | <ski> | iow, i guess i'd expect your `Fam' to use `foreach' instead, but to also be able to use `forall' on the type-level |
| 23:32:59 | → | iinuwa joins (iinuwamatr@gateway/shell/matrix.org/x-cburarlywoxtjfrp) |
| 23:33:12 | <boxscape> | yeah that makes sense |
| 23:34:06 | <ski> | that could have helped catch your confusion in the pasted code, preventing `Fam alt MkR = alt' to work, unless you used `foreach' |
| 23:34:17 | → | shutdown_-h_now joins (~arjan@2001:1c06:2d0b:2312:794d:ef9:43c6:21d5) |
| 23:34:23 | <boxscape> | that's true |
| 23:34:53 | <ski> | (btw, i think the "blind" terminology might come from Japaridze's computability logic) |
| 23:34:58 | <boxscape> | although even then I think in a value level function with foreach the result (as supposed to matching on other arguments) couldn't influence the invisible arguments like that? I'm not sure |
| 23:35:25 | <boxscape> | s/supposed/opposed |
| 23:37:00 | <ski> | i'm still not totally sure what you mean by "the result [..] couldn't influence the invisible arguments like that" -- i suspect you mean the "back-propagation" of unification of tyvars, to specialize the (implicit type-)parameters, based on the type inference/checking on the body |
| 23:37:33 | <boxscape> | that.. sounds it like should be what I mean |
| 23:38:18 | <dolio> | The whole system is kind of inconsistent. |
| 23:38:29 | × | nek0 quits (~nek0@mail.nek0.eu) (Quit: Ping timeout (120 seconds)) |
| 23:38:33 | <dolio> | Like, type families already let you match on things that you aren't normally allowed to match on. |
| 23:38:36 | <glguy> | unclechu: You around? |
| 23:38:42 | <ski> | hmm .. consider something like `sameNat :: foreach (m :: Nat) (n :: Nat). Maybe (Equal m n); sameNat = Just Refl; sameNat = Nothing' |
| 23:38:43 | × | ulidtko quits (~ulidtko@193.111.48.79) (Remote host closed the connection) |
| 23:38:50 | <glguy> | I was playing with a module based on your wanting a reusable, type-level Map https://gist.github.com/glguy/98331ca1c3876a188e5380b9d0da5751 |
| 23:39:02 | → | nek0 joins (~nek0@mail.nek0.eu) |
| 23:39:02 | → | ulidtko joins (~ulidtko@193.111.48.79) |
| 23:39:06 | <glguy> | It's not "light-weight", but I thought it was cool that it worked |
| 23:39:31 | <ski> | where the definition would be expanded into `sameNat @n @n = Just (Refl @Nat @n); sameNat @_ @_ = Nothing' |
| 23:39:34 | → | jonatanb joins (~jonatanb@83.24.155.27.ipv4.supernova.orange.pl) |
| 23:40:11 | <ski> | dolio : yea. we sortof pretend `*'/`Type' is a(n open) sum type, in families |
| 23:40:20 | <dolio> | So it's kind of hard to draw analogies between the two levels, because they don't work the same in many ways. |
| 23:41:14 | <boxscape> | right, but the eventual goal of folks like Richard is to unify them, so.. I guess I was analogizing with that hypothetical future value level |
| 23:41:15 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 23:41:29 | <boxscape> | though of course that's not fully specified at this point |
| 23:41:39 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Ping timeout: 256 seconds) |
| 23:41:52 | <dolio> | And even in more uniform systems, parametricity gets kind of fuzzy and unsatisfying when you talk about applying it to types. |
| 23:42:05 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 23:42:08 | <boxscape> | ski intuitively I would expect sameNat not to compile in a Haskell with foreach, but maybe it should, I'm not sure. Hm, would it compile in agda? |
| 23:42:28 | <ski> | (and this is one argument against the terminology "type constructor" (vs. "data constructor"), i suppose .. also, with `DataKinds', with say `data Tag = E | D', `Tag' being a kind, what do we call `Tag',`E',`D' ? calling the latter two "type constructors" would seem to be confusing, possibly ? .. oh, well) |
| 23:43:06 | <ski> | boxscape : in Agda, with implicit parameters, yes |
| 23:43:14 | <boxscape> | okay, fair enough |
| 23:43:32 | <ski> | or, well |
| 23:43:50 | <ski> | you'd have to actually do recursion on the `Nat's, not being able to use non-linear patterns |
| 23:44:09 | <ski> | (so not with that exact implementation. but you could implement it) |
| 23:44:13 | <boxscape> | ok |
| 23:44:30 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 23:46:37 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed) |
| 23:46:50 | × | jonatanb quits (~jonatanb@83.24.155.27.ipv4.supernova.orange.pl) (Remote host closed the connection) |
| 23:47:03 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 23:47:19 | × | hexfive quits (~hexfive@50-47-142-195.evrt.wa.frontiernet.net) (Quit: i must go. my people need me.) |
| 23:48:01 | <energizer> | usually arrays are indexed by natural numbers. is there something like an array but indexed by some other type |
| 23:48:30 | <energizer> | like strings or whatever |
| 23:48:33 | <ski> | > listArray (LT,GT) [-1,0,1] |
| 23:48:35 | <lambdabot> | array (LT,GT) [(LT,-1),(EQ,0),(GT,1)] |
| 23:48:38 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 23:49:01 | <ski> | perhaps you want some form of trie ? |
| 23:49:24 | <ski> | @type listArray (LT,GT) [-1,0,1 :: Integer] |
| 23:49:26 | <lambdabot> | Array Ordering Integer |
| 23:49:31 | <ClaudiusMaximus> | Ix is a class for mapping values of a type to natural numbers for use as array indices |
| 23:49:44 | <ski> | (an array indexed by values of type `Ordering') |
| 23:49:59 | <ski> | @type listArray |
| 23:50:01 | <lambdabot> | Ix i => (i, i) -> [e] -> Array i e |
| 23:50:23 | → | jonatanb joins (jonatanb@gateway/vpn/protonvpn/jonatanb) |
| 23:50:54 | <energizer> | there should be the property that a<b<c means b is a valid index whenever a and c are |
| 23:51:15 | <ski> | @type range |
| 23:51:16 | <lambdabot> | Ix a => (a, a) -> [a] |
| 23:51:27 | <ski> | gives values in a kind of "interval" |
| 23:51:46 | <ski> | (for two-dimensional arrays, it gives indices in a "rectangle") |
| 23:52:00 | <ClaudiusMaximus> | @type inRange -- tests, and i can never remember the argument order |
| 23:52:01 | <lambdabot> | Ix a => (a, a) -> a -> Bool |
| 23:52:05 | <ski> | > range ((-1,-1),(2,3)) |
| 23:52:06 | × | chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer) |
| 23:52:07 | <lambdabot> | [(-1,-1),(-1,0),(-1,1),(-1,2),(-1,3),(0,-1),(0,0),(0,1),(0,2),(0,3),(1,-1),(... |
| 23:52:23 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 23:52:54 | <ClaudiusMaximus> | (it has a name that sounds infix, but it is flipped w.r.t. infix usage) |
| 23:54:24 | <ski> | in other words, `range (lo,hi)' should give a list of all indices `i', where ⌜lo ≼ i ∧ i ≼ hi⌝, where the ordering here is not lexicographic ordering in case of tuples, but rather the product order (a partial order, not a total/linear one) |
| 23:57:06 | <ski> | (ClaudiusMaximus : i wonder how that happened ..) |
| 23:58:34 | <boxscape> | %! ghc --version |
| 23:58:34 | <yahb> | boxscape: [Segmentation fault] |
| 23:58:35 | <boxscape> | cool |
All times are in UTC on 2020-11-18.