Logs: liberachat/#haskell
| 2026-04-23 11:29:30 | × | arandombit quits (~arandombi@2a02:2455:8656:7100:a1d8:57d9:a02:f1ad) (Changing host) |
| 2026-04-23 11:29:30 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-23 11:31:27 | × | Googulator54 quits (~Googulato@84-236-65-56.pool.digikabel.hu) (Ping timeout: 245 seconds) |
| 2026-04-23 11:33:52 | → | layline_ joins (~layline@149.154.26.56) |
| 2026-04-23 11:33:52 | layline_ | is now known as layline-away |
| 2026-04-23 11:33:54 | → | puke joins (~puke@user/puke) |
| 2026-04-23 11:35:14 | layline-away | is now known as layline_ |
| 2026-04-23 11:35:52 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 2026-04-23 11:36:19 | → | tremon joins (~tremon@83.80.159.219) |
| 2026-04-23 11:42:57 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 272 seconds) |
| 2026-04-23 11:46:57 | × | misterfish quits (~misterfis@89.205.247.219) (Ping timeout: 255 seconds) |
| 2026-04-23 11:48:07 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-23 11:49:36 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 2026-04-23 12:07:09 | <haskellbridge> | <slack1256> I do not see anything related to lambdas on there (apart from nix?) |
| 2026-04-23 12:08:52 | <humasect> | maybe the french language? TIL haskell is american |
| 2026-04-23 12:20:51 | × | Googulator72 quits (~Googulato@78-131-16-66.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-23 12:21:07 | → | Googulator72 joins (~Googulato@78-131-16-66.pool.digikabel.hu) |
| 2026-04-23 12:26:07 | × | CiaoSen quits (~Jura@p549cbfb1.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2026-04-23 12:27:37 | → | misterfish joins (~misterfis@84.53.85.146) |
| 2026-04-23 12:30:09 | → | CiaoSen joins (~Jura@p549cbfb1.dip0.t-ipconnect.de) |
| 2026-04-23 12:32:45 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 265 seconds) |
| 2026-04-23 12:33:24 | → | califax_ joins (~califax@user/califx) |
| 2026-04-23 12:33:28 | → | gmg joins (~user@user/gehmehgeh) |
| 2026-04-23 12:36:08 | × | califax quits (~califax@user/califx) (Ping timeout: 265 seconds) |
| 2026-04-23 12:36:08 | califax_ | is now known as califax |
| 2026-04-23 12:42:31 | → | polykernel_ joins (~polykerne@user/polykernel) |
| 2026-04-23 12:44:36 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 2026-04-23 12:44:36 | × | tusko quits (~uwu@user/tusko) (Remote host closed the connection) |
| 2026-04-23 12:44:52 | → | tusko joins (~uwu@user/tusko) |
| 2026-04-23 12:44:53 | → | califax joins (~califax@user/califx) |
| 2026-04-23 12:45:10 | × | polykernel quits (~polykerne@user/polykernel) (Ping timeout: 245 seconds) |
| 2026-04-23 12:45:10 | polykernel_ | is now known as polykernel |
| 2026-04-23 12:48:37 | layline_ | is now known as layline-away |
| 2026-04-23 12:50:29 | × | layline-away quits (~layline@149.154.26.56) (Quit: ZZZzzz…) |
| 2026-04-23 12:52:18 | → | comerijn joins (~merijn@77.242.116.146) |
| 2026-04-23 12:54:09 | × | Googulator72 quits (~Googulato@78-131-16-66.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-23 12:54:22 | → | Googulator72 joins (~Googulato@78-131-16-66.pool.digikabel.hu) |
| 2026-04-23 12:55:21 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 2026-04-23 13:02:23 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-04-23 13:02:42 | × | CiaoSen quits (~Jura@p549cbfb1.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2026-04-23 13:21:16 | → | AlexNoo joins (~AlexNoo@85.174.181.200) |
| 2026-04-23 13:24:18 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 244 seconds) |
| 2026-04-23 13:34:22 | → | kuribas joins (~user@2a02:1808:51:6776:c5ce:b7ef:828f:40c5) |
| 2026-04-23 13:35:10 | × | xff0x quits (~xff0x@2405:6580:b080:900:ef2d:650d:209c:a61) (Ping timeout: 245 seconds) |
| 2026-04-23 13:36:07 | × | szkl quits (uid110435@2a03:5180:f:5::1:af63) (Quit: Connection closed for inactivity) |
| 2026-04-23 13:39:31 | <kuribas> | How would you model concurrent threads in a pure way, to proof properties? |
| 2026-04-23 13:39:44 | <kuribas> | Maybe each thread is a Free monad, which you can interleave? |
| 2026-04-23 13:39:55 | → | xff0x joins (~xff0x@2405:6580:b080:900:ef2d:650d:209c:a61) |
| 2026-04-23 13:50:38 | × | beagles_ quits (~beagles@142.163.133.95) (Remote host closed the connection) |
| 2026-04-23 13:51:29 | ski | . o O ( "A Poor Man's Concurrency Monad" by Koen Claessen in 1999-05 at <https://web.archive.org/web/20080222023959/http://www.cs.chalmers.se/~koen/pubs/entry-jfp99-monad.html> ) |
| 2026-04-23 13:54:10 | → | emaczen joins (~user@user/emaczen) |
| 2026-04-23 13:57:37 | × | shr\ke quits (~shrike@user/shrke:31298) (Remote host closed the connection) |
| 2026-04-23 13:58:22 | → | shr\ke joins (~shrike@user/paxhumana) |
| 2026-04-23 13:58:22 | × | shr\ke quits (~shrike@user/paxhumana) (Changing host) |
| 2026-04-23 13:58:22 | → | shr\ke joins (~shrike@user/shrke:31298) |
| 2026-04-23 13:58:43 | × | juri_ quits (~juri@217-114-215-140.pool.ovpn.com) (Ping timeout: 276 seconds) |
| 2026-04-23 14:10:10 | → | juri_ joins (~juri@217-114-215-140.pool.ovpn.com) |
| 2026-04-23 14:22:55 | → | machinedgod joins (~machinedg@d172-219-48-230.abhsia.telus.net) |
| 2026-04-23 14:24:04 | × | GdeVolpiano quits (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 245 seconds) |
| 2026-04-23 14:25:53 | → | GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano) |
| 2026-04-23 14:38:36 | × | puke quits (~puke@user/puke) (Remote host closed the connection) |
| 2026-04-23 14:39:01 | → | puke joins (~puke@user/puke) |
| 2026-04-23 14:39:28 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2026-04-23 14:42:29 | <comerijn> | kuribas: CSP? |
| 2026-04-23 14:42:39 | <comerijn> | Not to be confused with CPS :p |
| 2026-04-23 14:43:13 | <comerijn> | kuribas: I've done proofs about CSP using mu-calculus |
| 2026-04-23 14:44:38 | <kuribas> | comerijn: which tool is that? |
| 2026-04-23 14:49:51 | <comerijn> | We used muCRL |
| 2026-04-23 14:49:52 | <comerijn> | https://ir.cwi.nl/pub/4746 |
| 2026-04-23 14:50:42 | <comerijn> | Basically modelling things as CSP and the proving certain event traces are impossible |
| 2026-04-23 14:53:07 | <comerijn> | There's other mathematical models for concurrency, but I'm not aware of any as well known as CSP |
| 2026-04-23 14:53:14 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 245 seconds) |
| 2026-04-23 14:54:19 | <kuribas> | Couldn't I represent a thread as "Free (StateF s) a". |
| 2026-04-23 14:55:20 | → | misterfish joins (~misterfis@84.53.85.146) |
| 2026-04-23 14:55:22 | <comerijn> | kuribas: How do you represent communication between threads? |
| 2026-04-23 14:56:27 | <kuribas> | Store a mutex in the state? |
| 2026-04-23 14:56:56 | <kuribas> | "Free (StateF (MutexStore) a". |
| 2026-04-23 14:58:32 | <kuribas> | Maybe a custom StateF with extra primitives for accessing mutexes. |
| 2026-04-23 14:58:38 | → | haritz joins (~hrtz@140.228.70.141) |
| 2026-04-23 14:58:38 | × | haritz quits (~hrtz@140.228.70.141) (Changing host) |
| 2026-04-23 14:58:38 | → | haritz joins (~hrtz@user/haritz) |
| 2026-04-23 15:05:48 | <comerijn> | kuribas: Right, but then it's no longer a pure model :p |
| 2026-04-23 15:05:58 | <kuribas> | Why not? |
| 2026-04-23 15:06:41 | <comerijn> | Oh, wait, you mean have free model all threads at once? |
| 2026-04-23 15:06:47 | <comerijn> | Then you're just reinventing CSP ;) |
| 2026-04-23 15:06:49 | <kuribas> | yes |
| 2026-04-23 15:06:52 | <kuribas> | ah right :) |
| 2026-04-23 15:18:15 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 2026-04-23 15:18:29 | × | srazkvt quits (~sarah@user/srazkvt) (Ping timeout: 244 seconds) |
| 2026-04-23 15:18:32 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-04-23 15:18:39 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds) |
| 2026-04-23 15:18:39 | tnt2 | is now known as tnt1 |
| 2026-04-23 15:20:40 | → | Square3 joins (~Square@user/square) |
| 2026-04-23 15:21:15 | → | AlexZenon joins (~alzenon@85.174.181.200) |
| 2026-04-23 15:23:30 | × | Square2 quits (~Square4@user/square) (Ping timeout: 248 seconds) |
| 2026-04-23 15:24:32 | × | puke quits (~puke@user/puke) (Ping timeout: 250 seconds) |
| 2026-04-23 15:26:12 | <kuribas> | comerijn: wouldn't it be nice to have something in idris2 or agda though? |
| 2026-04-23 15:31:57 | × | tnt1 quits (~Thunderbi@user/tnt1) (Quit: tnt1) |
| 2026-04-23 15:32:48 | → | accountant joins (~accountan@2600:1702:5b61:8b40:955:b655:442f:e301) |
| 2026-04-23 15:35:21 | jmcantrell_ | is now known as jmcantrell |
All times are in UTC.