Logs: liberachat/#haskell
| 2021-06-11 02:03:13 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:2121:a570:d35e:ba7a) (Remote host closed the connection) |
| 2021-06-11 02:03:23 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:2121:a570:d35e:ba7a) |
| 2021-06-11 02:03:28 | <qrpnxz> | right but i just have to say "instance...". I'm playing around with alternative. functions `some` and `many` hang, not to sure how ppl use this |
| 2021-06-11 02:04:19 | → | Shaeto joins (~Shaeto@94.25.234.158) |
| 2021-06-11 02:08:49 | × | Shaeto quits (~Shaeto@94.25.234.158) (Ping timeout: 245 seconds) |
| 2021-06-11 02:08:55 | → | yd502_ joins (~yd502@180.168.212.6) |
| 2021-06-11 02:09:39 | × | td_ quits (~td@94.134.91.190) (Ping timeout: 245 seconds) |
| 2021-06-11 02:10:48 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-11 02:10:56 | <qrpnxz> | some and many don't appear to do different things actually i'm confused |
| 2021-06-11 02:11:29 | → | td_ joins (~td@94.134.91.189) |
| 2021-06-11 02:11:39 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection) |
| 2021-06-11 02:12:21 | × | awth13 quits (~user@user/awth13) (Ping timeout: 252 seconds) |
| 2021-06-11 02:12:58 | × | yd502__ quits (~yd502@180.168.212.6) (Ping timeout: 272 seconds) |
| 2021-06-11 02:13:29 | → | Shaeto joins (~Shaeto@94.25.234.158) |
| 2021-06-11 02:13:46 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 2021-06-11 02:15:04 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 245 seconds) |
| 2021-06-11 02:15:30 | × | xff0x_ quits (~xff0x@2001:1a81:5346:bf00:2779:734e:bb13:8382) (Ping timeout: 272 seconds) |
| 2021-06-11 02:15:41 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2021-06-11 02:15:57 | → | xff0x_ joins (~xff0x@2001:1a81:5346:bf00:6e52:b23e:6fc2:e844) |
| 2021-06-11 02:16:50 | <lyxia> | try getting an empty list out of some |
| 2021-06-11 02:16:53 | → | catern joins (~sbaugh@2604:2000:8fc0:b:a9c7:866a:bf36:3407) |
| 2021-06-11 02:17:15 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-11 02:17:18 | × | yd502_ quits (~yd502@180.168.212.6) (Ping timeout: 252 seconds) |
| 2021-06-11 02:18:20 | × | Shaeto quits (~Shaeto@94.25.234.158) (Ping timeout: 264 seconds) |
| 2021-06-11 02:19:19 | <catern> | is there a good non-theory explanation of practical uses of programs-as-proofs? for things other than theorem proving |
| 2021-06-11 02:20:32 | → | awth13 joins (~user@user/awth13) |
| 2021-06-11 02:22:54 | <qrpnxz> | lyxia, idk what that means. Even trying something like `take 3` on it doesn't seem to help with the hanging issue |
| 2021-06-11 02:23:16 | <qrpnxz> | to me it looks like it's doing an infinite list of a value, but i can't access it |
| 2021-06-11 02:23:34 | → | yd502_ joins (~yd502@180.168.212.6) |
| 2021-06-11 02:25:45 | <justsomeguy> | catern: Do any of the examples here qualify? https://ucsd-progsys.github.io/liquidhaskell-blog/ |
| 2021-06-11 02:27:48 | <catern> | justsomeguy: I guess that qualifies for what I said, but I should give an additional constraint (which replaces my theorem proving constraint): "in the absence of fancy types (such as dependent types)" |
| 2021-06-11 02:28:34 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.0.1) |
| 2021-06-11 02:30:03 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-11 02:31:13 | <catern> | (although I'm not sure even that qualifies... a dependent type lets you place constraints on what the inhabitants of a type are... but then using the resulting terms of that type isn't exactly a manifestation of programs-as-proofs, since knowing that the type is inhabited doesn't actually *tell* you anything, besides that the type is inhabited, which for the type of a pure function like in that example, isn't typically useful) |
| 2021-06-11 02:31:42 | → | Shaeto joins (~Shaeto@94.25.234.158) |
| 2021-06-11 02:32:47 | × | teaSlurper quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2021-06-11 02:33:20 | × | yd502_ quits (~yd502@180.168.212.6) (Ping timeout: 264 seconds) |
| 2021-06-11 02:34:01 | → | yd502 joins (~yd502@180.168.212.6) |
| 2021-06-11 02:34:05 | FinnElija | is now known as Guest9778 |
| 2021-06-11 02:34:05 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 2021-06-11 02:34:05 | × | Guest9778 quits (~finn_elij@user/finn-elija/x-0085643) (Killed (tin.libera.chat (Nickname regained by services))) |
| 2021-06-11 02:34:05 | finn_elija | is now known as FinnElija |
| 2021-06-11 02:34:32 | × | yahb quits (xsbot@user/mniip/bot/yahb) (Ping timeout: 264 seconds) |
| 2021-06-11 02:34:38 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 265 seconds) |
| 2021-06-11 02:35:27 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-06-11 02:36:33 | × | Shaeto quits (~Shaeto@94.25.234.158) (Ping timeout: 252 seconds) |
| 2021-06-11 02:38:12 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 252 seconds) |
| 2021-06-11 02:38:46 | → | yahb joins (xsbot@user/mniip/bot/yahb) |
| 2021-06-11 02:40:50 | → | Shaeto joins (~Shaeto@94.25.234.158) |
| 2021-06-11 02:41:19 | × | ec_ quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 252 seconds) |
| 2021-06-11 02:41:30 | × | shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 252 seconds) |
| 2021-06-11 02:44:58 | × | hammock quits (~Hammock@2600:1700:19a1:3330::625) (Quit: WeeChat 3.0.1) |
| 2021-06-11 02:45:56 | × | Shaeto quits (~Shaeto@94.25.234.158) (Ping timeout: 264 seconds) |
| 2021-06-11 02:54:50 | <bontaq`> | idk, all the proof assistants have dependent types or stronger |
| 2021-06-11 02:57:37 | <Axman6> | I've gelkt for a while that just having sum types and not allowing partial functions gets you a very long way in proving that you have handled everything that's possible in your program. writing functions which can operate over that domain proves that you have handled all cases, which for most practical work is better than you get in most languages |
| 2021-06-11 02:57:43 | <Axman6> | felt* |
| 2021-06-11 02:59:06 | → | Shaeto joins (~Shaeto@94.25.234.158) |
| 2021-06-11 03:00:06 | <keltono> | bontaq`: well, not _all_ of them (https://en.wikipedia.org/wiki/Isabelle_(proof_assistant), for one) |
| 2021-06-11 03:02:08 | <bontaq`> | :P |
| 2021-06-11 03:02:41 | × | yd502 quits (~yd502@180.168.212.6) (Ping timeout: 268 seconds) |
| 2021-06-11 03:03:44 | → | yd502 joins (~yd502@180.168.212.6) |
| 2021-06-11 03:04:19 | × | Shaeto quits (~Shaeto@94.25.234.158) (Ping timeout: 272 seconds) |
| 2021-06-11 03:08:13 | → | Shaeto joins (~Shaeto@94.25.234.158) |
| 2021-06-11 03:09:36 | <qrpnxz> | how do get declarations in an import to replace declarations from prelude? |
| 2021-06-11 03:09:39 | → | cpnuj joins (~cpnuj@217.163.30.217) |
| 2021-06-11 03:12:18 | × | cpnuj quits (~cpnuj@217.163.30.217) (Client Quit) |
| 2021-06-11 03:12:20 | × | awth13 quits (~user@user/awth13) (Ping timeout: 265 seconds) |
| 2021-06-11 03:12:25 | <Axman6> | qrpnxz: here's a few ways, which is the correct one will depend on the specific import though, there's some idioms that are used for some modules and not others |
| 2021-06-11 03:12:57 | <qrpnxz> | In my case i wanted Text.IO to subplant the prelude defaults |
| 2021-06-11 03:13:08 | × | Shaeto quits (~Shaeto@94.25.234.158) (Ping timeout: 272 seconds) |
| 2021-06-11 03:13:09 | <hololeap> | qrpnxz: in regards to some and many, look into parsing libraries like parsec. that should give you an intuition for how those functions are used |
| 2021-06-11 03:13:37 | <hololeap> | it doesn't work very well for most Alternatives found in base |
| 2021-06-11 03:14:05 | <Axman6> | well one option is to do import Prelude hiding (functionsThat, youUseIn, your, code) |
| 2021-06-11 03:14:08 | <qrpnxz> | yeah that makes sense but idk why i'm unable to say `take 3` from a `some (Just 1)` idk what's going on there |
| 2021-06-11 03:14:28 | <qrpnxz> | Axman6, wow that's a lot of work, i'll just qualify it |
| 2021-06-11 03:14:46 | <Axman6> | yeah, usually people will just do import Data.Text.IO as T |
| 2021-06-11 03:15:02 | <Axman6> | qualified as T* |
| 2021-06-11 03:15:35 | <Axman6> | a fairly common thing to do is: import Data.Text.IO qualified as T; import Data.Text.IO (nonClashing,names) |
| 2021-06-11 03:15:56 | × | BosonCollider quits (~olofs@90-227-86-119-no542.tbcn.telia.com) (Ping timeout: 264 seconds) |
| 2021-06-11 03:17:22 | → | Shaeto joins (~Shaeto@94.25.234.158) |
| 2021-06-11 03:21:45 | × | cdsmith quits (~cdsmithma@2001:470:69fc:105::284) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | ru0mad[m] quits (~ru0madmat@2001:470:69fc:105::9b2) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | Drezil quits (~drezilkif@2001:470:69fc:105::7f8) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | Artem[m] quits (~artemtype@2001:470:69fc:105::75b) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | wallymathieu[m] quits (~wallymath@2001:470:69fc:105::16ae) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | cdepillabout[m] quits (~cdepillab@2001:470:69fc:105::3d3) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | amesgen[m] quits (~amesgenam@2001:470:69fc:105::82b) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | eddiemundo quits (~eddiemund@2001:470:69fc:105::a9c) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | Soft quits (~soft-matr@2001:470:69fc:105::c75) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | autrim64[m] quits (~autrim64m@2001:470:69fc:105::16a1) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | RohitGoswami[m] quits (~rgoswamim@2001:470:69fc:105::16cc) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | Las[m] quits (~lasmatrix@2001:470:69fc:105::74e) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | ServerStatsDisco quits (~serversta@2001:470:69fc:105::1a) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | the-coot[m] quits (~the-cootm@2001:470:69fc:105::95f) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | psydroid quits (~psydroidm@user/psydroid) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:45 | × | ac quits (~aloiscoch@2001:470:69fc:105::65) (Ping timeout: 244 seconds) |
| 2021-06-11 03:21:55 | × | jophish quits (~jophish@2001:470:69fc:105::670) (Ping timeout: 264 seconds) |
| 2021-06-11 03:21:55 | × | kadoban quits (~kadoban@user/kadoban) (Ping timeout: 264 seconds) |
| 2021-06-11 03:21:55 | × | MatrixTravelerbo quits (~voyagert2@2001:470:69fc:105::22) (Ping timeout: 264 seconds) |
| 2021-06-11 03:22:03 | × | bitonic quits (~bitonicma@2001:470:69fc:105::1812) (Ping timeout: 244 seconds) |
All times are in UTC.