Logs: liberachat/#haskell
| 2021-08-25 19:16:18 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-25 19:16:22 | × | ec_ quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-25 19:19:27 | × | cheater quits (~Username@user/cheater) (Ping timeout: 240 seconds) |
| 2021-08-25 19:19:55 | → | remedan joins (~remedan@balak.me) |
| 2021-08-25 19:19:58 | → | cheater joins (~Username@user/cheater) |
| 2021-08-25 19:21:33 | × | dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.2) |
| 2021-08-25 19:23:22 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-08-25 19:23:31 | → | chris joins (~chris@81.96.113.213) |
| 2021-08-25 19:23:34 | chris | is now known as Guest6628 |
| 2021-08-25 19:27:42 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 250 seconds) |
| 2021-08-25 19:27:46 | × | azeem quits (~azeem@176.201.15.223) (Read error: Connection reset by peer) |
| 2021-08-25 19:27:51 | → | ec_ joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-25 19:28:38 | → | azeem joins (~azeem@dynamic-adsl-78-13-242-140.clienti.tiscali.it) |
| 2021-08-25 19:37:37 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:d4c9:355c:bd9d:df19) (Remote host closed the connection) |
| 2021-08-25 19:41:17 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 2021-08-25 19:41:31 | → | liskin joins (~liskin@xmonad/liskin) |
| 2021-08-25 19:42:35 | × | liskin quits (~liskin@xmonad/liskin) (Remote host closed the connection) |
| 2021-08-25 19:43:45 | → | liskin joins (~liskin@xmonad/liskin) |
| 2021-08-25 19:47:16 | × | liskin quits (~liskin@xmonad/liskin) (Read error: Connection reset by peer) |
| 2021-08-25 19:48:17 | → | jtomas_ joins (~jtomas@233.red-83-34-2.dynamicip.rima-tde.net) |
| 2021-08-25 19:48:30 | × | jtomas quits (~jtomas@233.red-83-34-2.dynamicip.rima-tde.net) (Ping timeout: 250 seconds) |
| 2021-08-25 19:49:39 | × | teo quits (~teo@137.220.120.222) () |
| 2021-08-25 19:50:28 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-08-25 19:52:01 | → | liskin joins (~liskin@xmonad/liskin) |
| 2021-08-25 19:56:50 | → | fendor_ joins (~fendor@91.141.62.191.wireless.dyn.drei.com) |
| 2021-08-25 19:59:40 | × | fendor quits (~fendor@91.141.62.191.wireless.dyn.drei.com) (Ping timeout: 240 seconds) |
| 2021-08-25 20:00:48 | × | ec_ quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-25 20:04:47 | × | juhp quits (~juhp@128.106.188.220) (Ping timeout: 240 seconds) |
| 2021-08-25 20:05:15 | → | neurocyte830 joins (~neurocyte@user/neurocyte) |
| 2021-08-25 20:05:50 | × | dispater quits (~dispater@user/brprice) (Quit: ZNC 1.8.1 - https://znc.in) |
| 2021-08-25 20:06:41 | → | elf_fortrez joins (~elf_fortr@adsl-72-50-4-45.prtc.net) |
| 2021-08-25 20:06:57 | × | mastarija quits (~mastarija@78-3-210-70.adsl.net.t-com.hr) (Ping timeout: 248 seconds) |
| 2021-08-25 20:07:10 | → | dispater joins (~dispater@user/brprice) |
| 2021-08-25 20:07:11 | × | dispater quits (~dispater@user/brprice) (Remote host closed the connection) |
| 2021-08-25 20:08:02 | → | juhp joins (~juhp@128.106.188.220) |
| 2021-08-25 20:08:31 | → | dispater joins (~dispater@user/brprice) |
| 2021-08-25 20:09:02 | → | orcus joins (~orcus@mail.brprice.uk) |
| 2021-08-25 20:09:54 | × | Guest6628 quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2021-08-25 20:10:31 | → | chris joins (~chris@81.96.113.213) |
| 2021-08-25 20:10:35 | chris | is now known as Guest9305 |
| 2021-08-25 20:10:46 | × | orcus quits (~orcus@mail.brprice.uk) (Client Quit) |
| 2021-08-25 20:11:16 | → | mastarija joins (~mastarija@78-3-210-70.adsl.net.t-com.hr) |
| 2021-08-25 20:11:38 | → | ec_ joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-25 20:12:45 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-08-25 20:12:56 | → | acidjnk joins (~acidjnk@p200300d0c72b9541f8d5911f73b02544.dip0.t-ipconnect.de) |
| 2021-08-25 20:12:57 | → | orcus joins (~orcus@user/brprice) |
| 2021-08-25 20:13:27 | × | xff0x quits (~xff0x@2001:1a81:536c:3300:2715:adb6:6b2e:5e0d) (Ping timeout: 240 seconds) |
| 2021-08-25 20:14:33 | → | xff0x joins (~xff0x@2001:1a81:536c:3300:1de6:1836:7ec4:e477) |
| 2021-08-25 20:14:56 | × | Guest9305 quits (~chris@81.96.113.213) (Ping timeout: 250 seconds) |
| 2021-08-25 20:17:03 | × | orcus quits (~orcus@user/brprice) (Client Quit) |
| 2021-08-25 20:17:03 | × | dispater quits (~dispater@user/brprice) (Quit: ZNC 1.8.1 - https://znc.in) |
| 2021-08-25 20:19:03 | → | dispater joins (~dispater@user/brprice) |
| 2021-08-25 20:19:35 | → | orcus joins (~orcus@user/brprice) |
| 2021-08-25 20:20:39 | × | oxide quits (~lambda@user/oxide) (Quit: oxide) |
| 2021-08-25 20:23:20 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:d4c9:355c:bd9d:df19) |
| 2021-08-25 20:25:07 | × | jtomas_ quits (~jtomas@233.red-83-34-2.dynamicip.rima-tde.net) (Ping timeout: 252 seconds) |
| 2021-08-25 20:29:08 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 2021-08-25 20:33:51 | → | oxide joins (~lambda@user/oxide) |
| 2021-08-25 20:33:58 | × | oxide quits (~lambda@user/oxide) (Client Quit) |
| 2021-08-25 20:35:56 | × | elf_fortrez quits (~elf_fortr@adsl-72-50-4-45.prtc.net) (Quit: Client closed) |
| 2021-08-25 20:40:03 | → | mcglk_ joins (~mcglk@131.191.49.120) |
| 2021-08-25 20:41:28 | × | mcglk quits (~mcglk@131.191.49.120) (Ping timeout: 268 seconds) |
| 2021-08-25 20:43:06 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 250 seconds) |
| 2021-08-25 20:44:12 | × | ec_ quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-25 20:44:31 | → | Alicebudda joins (~Alicebudd@cold.passenger.volia.net) |
| 2021-08-25 20:45:05 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-08-25 20:45:05 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host) |
| 2021-08-25 20:45:05 | → | wroathe joins (~wroathe@user/wroathe) |
| 2021-08-25 20:50:36 | <siers> | how does one use Data.Type.Equality practically? what is it for? https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-Type-Equality.html |
| 2021-08-25 20:51:03 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:d4c9:355c:bd9d:df19) (Remote host closed the connection) |
| 2021-08-25 20:52:07 | × | Topsi quits (~Tobias@dyndsl-095-033-024-207.ewe-ip-backbone.de) (Ping timeout: 240 seconds) |
| 2021-08-25 20:55:16 | → | ec_ joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-25 20:55:25 | → | markpythonicbtc joins (~textual@2601:647:5a00:35:780a:5d22:10f6:8b18) |
| 2021-08-25 20:56:12 | <monochrom> | IIRC Data.Typeable has a use case. |
| 2021-08-25 20:56:16 | → | Alicebudda74 joins (~Alicebudd@cold.passenger.volia.net) |
| 2021-08-25 20:56:39 | <Ollie[m]> | siers: that's a hard one to answer, but generally when you have some `T a`, and you want to learn what `a` actually is, you need equality proofs |
| 2021-08-25 20:57:05 | <Ollie[m]> | For example, `T` might be a GADT, and you might to prove that if someone gives you a `T a`, they've actually given you a `T Bool` |
| 2021-08-25 20:58:10 | × | Alicebudda quits (~Alicebudd@cold.passenger.volia.net) (Ping timeout: 246 seconds) |
| 2021-08-25 20:58:34 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:d4c9:355c:bd9d:df19) |
| 2021-08-25 21:00:28 | × | fendor_ quits (~fendor@91.141.62.191.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 2021-08-25 21:01:14 | <siers> | so you'd have `a :~: Bool` passed to make use of that `ta :: T a`? what do you do with it then? does this mean you can convert that `ta` to, say, `Maybe Bool`? |
| 2021-08-25 21:02:21 | <siers> | is it easier to learn what it does/how it works by simply learning agda instead? :) |
| 2021-08-25 21:07:03 | × | amahl quits (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Ping timeout: 250 seconds) |
| 2021-08-25 21:07:45 | × | d0ku quits (~d0ku@178.43.56.75.ipv4.supernova.orange.pl) (Ping timeout: 248 seconds) |
| 2021-08-25 21:08:10 | → | nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-08-25 21:11:02 | <maerwald> | so who managed to do partial static linking on windows? |
| 2021-08-25 21:11:15 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2021-08-25 21:11:27 | × | mikoto-chan quits (~mikoto-ch@ip-83-134-2-136.dsl.scarlet.be) (Ping timeout: 240 seconds) |
| 2021-08-25 21:11:46 | <maerwald> | so that mingw c libs are statically linked |
| 2021-08-25 21:12:49 | × | ubert quits (~Thunderbi@178.165.195.172.wireless.dyn.drei.com) (Remote host closed the connection) |
| 2021-08-25 21:13:07 | × | nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 250 seconds) |
| 2021-08-25 21:13:30 | <Ollie[m]> | siers: it's certainly easier to learn about when you are working with/familiar with dependant types |
| 2021-08-25 21:13:45 | <Ollie[m]> | How about checking out Richard Eisenberg's functional pearl? |
| 2021-08-25 21:14:12 | <Ollie[m]> | It's about building a compiler - I think it's all called Stich |
| 2021-08-25 21:14:20 | <Ollie[m]> | https://richarde.dev/papers/2018/stitch/stitch.pdf |
| 2021-08-25 21:16:30 | → | Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 2021-08-25 21:16:52 | → | jtomas_ joins (~jtomas@233.red-83-34-2.dynamicip.rima-tde.net) |
| 2021-08-25 21:16:57 | <siers> | I'll take a look |
| 2021-08-25 21:17:07 | → | schuelermine joins (~anselmsch@user/schuelermine) |
| 2021-08-25 21:17:31 | × | schuelermine quits (~anselmsch@user/schuelermine) (Client Quit) |
All times are in UTC.