Home liberachat/#haskell: Logs Calendar

Logs on 2025-06-02 (liberachat/#haskell)

00:01:33 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
00:01:53 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
00:04:15 × jespada quits (~jespada@r167-61-127-149.dialup.adsl.anteldata.net.uy) (Ping timeout: 276 seconds)
00:07:50 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
00:07:58 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
00:08:14 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
00:08:24 → ljdarj1 joins (~Thunderbi@user/ljdarj)
00:10:04 × phma quits (~phma@host-67-44-208-56.hnremote.net) (Read error: Connection reset by peer)
00:10:50 → phma joins (~phma@2001:5b0:210d:9c38:6091:34d1:6f16:4051)
00:12:17 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
00:12:17 ljdarj1 is now known as ljdarj
00:15:03 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
00:15:25 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
00:19:07 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
00:21:43 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
00:22:07 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
00:23:45 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
00:29:35 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
00:29:57 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
00:34:54 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
00:36:22 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
00:36:44 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
00:39:55 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
00:42:54 <EvanR> any clue why this is happening or if I'm just tripping. readFile on a named pipe acts normally the first time you open the fifo, "blocking" until a writer appears and starts sending data, then the lazy list terminates when the writer closes the fifo
00:43:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
00:43:03 × Digit quits (~user@user/digit) (Ping timeout: 244 seconds)
00:43:13 <EvanR> after consuming the entire list, another call to readFile on the fifo immediately returns []
00:43:23 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
00:44:20 <geekosaur> that's standard fifo behavior, yes
00:44:33 <EvanR> so you can never reopen a fifo?
00:44:38 <geekosaur> right
00:45:13 <geekosaur> you need to hold it open `O_RDWR` and have some protocol for "end of current connection". or use an `AF_LOCAL` socket, which behaves the way you want FIFOs to work
00:46:10 <geekosaur> actually this isn't 100% POSIXX behavior, `readFile` and the somewhat weird Haskell Report-specified semantics of lazy I/O are contributing
00:46:41 <geekosaur> the two together make FIFOs kinda unusable in Haskell
00:46:43 → Digit joins (~user@user/digit)
00:47:05 <geekosaur> but that's only slightly worse than the normal POSIX behavior
00:47:21 <geekosaur> really, just don't use FIFOs
00:49:54 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
00:50:17 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
00:50:28 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
00:50:44 <EvanR> I don't understand the condition which causes a 2nd opening of the fifo to instantly return EOF
00:50:58 <EvanR> e.g. I can run the program again or a second program to open it and it blocks
00:51:07 <EvanR> for reading
00:51:20 <EvanR> is it like "one process, one opening"
00:51:56 <EvanR> come back with another process if you want more fifo
00:52:11 <geekosaur> yes
00:52:15 <EvanR> interesting
00:52:54 <geekosaur> POSIX FIFO semantics come from UNIX System III/V and are rather strange
00:54:02 <geekosaur> I only know of one program which made useful use of them: on System V R3, `cron` opened a private FIFO for read/write and listened for lines written by `crontab`, which told it to reread the specified crontab file
00:55:49 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
00:56:15 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
00:56:36 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
00:57:59 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
00:58:38 <geekosaur> btw I think what causes that instant-EOF behavior is that the RTS opens it non-blocking, then `readFile` sets up an `unsafeInterleaveIO` which fails on the first read, which is passed back to you as EOF
00:59:39 <geekosaur> lazy I/O doesn't hande exceptional conditions at all well
01:02:39 <EvanR> I tried using openFile and hGetLine
01:02:43 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:02:52 <geekosaur> so anyway FIFOs are broken, lazy I/O is broken, if you use them together you get to keep all the shattered pieces
01:03:05 <EvanR> same result, first it blocks waiting for a writer, second time it suceeds immediately but hGetLine throws because EOF
01:03:05 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:03:33 <EvanR> is it open blocking the first time and non-blocking the second time
01:04:25 <geekosaur> it should always be non-blocking, I think? the RTS doesn't use blocking fds because that would block the whole process instead of just the running thread
01:04:29 <EvanR> if this can't be adjusted I'm not sure how that crontab trick even worked
01:04:41 <EvanR> opening the first time blocks if there's no writer yet
01:05:02 <geekosaur> because only writers close it. cron kept it open O_RDWR|O_NONBLOCK continuously
01:05:16 <EvanR> oh
01:05:35 <EvanR> i'll try opening it RDWR
01:05:40 <geekosaur> so it never saw EOF, it just relied on every "record" being a single line
01:06:16 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:06:24 <EvanR> that made it behave
01:07:58 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:08:23 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:08:30 <EvanR> it causes reader to not see EOF from writers closing
01:08:43 <EvanR> which is good enough for government work
01:09:10 <EvanR> but also closing and reopening a second time gives blocking behavior again
01:09:17 <EvanR> weird
01:11:11 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
01:14:50 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:15:13 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:16:23 <EvanR> if the RTS puts all file I/O through the select mechanism they wouldn't need to be non-blocking right
01:16:47 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:16:49 <EvanR> since then it knows if a read or write would block
01:17:11 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:18:28 <monochrom> It is still simpler to keep using the non-blocking mode.
01:20:32 <EvanR> does it make any difference if it's all selected?
01:21:09 <monochrom> Suppose two threads race to read from the same FD. Suppose select detects that data has arrived. Should the RTS wake up just one of them? Or both of them? Either way is easily broken under blocking mode because you don't know how much each thread actually reads.
01:21:11 <geekosaur> yes, because it affects semantics of the FIFO, not just blocking-ness
01:21:22 <geekosaur> also that
01:21:47 <monochrom> I don't mean it is unsolvable. There is a way you can go out of your way to fool-proof that.
01:22:01 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
01:22:03 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:22:03 × xff0x quits (~xff0x@2405:6580:b080:900:9dbe:32d6:8014:9bea) (Ping timeout: 268 seconds)
01:22:19 <EvanR> the RTS doesn't just make 1 thread at a time accessing the FD
01:22:22 <monochrom> Alternatively, non-blocking mode relieves you from working so hard, while still be completely safe and correct.
01:22:22 <EvanR> ?
01:23:48 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:24:11 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:25:24 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:25:25 <EvanR> k I messed up my original test by also pipe the fifo to stdin
01:25:32 <EvanR> now the behavior with lazy I/O is consistent
01:25:52 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:25:59 <EvanR> it *always* immediately returns an empty list
01:26:45 <monochrom> OK, even better example without racing. 2 bytes have arrived. But the thread called read(fd, buf, 10). Blocking mode hangs that read() waiting for 8 more bytes (or EOF or error).
01:26:58 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
01:27:16 <monochrom> GHC uses green threads so all of RTS hangs.
01:27:35 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Read error: Connection reset by peer)
01:28:58 <int-e> You should get a partial read; it's supposed to block only when no data is available at all.
01:29:09 × _d0t quits (~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 252 seconds)
01:29:23 <EvanR> yes it returns less than requested in blocking mode
01:29:27 <monochrom> At this point I hope you don't react like my students. They are lazy and switch to read(fd, buf, 1) and be egregiously inefficient. GHC RTS cannot afford to do that, people would riot.
01:29:49 <monochrom> Ah OK my bad.
01:30:02 <EvanR> that's why you have to repeatedly write until everything goes through since it might return less than what you wanted to write
01:30:49 <int-e> fread() does that loop for you, so if you took your semantics from there you'd be right.
01:31:56 <int-e> (you still get partial reads but only on actual errors or EOF)
01:32:08 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:32:31 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:32:51 <int-e> Anyway. This shouldn't distract from the point that read *can* block if the fd is not in non-blocking mode, and allowing blind reads simplifies some code..
01:35:07 <int-e> ...and break some foreign libraries that you might want to pass fds to as a bonus. ;-)
01:36:21 → mange joins (~mange@user/mange)
01:37:51 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:38:01 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
01:38:15 → _d0t joins (~{-d0t-}@user/-d0t-/x-7915216)
01:39:49 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:40:11 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:45:05 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
01:45:11 × haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
01:45:42 → haritz joins (~hrtz@152.37.64.162)
01:45:43 × haritz quits (~hrtz@152.37.64.162) (Changing host)
01:45:43 → haritz joins (~hrtz@user/haritz)
01:47:42 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:48:04 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:48:18 → jmcantrell joins (~weechat@user/jmcantrell)
01:55:41 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
01:55:54 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:56:06 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
01:57:21 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
02:00:26 → j1n37 joins (~j1n37@user/j1n37)
02:00:53 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
02:01:53 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
02:02:17 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
02:08:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
02:08:23 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
02:11:44 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:15:03 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
02:15:25 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
02:16:45 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
02:20:11 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:22:06 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
02:22:27 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
02:24:50 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
02:28:51 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
02:29:12 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
02:35:38 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
02:35:56 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:36:00 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
02:40:49 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
02:41:06 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
02:41:29 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
02:48:05 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
02:48:26 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
02:51:55 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:54:33 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
02:54:59 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
02:57:04 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
02:58:22 × td_ quits (~td@i53870925.versanet.de) (Ping timeout: 276 seconds)
02:59:32 → td_ joins (~td@i53870908.versanet.de)
03:01:40 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:02:01 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
03:07:42 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
03:09:05 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:09:23 <EvanR> this is fun, if I try to open a named pipe in haskell in WriteMode, to act as the writer, openFile: does not exist (No such device or address)
03:09:28 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
03:09:33 <EvanR> ReadWriteMode again "fixes" it
03:10:21 <EvanR> meanwhile in C it's the opposite, opening the "write only" fifo with fopen and "rw" causes it to fail to write, while "w" makes it behave
03:12:22 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
03:14:02 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:14:30 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
03:18:21 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
03:20:54 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:21:07 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
03:21:15 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
03:22:01 → j1n37 joins (~j1n37@user/j1n37)
03:23:32 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:23:57 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
03:27:58 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
03:30:29 <mauke> EvanR: "rw" is not a thing in fopen. did you mean "r+"?
03:30:51 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:31:16 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
03:32:41 <mauke> ENXIO is returned when you open a fifo in non-blocking mode for writing while there are no readers
03:33:32 <mauke> (in blocking mode, open() will block until there is a reader)
03:36:31 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:36:55 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
03:39:10 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
03:44:35 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
03:44:58 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:45:22 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
03:51:03 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:51:26 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
03:54:57 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
03:55:23 → xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
03:59:25 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
03:59:48 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
04:00:07 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
04:06:39 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
04:06:58 → trickard joins (~trickard@cpe-51-98-47-163.wireline.com.au)
04:07:01 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
04:10:32 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:13:00 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
04:13:22 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
04:15:53 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
04:16:38 <haskellbridge> <Liamzee> https://www.stackage.org/lts-23.24/hoogle?q=foo is this broken for anyone else?
04:16:55 <haskellbridge> <Liamzee> and hoogle seems to be pointing to haskell platform only, not stackage
04:18:48 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
04:19:10 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
04:22:07 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:22:23 <trickard> I get 502 bad gateway
04:23:29 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 260 seconds)
04:25:16 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
04:25:35 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
04:25:38 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
04:25:50 → michalz joins (~michalz@185.246.207.203)
04:25:59 → j1n37 joins (~j1n37@user/j1n37)
04:27:30 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
04:29:23 → tavare joins (~tavare@user/tavare)
04:29:32 × tavare quits (~tavare@user/tavare) (Remote host closed the connection)
04:32:40 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
04:33:15 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
04:33:40 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
04:35:42 → j1n37 joins (~j1n37@user/j1n37)
04:37:54 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:41:02 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
04:41:25 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
04:42:44 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
04:47:21 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
04:47:48 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
04:51:05 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
04:51:26 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
04:51:27 <haskellbridge> <sm> Stackage has its own separate Google
04:51:37 <haskellbridge> <sm> * hoogle
04:53:26 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:57:48 → Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
04:58:10 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
04:58:30 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds)
04:59:09 Lord_of_Life_ is now known as Lord_of_Life
04:59:09 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
04:59:19 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
04:59:43 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:00:28 → Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
05:02:08 → j1n37 joins (~j1n37@user/j1n37)
05:05:06 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
05:05:28 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:11:38 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
05:12:01 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:17:31 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
05:17:55 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:22:44 × tinjamin4 quits (~tinjamin@banshee.h4x0r.space) (Ping timeout: 272 seconds)
05:23:07 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
05:25:04 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
05:25:30 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:27:49 × internatetional quits (~nate@2404:c0:5c60::339d:583b) (Ping timeout: 272 seconds)
05:27:51 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
05:28:49 × trickard quits (~trickard@cpe-51-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
05:29:02 → trickard joins (~trickard@cpe-51-98-47-163.wireline.com.au)
05:30:18 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
05:30:49 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:35:39 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
05:36:00 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:38:55 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
05:39:12 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
05:41:41 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
05:42:04 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:44:16 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
05:45:18 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
05:45:46 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
05:46:07 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:47:42 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
05:51:39 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
05:52:47 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
05:53:12 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
05:54:41 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
05:58:22 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
05:59:46 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
06:00:51 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
06:01:19 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:02:35 → califax_ joins (~califax@user/califx)
06:03:31 × califax quits (~califax@user/califx) (Remote host closed the connection)
06:03:50 califax_ is now known as califax
06:07:42 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
06:08:03 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:08:10 × jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 276 seconds)
06:10:29 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
06:10:57 × haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
06:11:28 → JuanDaugherty joins (~juan@user/JuanDaugherty)
06:13:33 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
06:14:20 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
06:14:46 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:15:23 → CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
06:15:29 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
06:18:55 → machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
06:19:10 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
06:20:29 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
06:20:50 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:22:26 → j1n37 joins (~j1n37@user/j1n37)
06:22:33 × trickard quits (~trickard@cpe-51-98-47-163.wireline.com.au) (Ping timeout: 276 seconds)
06:24:09 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
06:25:35 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
06:26:01 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:26:50 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
06:29:29 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
06:30:05 → j1n37 joins (~j1n37@user/j1n37)
06:31:10 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
06:31:22 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
06:31:43 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:33:35 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
06:34:43 → j1n37 joins (~j1n37@user/j1n37)
06:34:54 → trickard joins (~trickard@cpe-51-98-47-163.wireline.com.au)
06:37:03 → werneta joins (~werneta@syn-071-083-160-242.res.spectrum.com)
06:38:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
06:38:27 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:39:55 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
06:40:00 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
06:44:07 × Digit quits (~user@user/digit) (Remote host closed the connection)
06:44:43 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
06:45:04 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:45:05 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
06:45:42 → j1n37 joins (~j1n37@user/j1n37)
06:49:41 → fp joins (~Thunderbi@wireless-86-50-140-9.open.aalto.fi)
06:51:16 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
06:51:39 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:51:51 → smalltalkman joins (uid545680@id-545680.hampstead.irccloud.com)
06:53:38 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Read error: Connection reset by peer)
06:55:09 → Digit joins (~user@user/digit)
06:55:41 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
06:58:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
06:58:25 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
06:59:09 → sawilagar joins (~sawilagar@user/sawilagar)
07:00:01 × caconym7 quits (~caconym@user/caconym) (Quit: bye)
07:00:04 × emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir)
07:00:26 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
07:00:42 → caconym7 joins (~caconym@user/caconym)
07:02:13 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:02:42 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:04:43 × werneta quits (~werneta@syn-071-083-160-242.res.spectrum.com) (Ping timeout: 276 seconds)
07:09:52 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:10:22 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:11:05 × trickard quits (~trickard@cpe-51-98-47-163.wireline.com.au) (Ping timeout: 260 seconds)
07:11:30 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
07:11:54 → rvalue- joins (~rvalue@user/rvalue)
07:13:10 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 276 seconds)
07:14:12 × Digit quits (~user@user/digit) (Remote host closed the connection)
07:14:19 → acidjnk joins (~acidjnk@p200300d6e71c4f46a4d9c5906f327091.dip0.t-ipconnect.de)
07:14:26 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
07:16:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:16:14 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
07:16:24 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:17:08 × econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
07:18:46 rvalue- is now known as rvalue
07:19:09 → Digit joins (~user@user/digit)
07:22:07 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:22:35 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:23:14 → trickard joins (~trickard@cpe-51-98-47-163.wireline.com.au)
07:24:05 → sord937 joins (~sord937@gateway/tor-sasl/sord937)
07:25:52 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:26:20 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:30:55 × fp quits (~Thunderbi@wireless-86-50-140-9.open.aalto.fi) (Ping timeout: 244 seconds)
07:32:14 → fp joins (~Thunderbi@wireless-86-50-140-9.open.aalto.fi)
07:34:02 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:34:22 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:34:26 → harveypwca joins (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c)
07:35:24 × harveypwca quits (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Remote host closed the connection)
07:39:44 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: irc.renjuan.org (juan@acm.org))
07:40:42 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:40:54 × developer_ quits (~developer@90.167.50.215) (Quit: Leaving)
07:41:05 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:41:19 → aman joins (~aman@user/aman)
07:41:46 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection)
07:42:21 → sord937 joins (~sord937@gateway/tor-sasl/sord937)
07:46:00 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:46:22 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:50:29 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:50:51 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:54:35 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
07:54:57 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
07:59:18 → ljdarj joins (~Thunderbi@user/ljdarj)
08:00:22 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
08:00:44 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:03:18 × aman quits (~aman@user/aman) (Ping timeout: 276 seconds)
08:04:18 × sawilagar quits (~sawilagar@user/sawilagar) (Read error: Connection reset by peer)
08:05:24 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
08:05:48 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:07:14 → tinjamin4 joins (~tinjamin@banshee.h4x0r.space)
08:09:16 → aman joins (~aman@user/aman)
08:10:00 → merijn joins (~merijn@77.242.116.146)
08:10:35 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
08:10:58 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:11:23 × tinjamin4 quits (~tinjamin@banshee.h4x0r.space) (Ping timeout: 252 seconds)
08:16:08 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
08:16:30 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:17:12 → ubert joins (~Thunderbi@2a02:8109:abb3:7000:51f4:aea7:1982:b1a4)
08:23:16 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
08:23:39 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:24:02 → Lycurgus joins (~juan@user/Lycurgus)
08:26:47 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
08:27:04 → sawilagar joins (~sawilagar@user/sawilagar)
08:27:07 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:30:03 → euandreh joins (~Thunderbi@189.6.105.228)
08:34:38 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
08:35:00 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:36:47 → dhil joins (~dhil@5.151.29.138)
08:39:56 → pointlessslippe1 joins (~pointless@62.106.85.17)
08:40:21 × pointlessslippe1 quits (~pointless@62.106.85.17) (Read error: Connection reset by peer)
08:40:22 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
08:40:43 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:45:53 × Lycurgus quits (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org))
08:46:02 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
08:46:04 → pointlessslippe1 joins (~pointless@62.106.85.17)
08:46:26 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:53:08 × euandreh quits (~Thunderbi@189.6.105.228) (Quit: euandreh)
08:53:43 → euandreh1 joins (~Thunderbi@189.31.61.8)
08:54:52 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
08:55:16 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
08:56:01 euandreh1 is now known as euandreh
08:56:51 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds)
08:59:52 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
09:00:12 × puke quits (~puke@user/puke) (Remote host closed the connection)
09:00:15 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
09:00:32 → puke joins (~puke@user/puke)
09:06:48 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
09:07:11 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
09:09:34 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
09:10:12 → __monty__ joins (~toonn@user/toonn)
09:15:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
09:15:25 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
09:20:33 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
09:25:27 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
09:28:59 → jmnyarega joins (~jmnyarega@user/jmnyarega)
09:29:02 × jmnyarega quits (~jmnyarega@user/jmnyarega) (Max SendQ exceeded)
09:30:49 → jmnyarega joins (~jmnyarega@user/jmnyarega)
09:30:51 × jmnyarega quits (~jmnyarega@user/jmnyarega) (Max SendQ exceeded)
09:31:06 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
09:31:27 → jmnyarega joins (~jmnyarega@user/jmnyarega)
09:31:29 × jmnyarega quits (~jmnyarega@user/jmnyarega) (Max SendQ exceeded)
09:32:12 → jmnyarega joins (~jmnyarega@user/jmnyarega)
09:32:14 × jmnyarega quits (~jmnyarega@user/jmnyarega) (Max SendQ exceeded)
09:33:05 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
09:33:29 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
09:38:19 × aman quits (~aman@user/aman) (Ping timeout: 245 seconds)
09:38:48 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
09:39:43 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
09:40:05 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
09:43:53 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
09:44:15 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
09:47:05 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds)
09:51:13 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
09:51:36 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
09:52:48 → merijn joins (~merijn@77.242.116.146)
09:53:17 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
09:53:42 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
09:53:43 × fp quits (~Thunderbi@wireless-86-50-140-9.open.aalto.fi) (Ping timeout: 276 seconds)
09:54:10 → szkl joins (uid110435@id-110435.uxbridge.irccloud.com)
09:55:40 → omegatron joins (~some@user/omegatron)
09:55:50 → aman joins (~aman@user/aman)
09:59:42 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:00:05 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:00:39 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
10:00:40 × dhil quits (~dhil@5.151.29.138) (Ping timeout: 252 seconds)
10:05:56 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:06:18 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:09:34 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Read error: Connection reset by peer)
10:10:29 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
10:10:33 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 252 seconds)
10:11:49 → iNomad joins (~iNomad@user/iNomad)
10:12:29 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:12:50 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:13:25 → dhil joins (~dhil@5.151.29.140)
10:16:48 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds)
10:18:15 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:18:40 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:25:05 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:25:29 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:26:05 → tinjamin4 joins (~tinjamin@banshee.h4x0r.space)
10:28:52 → ubert1 joins (~Thunderbi@2a02:8109:abb3:7000:4996:54f4:2d2d:1024)
10:29:33 → merijn joins (~merijn@77.242.116.146)
10:30:31 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:30:57 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:31:39 × xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 245 seconds)
10:32:16 × ubert quits (~Thunderbi@2a02:8109:abb3:7000:51f4:aea7:1982:b1a4) (Ping timeout: 244 seconds)
10:32:16 ubert1 is now known as ubert
10:35:29 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:35:51 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:37:37 → fp joins (~Thunderbi@wireless-86-50-140-9.open.aalto.fi)
10:41:39 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:42:05 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:50:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:50:17 × sawilagar quits (~sawilagar@user/sawilagar) (Read error: Connection reset by peer)
10:50:25 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:50:48 → ubert1 joins (~Thunderbi@ip5f59455a.dynamic.kabel-deutschland.de)
10:50:49 × ubert quits (~Thunderbi@2a02:8109:abb3:7000:4996:54f4:2d2d:1024) (Remote host closed the connection)
10:50:49 ubert1 is now known as ubert
10:51:06 → sawilagar joins (~sawilagar@user/sawilagar)
10:52:41 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
10:56:11 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
10:56:35 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
10:57:53 × orcus- quits (~orcus@2a03:4000:55:d87::1) (Quit: ZNC 1.8.2 - https://znc.in)
10:57:54 × dispater- quits (~dispater@202.61.255.182) (Quit: ZNC 1.8.2 - https://znc.in)
10:59:42 → dispater- joins (~dispater@2a03:4000:55:d87::1)
11:00:12 → orcus- joins (~orcus@2a03:4000:55:d87::1)
11:00:18 → ljdarj joins (~Thunderbi@user/ljdarj)
11:01:40 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:01:41 → jespada joins (~jespada@r167-61-127-149.dialup.adsl.anteldata.net.uy)
11:02:03 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:03:24 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
11:05:07 → CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
11:06:01 → comerijn joins (~merijn@77.242.116.146)
11:08:04 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:08:26 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:08:54 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds)
11:13:49 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:14:10 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:15:49 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:16:09 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:23:34 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:23:58 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:24:26 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
11:26:56 → xff0x joins (~xff0x@2405:6580:b080:900:effa:612a:1339:418c)
11:30:18 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
11:30:41 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:34:22 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
11:35:33 × fp quits (~Thunderbi@wireless-86-50-140-9.open.aalto.fi) (Ping timeout: 252 seconds)
11:35:36 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Quit: Frostillicus)
11:37:23 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:37:47 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:38:02 × orcus quits (~orcus@mail.brprice.uk) (Changing host)
11:38:02 → orcus joins (~orcus@user/brprice)
11:41:48 → fp joins (~Thunderbi@2001:708:150:10::3664)
11:42:20 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:42:36 × img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
11:42:45 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:43:58 → img joins (~img@user/img)
11:44:33 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
11:44:41 → aforemny joins (~aforemny@i59F4C7F8.versanet.de)
11:44:53 × aforemny_ quits (~aforemny@i59F4C598.versanet.de) (Ping timeout: 268 seconds)
11:48:22 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:48:44 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:50:41 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:51:11 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:51:20 × poscat quits (~poscat@user/poscat) (Remote host closed the connection)
11:51:43 × orcus- quits (~orcus@2a03:4000:55:d87::1) (Quit: ZNC 1.8.2 - https://znc.in)
11:52:05 → orcus- joins (~orcus@user/brprice)
11:54:09 × fp quits (~Thunderbi@2001:708:150:10::3664) (Ping timeout: 268 seconds)
11:54:28 → poscat joins (~poscat@user/poscat)
11:56:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
11:56:20 × dispater- quits (~dispater@2a03:4000:55:d87::1) (Quit: ZNC 1.8.2 - https://znc.in)
11:56:25 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
11:56:42 → dispater- joins (~dispater@user/brprice)
11:59:50 × comerijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds)
12:01:16 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
12:02:05 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
12:02:31 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:02:34 → fp joins (~Thunderbi@wireless-86-50-140-9.open.aalto.fi)
12:05:18 → merijn joins (~merijn@77.242.116.146)
12:07:37 × fp quits (~Thunderbi@wireless-86-50-140-9.open.aalto.fi) (Quit: fp)
12:09:15 → fp joins (~Thunderbi@2001:708:20:1406::10c5)
12:09:28 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
12:09:52 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:10:20 × andreas303 quits (andreas303@is.drunk.and.ready-to.party) (Ping timeout: 260 seconds)
12:17:26 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
12:17:52 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:17:52 <hellwolf> | Consider the Pascal statement y := z + 1. Using the convention that y’ denotes the new value of y, we can rewrite this statement as the mathematical formula y’ = z + 1, Many readers will think that the Pascal statement and the formula are equally simple.
12:17:52 <hellwolf> They are wrong. The formula is much simpler than the Pascal statement. Equality is a simple concept that five-year-old children understand. Assignment (:=) is a complicated concept that university students find difficult.
12:18:11 <hellwolf> ^-- I found this statement from a CS paper amusing.
12:20:40 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 252 seconds)
12:21:05 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds)
12:23:19 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
12:23:46 × jespada quits (~jespada@r167-61-127-149.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…)
12:23:47 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:26:08 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
12:29:12 → jespada joins (~jespada@r167-61-127-149.dialup.adsl.anteldata.net.uy)
12:30:20 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
12:30:42 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:33:27 → ttybitnik joins (~ttybitnik@user/wolper)
12:34:42 × aman quits (~aman@user/aman) (Quit: aman)
12:35:03 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
12:35:27 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:41:30 <ski> well, one could draw a distinction between local mutation, and mutation via (possibly aliased) indirections/references/pointers (transitively) to data structures. the former can be modelled via a group of mutually tail-recursive functions (indicating labels for branching & joining, and for loops) (basically SSA, Single Static-Assignment, form)
12:41:43 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
12:42:07 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:42:46 × AlexZenon quits (~alzenon@178.34.162.18) (Quit: ;-)
12:43:01 <ski> latter, and i suppose especially mutating references/pointers, would be harder to try to model in such a nicer way
12:43:57 <ski> (in den. sem., you carry around a store mapping abstract locations to values, where those values could include other locations)
12:44:32 × AlexNoo quits (~AlexNoo@178.34.162.18) (Quit: Leaving)
12:48:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
12:48:24 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:50:25 <tomsmeding> hellwolf: it's definitely amusing, but not so sure about its validity :)
12:51:10 <tomsmeding> (counterpoint: the formula has 3 quantities involved (old y, new y, z), whereas the assignment only has 2 (new y, z))
12:51:17 <hellwolf> it's a well cited paper (3000+ citations)
12:51:31 <tomsmeding> well-cited papers can be wrong
12:51:32 <hellwolf> (not saying that is a proof for it's validity)
12:51:50 <hellwolf> it's amusing that some myth, or mistakes, can spread so far.
12:51:52 <tomsmeding> and also, the paper as a whole can be valid even if this particular claim is dubious :)
12:52:26 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
12:52:50 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:52:59 <tomsmeding> (another counterpoint: in the equation model, you have to keep the equations in mind in order to make sense of new ones. In the assignment model, you have to keep only the variables' values in mind)
12:53:07 <__monty__> It immediately becomes less dubious with the example `y := y + 1`.
12:53:20 <tomsmeding> then they should have taken that example!
12:53:45 <tomsmeding> also, I posit that's primarily because of the notation using '='
12:53:49 <__monty__> Did they not? We don't know what `z` is, maybe it's `z := y + 1`!
12:53:58 <tomsmeding> a 5-year old, or at least a 5-year-old of 10 years ago, has certainly used an eraser before
12:56:44 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
12:57:06 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
12:57:21 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 248 seconds)
13:04:03 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:04:26 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
13:05:28 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
13:07:34 × ubert quits (~Thunderbi@ip5f59455a.dynamic.kabel-deutschland.de) (Quit: ubert)
13:08:06 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:08:28 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
13:12:08 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:12:32 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
13:14:07 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
13:18:48 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:19:10 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 260 seconds)
13:19:10 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
13:21:53 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
13:24:15 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:24:39 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
13:24:57 → AlexNoo joins (~AlexNoo@178.34.162.18)
13:26:59 → AlexZenon joins (~alzenon@178.34.162.18)
13:30:49 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds)
13:32:00 → merijn joins (~merijn@77.242.116.146)
13:32:08 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:32:29 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
13:36:00 → kuribas joins (~user@ptr-17d51em5ayej71s7xap.18120a2.ip6.access.telenet.be)
13:37:50 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds)
13:38:45 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:39:15 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
13:42:05 → ruehrei joins (~ruehrei@2a09:bac2:2a79:1b4b::2b8:77)
13:45:09 → par1tet joins (~par1tet@185.63.216.143)
13:46:08 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:46:16 → ljdarj joins (~Thunderbi@user/ljdarj)
13:46:29 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
13:53:11 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:53:38 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
13:55:49 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 245 seconds)
13:57:27 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
13:57:57 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
14:04:50 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
14:05:11 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
14:08:13 × mange quits (~mange@user/mange) (Quit: Zzz...)
14:09:57 × fp quits (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 248 seconds)
14:10:29 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds)
14:12:00 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
14:12:27 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
14:18:57 × trickard quits (~trickard@cpe-51-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
14:19:11 → trickard joins (~trickard@cpe-51-98-47-163.wireline.com.au)
14:20:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
14:20:28 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
14:22:46 → fp joins (~Thunderbi@130.233.53.37)
14:26:22 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
14:26:45 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
14:27:25 × fp quits (~Thunderbi@130.233.53.37) (Client Quit)
14:27:35 → fp1 joins (~Thunderbi@130.233.53.37)
14:31:36 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
14:32:00 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
14:32:07 × fp1 quits (~Thunderbi@130.233.53.37) (Ping timeout: 252 seconds)
14:34:06 × dyniec quits (~dyniec@dybiec.info) (Remote host closed the connection)
14:34:45 → dyniec joins (~dyniec@dybiec.info)
14:36:05 → Lycurgus joins (~juan@user/Lycurgus)
14:37:03 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
14:37:25 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
14:38:48 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
14:40:04 × cptaffe quits (~cptaffe@user/cptaffe) (Ping timeout: 260 seconds)
14:42:07 → fp joins (~Thunderbi@wireless-86-50-140-9.open.aalto.fi)
14:42:27 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
14:42:52 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
14:43:04 × dyniec quits (~dyniec@dybiec.info) (Remote host closed the connection)
14:43:46 → dyniec joins (~dyniec@dybiec.info)
14:44:26 × ttybitnik quits (~ttybitnik@user/wolper) (Remote host closed the connection)
14:49:08 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
14:49:32 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
14:55:08 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
14:55:31 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:00:18 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:00:39 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:01:49 × fp quits (~Thunderbi@wireless-86-50-140-9.open.aalto.fi) (Ping timeout: 276 seconds)
15:05:02 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:05:26 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:07:39 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
15:08:37 × distopico quits (~cerdolibr@2001:4b98:dc2:41:216:3eff:fe6c:52a1) (Ping timeout: 248 seconds)
15:11:19 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:11:44 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:16:43 <hellwolf> ¬ ∀ ¬ <-- what is the closest you can get from Haskell to this?
15:16:46 → distopico joins (~cerdolibr@xvm-111-150.dc2.ghst.net)
15:18:13 → cptaffe joins (~cptaffe@user/cptaffe)
15:19:45 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:20:11 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:25:31 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:25:54 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:32:07 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:32:29 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:33:05 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2)
15:35:10 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
15:36:05 ← takotaco parts (matsu@user/takotaco) ()
15:37:23 → ubert joins (~Thunderbi@2a02:8109:abb3:7000:7d87:de41:2d11:5165)
15:37:26 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:37:27 → ljdarj joins (~Thunderbi@user/ljdarj)
15:37:48 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:40:22 × iNomad quits (~iNomad@user/iNomad) (Quit: leaving)
15:41:12 × ubert quits (~Thunderbi@2a02:8109:abb3:7000:7d87:de41:2d11:5165) (Client Quit)
15:42:02 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:42:30 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:45:59 → srk- joins (~sorki@user/srk)
15:46:29 × srk quits (~sorki@user/srk) (Ping timeout: 248 seconds)
15:46:57 × jespada quits (~jespada@r167-61-127-149.dialup.adsl.anteldata.net.uy) (Ping timeout: 248 seconds)
15:47:34 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:48:02 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:48:54 srk- is now known as srk
15:49:51 × Lycurgus quits (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org))
15:50:34 → jespada joins (~jespada@r167-61-127-149.dialup.adsl.anteldata.net.uy)
15:51:33 <ski> (forall a. f a -> o) -> o -- ?
15:51:58 <ski> (forall a. f a -> m Void) -> m Void -- ?
15:53:00 <ski> p (forall a. p (f a) Void) Void -- ?
15:54:11 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
15:54:37 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
15:56:19 × par1tet quits (~par1tet@185.63.216.143) (Quit: Client closed)
15:57:31 → fp joins (~Thunderbi@hof1.kyla.fi)
15:58:30 × ruehrei quits (~ruehrei@2a09:bac2:2a79:1b4b::2b8:77) (Ping timeout: 240 seconds)
15:59:38 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
15:59:59 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:03:08 × bramh quits (~bramh@user/bramh) (Quit: Ping timeout (120 seconds))
16:03:45 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
16:04:08 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:04:29 → bramh joins (~bramh@user/bramh)
16:05:11 × orcus- quits (~orcus@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
16:05:11 × dispater- quits (~dispater@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
16:07:10 → dispater- joins (~dispater@user/brprice)
16:07:40 → orcus- joins (~orcus@user/brprice)
16:09:44 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
16:10:06 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:14:31 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
16:14:56 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:17:02 × dispater- quits (~dispater@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
16:17:02 × orcus- quits (~orcus@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
16:17:41 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
16:18:06 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:18:49 → dispater- joins (~dispater@user/brprice)
16:19:19 → orcus- joins (~orcus@user/brprice)
16:19:33 × sawilagar quits (~sawilagar@user/sawilagar) (Read error: Connection reset by peer)
16:19:55 → ttybitnik joins (~ttybitnik@user/wolper)
16:22:42 → comerijn joins (~merijn@77.242.116.146)
16:24:18 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
16:24:42 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:24:59 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 245 seconds)
16:26:23 → harveypwca joins (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c)
16:27:37 × comerijn quits (~merijn@77.242.116.146) (Ping timeout: 276 seconds)
16:27:43 <dolio> tomsmeding: Is your objection that equality is not really understood by 5 year olds?
16:27:51 <dolio> Not that assignment is simple?
16:31:29 → miguelnegrao joins (~miguelneg@2001:818:dc71:d100:97a9:f15a:6ac:fc9e)
16:31:30 × jrm quits (~jrm@user/jrm) (Quit: ciao)
16:31:46 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
16:32:02 <hellwolf> I have more outrageous statement from the same paper: "advocates of so-called functional programming languages often claim that they just use ordinary mathematical functions, but try explaining to a twelve-year-old how evaluating a mathematical function can display a character on her computer screen"
16:32:08 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:32:29 <hellwolf> -- The temporal logic of actions, Leslie Lamport.
16:32:44 <hellwolf> 1994
16:32:54 → jrm joins (~jrm@user/jrm)
16:34:24 <hellwolf> ski: somehow that (not forall not) equivalent to ∃. So, by extension, Haskell's idiom of existential type is a way to encode that? I don't know, just guessing.
16:34:50 <dolio> It's not equivalent except in classical logic.
16:36:23 <__monty__> TLA+ is interesting. I don't think the mathematical function is really the hard part of that though.
16:36:28 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
16:36:58 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:37:07 <miguelnegrao> Hi all, I'm completely stuck with something from Data.Type.Equality .  How can I define use p = gcastWith p Refl ? If I use gcastWith p Refl it works fine to for instance to prove (a + 1 ) :~: (b+1) from (a :~: b) but I can't seem to define it with a function. use p = gcastWith p Refl does not work without a type signature, and I can't figure one
16:37:07 <miguelnegrao> out.
16:38:13 × olivial quits (~benjaminl@user/benjaminl) (Read error: Connection reset by peer)
16:38:28 → olivial joins (~benjaminl@user/benjaminl)
16:38:47 <miguelnegrao> chatgpt O3 can't figure this one out either :-)
16:40:30 <miguelnegrao> use :: forall f a b. (a :~: b) -> f a :~: f b doesn't quite do it, then GHC doesn't know what the "f" should be
16:41:50 × jrm quits (~jrm@user/jrm) (Quit: ciao)
16:41:59 × fp quits (~Thunderbi@hof1.kyla.fi) (Ping timeout: 244 seconds)
16:42:17 <dolio> You want to define `p = gcastWith p Refl`? That seems like it will just loop.
16:43:05 <miguelnegrao> no: use p = gcastWith p Refl
16:43:15 → jrm joins (~jrm@user/jrm)
16:43:20 <dolio> Oh.
16:43:25 <miguelnegrao> define a function named "use". I belive it is also called "cong" ?
16:43:36 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
16:43:48 <dolio> I see.
16:43:59 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:44:28 <miguelnegrao> The reason for the name is like "GHC please use this theorem and in this bigger expression"
16:44:33 → sawilagar joins (~sawilagar@user/sawilagar)
16:44:49 × jrm quits (~jrm@user/jrm) (Client Quit)
16:45:46 <miguelnegrao> If I type the expression by inplace "gcastWith p Refl" for some p that I have around, then it will work, GHC goes and works its magic.
16:46:11 → jrm joins (~jrm@user/jrm)
16:46:12 <Leary> That's what `gcastWith` itself is already doing.
16:46:14 <dolio> Well, cong normally has a type that would be like `a :~: b -> f a :~: f b`. However, if you're expecting to use it with `_ + 1`, it seems unlikely that you will be able to get `f` to be that.
16:46:24 <Leary> You're just specialising `r` in the signature of `gcastWith` to `c :~: d`?
16:46:55 <miguelnegrao> Example:  theoremAddZero :: forall n . SNat n -> n + Zero :~: n
16:47:06 <miguelnegrao> theoremAddZero (SSucc n) = gcastWith (theoremAddZero n) Refl
16:47:21 <tomsmeding> miguelnegrao: do you have the typing plugins?
16:47:29 <miguelnegrao> No, its all vanilla GHC
16:47:41 <miguelnegrao> using just singletons package
16:47:42 <tomsmeding> then that theoremAddZero will not work
16:47:49 <miguelnegrao> works fine
16:48:06 <tomsmeding> oh, yes, my mistake
16:48:13 <dolio> The reason that the expression works is that `r` gets instantiated to `a + 1 :~: b + 1` or something, but factoring out that `(+1)` as an `f` is dubious.
16:48:13 <miguelnegrao> $(singletons [d|
16:48:13 <miguelnegrao>     data Nat = Zero | Succ Nat
16:48:14 <miguelnegrao>     |])
16:49:17 <tomsmeding> not only dubious: it's impossible, since `f ~ (+1)` would mean that (+) here is a partially-applied type family, which GHC does not allow
16:49:20 <miguelnegrao> btw, the other case is the theorem is trivial theoremAddZero SZero = Refl
16:49:30 <dolio> Right.
16:50:00 <miguelnegrao> basically I wanted to write these proofs like:
16:50:00 <miguelnegrao> theoremAddZero (SSucc n) = use (theoremAddZero n)
16:50:04 <miguelnegrao> it would be pretier
16:50:41 <tomsmeding> well, perhaps it would, but I'm fairly sure it's impossible to give `use` a type that makes that work
16:51:02 <miguelnegrao> ok, that is good to know. I just felt a bit stupid writting it over and over :-)
16:51:14 <miguelnegrao> glad to know the problem is not on my side
16:51:27 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
16:51:50 <tomsmeding> there are other languages that do allow partial application of "type families"; in particular, Agda and Idris
16:51:50 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:52:24 <tomsmeding> but that's a whole different territory :)
16:52:42 <miguelnegrao> Another thing I have a feeling I cannot do is compile a list of proofs and tell GHC to use all those proofs to prove something else.
16:53:06 <tomsmeding> data Dict c where Dict :: c => Dict c
16:53:06 <miguelnegrao> I have to write it like: gcastWith p1 $ gcastWith p2 $ gcastWith p3 $ Refl
16:53:12 × omegatron quits (~some@user/omegatron) (Quit: Power is a curious thing. It can be contained, hidden, locked away, and yet it always breaks free.)
16:53:23 <tomsmeding> then use `Dict @(a :~: b, c :~: d, e :~: f)`
16:53:27 <miguelnegrao> I did rename gcastWith to "have" so it looks a bit better
16:53:40 <tomsmeding> to bundle up a bunch of proofs
16:53:48 <tomsmeding> but it's not generic like passing a list of proofs, no
16:53:49 <miguelnegrao> interesting
16:54:41 <tomsmeding> but that may help only if you have the same set of "lemmas" in a bunch of places
16:54:44 <miguelnegrao> Thanks tomsmeding for that tip, I will investigate
16:55:20 <miguelnegrao> No, usually I just build a group of substeps in the proof which I then use in a more complicated expression part of the same proof
16:55:42 <tomsmeding> is the goal of this just to play around with singletons in haskell?
16:55:53 → internatetional joins (~nate@2001:448a:20a3:c2e5:5e5:e8fb:73b6:1daa)
16:55:59 <tomsmeding> because if the goal is to formalise some mathematics, haskell is _not_ the suitable language :p
16:56:15 <miguelnegrao> Essentially yes, it is just for fun
16:56:23 <tomsmeding> then have at it :)
16:56:29 <miguelnegrao> But I have been porting mathlib, the Nats part
16:56:52 <miguelnegrao> stuff like theoremAddMulDivLeft :: forall x y z . SNat x -> SNat y -> SNat z -> N0 < y -> (x + (y * z)) / y :~: (x / y) + z
16:57:01 <dolio> Translating mathlib to Haskell is going to be very painful, I expect.
16:57:07 <miguelnegrao> YES !
16:57:22 <miguelnegrao> comutativity and associativity is very painful
16:57:47 <miguelnegrao> but it puts me in a zen state I guess
16:57:54 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
16:58:17 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
16:59:31 <EvanR> associativity was a mistake, lisp was right, just use gratuitous amount of parentheses
16:59:53 <miguelnegrao> In proofs you have to move every single parenthesis manually...
17:00:14 <miguelnegrao> (a + b) + c is not equial to a + (b + c) unless you use a proof of that...
17:00:49 <Leary> miguelnegrao: Suggestion: declare `pattern QED = Refl; (==>) = gcastWith; infixr 1 ==>` and write `p1 ==> p2 ==> p3 ==> QED`.
17:01:07 × internatetional quits (~nate@2001:448a:20a3:c2e5:5e5:e8fb:73b6:1daa) (Remote host closed the connection)
17:01:19 <miguelnegrao> oh, I like that !
17:01:25 → internatetional joins (~nate@2001:448a:20a3:c2e5:5e5:e8fb:73b6:1daa)
17:02:18 × internatetional quits (~nate@2001:448a:20a3:c2e5:5e5:e8fb:73b6:1daa) (Client Quit)
17:03:29 × miguelnegrao quits (~miguelneg@2001:818:dc71:d100:97a9:f15a:6ac:fc9e) (Quit: Client closed)
17:03:40 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
17:04:06 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:04:43 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
17:06:19 <ski> hellwolf : i didn't bring up existentials. however, in logic, you often define `Not a = a -> Void' (`Void' being the false proposition (the nullary disjunction), having no proof, but having an elimination rule, with zero branches, in Haskell terms effectively `void :: Void -> a; void v = case v of {}'). however, if you don't use the elimination, you can replace `Void' with an arbitrary proposition `o'
17:06:25 <ski> (giving you "minimal logic", rather than "intuitionistic logic"), so instead of `Not (...)' you'd have `... -> o'
17:08:07 × orcus- quits (~orcus@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
17:08:08 × dispater- quits (~dispater@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
17:08:31 <__monty__> And that's because o *could* be Void?
17:09:51 → dispater- joins (~dispater@user/brprice)
17:10:22 → orcus- joins (~orcus@user/brprice)
17:10:55 <EvanR> because parametricity stops you from ever producing an o, Void or not
17:11:20 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
17:11:41 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:11:53 <EvanR> unless one of the hypotheses lets you, which in fact could let you produce a Void, hypothetically
17:13:26 <ski> the second two versions were replacing the function arrow `(->)' with a kleisli arrow `Kleisli m' (where `Kleisli m a b = a -> m b', and `m' is a monad) (although, categorically speaking, one should distinguish between a morphism/arrow `f : A >---> B' in a category (between two objects `A' and `B'), and an "internalization" of that as an object itself, commonly written as `B^A' (or perhaps `A -> B' or `A =>
17:13:32 <ski> B') (e.g. currying being expressed as (for each object `A') collection of arrows `Gamma * A >---> B' being ("naturally", in objects `Gamma' and `B') equivalent to `Gamma >---> (A -> B)'))
17:13:42 <EvanR> (a -> o) -> a -> o
17:14:23 <EvanR> not (not a and a)
17:16:09 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
17:16:34 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:19:32 <ski> anyway, i used `M Void' for some particular monad `M', to express that a particular computation didn't terminate normally (.. more specifically, i was doing something like (cooperative) concurrency, and i wanted to express that a spawned thread eventually called `killThread :: M Void' at the end (or went on infinitely, or was partial) .. originally i used `()' instead of `Void', which resulted in a
17:19:38 <ski> sprinkling of `undefined's throughout the code, leaving me unsure whether i'd gotten it correct. swapping to the more conceptually correct `Void' allowed me to gain more confidence of the correctness, removing all the `undefined's)
17:20:09 <ski> @djinn-add type NotNot a = Not (Not a)
17:20:22 <ski> @djinn NotNot (Either a (Not a))
17:20:22 <lambdabot> f a = void (a (Right (\ b -> a (Left b))))
17:22:05 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
17:22:09 <ski> btw, Djinn is a bit overeager here, that `void' can be removed (replaced by `id') (it's using the instance `void @Void :: Void -> Void' of `void :: forall o. Void -> o')
17:22:30 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:24:44 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
17:24:48 <ski> (and because this doesn't need to use `void', it can be proved in minimal logic, with an arbitrary proposition `o' replacing `Void', so that `NotNot (Either a (Not a))' becomes `(Either a (a -> o) -> o) -> o')
17:24:54 <ski> @type let f a = a (Right (\ b -> a (Left b))) in f
17:24:55 <lambdabot> (Either a (a -> t) -> t) -> t
17:26:03 <ski> for comparision
17:26:06 <ski> @type let f a = absurd (a (Right (\ b -> a (Left b)))) in f
17:26:07 <lambdabot> (Either a1 (a1 -> Void) -> Void) -> a2
17:27:42 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
17:28:06 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:28:35 <ski> (note that, for some silly reason, `void :: Functor f => f a -> f ()' is a library operation, name coming from FFI, so the corresponding operation we want to use from `Data.Void' was named `absurd' ..)
17:28:45 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
17:29:00 → raym joins (~ray@user/raym)
17:29:23 × sawilagar quits (~sawilagar@user/sawilagar) (Read error: Connection reset by peer)
17:29:31 <EvanR> so in your example of an action which doesn't return normally would you use o instead of Void
17:29:33 <ski> __monty__ : yea, that's one way to think about it
17:30:58 <ski> well, that could be used for `killThread :: M o', but for the spawn case, you'd need `spawnThread :: (forall o. M o) -> M ()' to replace `spawnThread :: M Void -> M ()'
17:31:30 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Read error: Connection reset by peer)
17:33:23 <ski> (iirc, i was also pondering an operation `forkThread :: M Void -> M Void -> M Void' as well (forget whether i also provided that) .. which would then become `forkThread :: (forall o. M o) -> (forall p. M p) -> M q')
17:34:56 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
17:35:22 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:36:06 <ski> anyway, the rank-2 would perhaps feel a bit overkill. but i suppose one could replace `Void' in positive/covariant/output/producer position with `o', but not do any replacement in negative/contravariant/input/consumer position, so `forkThread :: M Void -> M Void -> M o'
17:37:48 <ski> @type (<*)
17:37:49 <lambdabot> Applicative f => f a -> f b -> f a
17:38:13 <ski> note how that uses `b' instead of `()', this is a similar thing
17:38:35 <monochrom> @type forever
17:38:36 <lambdabot> Applicative f => f a -> f b
17:39:42 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
17:40:03 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:40:30 <EvanR> forkThread :: M a -> M b -> M o ?
17:42:42 <ski> replacing `()' in input position with an arbitrary result (conceptually throwing away the result, replacing it with the empty tuple .. `()' (hand-waving) would correspond to terminal object, there's a unique arrow `const () : A >---> 1' for any object `A') .. while, i suppose, in output position, you'd want to use `exists r. ..r..' (note that for input position, `(exists r. ..r..) -> ...' is equivalent to
17:42:49 <ski> `forall r. (..r.. -> ...)', as in `forever :: Applicative f => (exists a. f a) -> f b')
17:42:53 → wootehfoot joins (~wootehfoo@user/wootehfoot)
17:43:18 → tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
17:43:20 → shaeto joins (~Shaeto@94.25.234.79)
17:43:49 <ski> so, yea, we "morally" have `forever :: Applicative f => f () -> f Void' (turn a (hopefully) terminating chunk of a computation into a non-terminating loop repeating that chunk)
17:44:53 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
17:44:58 <EvanR> with laziness wouldn't f a -> f b possibly make sense even if the action "doesn't terminate"
17:45:09 <ski> EvanR : that would correspond to `forkThread :: M () -> M () -> M Void', which isn't what i wanted to express. i wanted both branches to end in `killThread'
17:45:29 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
17:45:47 <EvanR> it doesn't because a or b could be Void
17:45:52 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:45:58 <EvanR> it doesn't guarantee a result
17:46:12 <EvanR> like () "does"
17:47:05 <ski> basically, i had a `runM :: M Void -> IO ()', providing a "full program" (calling `killThread' at the end). and then you can issue `forkThread's while you keep on that "program spine". but in (non-tail) sub-computations, you could only introduce more threads by using `spawnThread' instead, which attaches a "full program" to a (normally terminating" "chunk"
17:47:20 <monochrom> f a -> f b still makes sense if the action non-terminates, or even if you set a=Void.
17:47:53 <ski> yep, but it doesn't require the `f a' to call `killThread' (or go into an infinite loop, or be partial)
17:48:20 → target_i joins (~target_i@user/target-i/x-6023099)
17:48:51 <EvanR> ok Void guarantees no result
17:49:04 <monochrom> Yeah forever is different from forkThread.
17:49:12 <EvanR> no results allowed
17:49:40 <EvanR> a type variable only guarantees you can't use the result if it exists
17:49:43 <monochrom> It is just not everyday that one wants a function that says "the input must be a non-terminating program!".
17:50:15 <EvanR> or is it
17:50:33 <EvanR> in game dev community "never let the game crash ever"
17:50:39 <ski> i maintained a scheduler queue of tasks
17:50:57 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
17:51:18 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:51:30 <monochrom> For games and OSes, you use forever. Only the outermost layer needs to be run forever.
17:51:47 <ski> `killThread' merely removed the currently executing task, switching to the next available one (or ending `runM', if empty queue now)
17:53:01 <EvanR> I guess most games, not on nintendo switch, come with a "quit to windows" (or DOS or whatever) menu option
17:53:18 <EvanR> which would cause the program to terminate
17:53:35 <EvanR> so input must be non terminating program is useful for nintendo switch games
17:53:45 <ski> and the continuation of `M Void' accepting a `Void' meant that it's effectively dead code, unreachable (ignoring bottoms, yes), so we can throw it away, without getting any surprises in the surface of the API
17:55:29 <monochrom> Oh, you just want to say "there is no continuation".
17:56:32 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
17:56:43 <ski> right
17:56:57 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
17:58:34 → jmcantrell joins (~weechat@user/jmcantrell)
18:00:40 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
18:02:19 <ski> dialogue I/O used `type Dialogue = [Response] -> [Request]' as it's "final answer" type of "full I/O programs" (seeming to correspond to `Void', or perhaps more `M Void' ?). instead of ending your `main :: Dialogue' with `end :: Dialogue; end _ = []', you'd pass a continuation (or several, in some cases), with `getChar :: (Char -> Dialogue) -> Dialogue' (iow `getChar :: Cont Dialogue Char') and `putChar ::
18:02:25 <ski> Char -> Dialogue -> Dialogue' (iow `putChar :: Char -> Cont Dialogue ()') as representative examples)
18:03:46 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
18:04:13 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:04:22 <ski> so typically instead of hard-wiring `end' at the end of every branch of your `main :: Dialogue', you could do `main = myMain end' where `myMain :: Dialogue -> Dialogue' (iow `myMain :: Cont Dialogue ()'), making more (normally terminating) operations easily composable
18:07:24 <ski> ("Modern Compiler Implementation in {ML,Java,C}" by Andrew W. Appel in 1998 at <https://www.cs.princeton.edu/~appel/modern/> also happens to use an `end : Answer' operation for a purely functional mini-language, including I/O operations, just treating `Answer' as abstract, as opposed to `Dialogue' above)
18:08:30 <ski> (oh, and it's a strict language, so the "backwards" request-response model wouldn't work like in early Haskell)
18:10:02 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
18:10:24 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:13:05 → euphores joins (~SASL_euph@user/euphores)
18:14:12 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
18:14:37 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:14:52 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
18:16:00 → machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
18:20:29 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
18:20:53 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:25:12 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 252 seconds)
18:26:42 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
18:26:42 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
18:27:05 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:27:47 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
18:29:14 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
18:32:06 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
18:32:10 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
18:32:30 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
18:32:30 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:33:03 → Everything joins (~Everythin@77.120.244.38)
18:38:24 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
18:38:48 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:39:52 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 252 seconds)
18:40:39 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
18:41:02 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:44:13 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
18:44:38 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:45:07 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
18:48:13 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
18:49:33 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
18:49:45 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
18:49:54 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
18:50:08 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
18:50:38 × jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 244 seconds)
18:53:07 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
18:55:02 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
18:55:28 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:00:00 × caconym7 quits (~caconym@user/caconym) (Quit: bye)
19:00:31 × califax quits (~califax@user/califx) (Remote host closed the connection)
19:00:39 → caconym7 joins (~caconym@user/caconym)
19:00:47 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:00:54 → ljdarj1 joins (~Thunderbi@user/ljdarj)
19:00:55 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:00:58 → califax joins (~califax@user/califx)
19:01:10 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:02:55 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:03:19 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:05:09 → Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
19:05:13 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
19:05:13 ljdarj1 is now known as ljdarj
19:05:37 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
19:05:53 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
19:06:22 → sprotte24 joins (~sprotte24@p200300d16f1d160071ddcdfe558a8c3b.dip0.t-ipconnect.de)
19:06:47 × Yumemi quits (~Yumemi@chamoin.net) (Quit: .)
19:07:09 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
19:07:42 → Yumemi joins (~Yumemi@chamoin.net)
19:08:10 × jespada quits (~jespada@r167-61-127-149.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…)
19:10:14 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:10:16 → jespada joins (~jespada@r167-61-127-149.dialup.adsl.anteldata.net.uy)
19:10:36 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:16:32 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:16:56 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:17:23 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:19:58 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:20:24 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:23:07 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
19:25:02 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:25:28 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:28:44 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
19:31:26 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:31:48 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:34:34 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:37:00 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:37:22 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:39:16 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
19:40:29 × shaeto quits (~Shaeto@94.25.234.79) (Quit: WeeChat 4.1.1)
19:42:35 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:42:59 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:47:04 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
19:47:39 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:48:00 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:48:26 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 252 seconds)
19:49:55 → sshine joins (~simon@dao.mechanicus.xyz)
19:50:20 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:51:04 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:51:27 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:51:50 <sshine> there was a property test framework featured in Haskell Weekly recently. I can't find it, but it did something to improve on hedgehog. can anyone guess what package I'm looking for? it's not quickcheck-lockstep.
19:53:01 → sawilagar joins (~sawilagar@user/sawilagar)
19:55:29 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
19:56:20 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
19:56:43 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
19:56:59 → tromp joins (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b)
19:59:33 → Unhammer joins (~Unhammer@user/unhammer)
20:01:48 <Unhammer> Hi, after upgrading a thing from 9.2.8 to 9.6.7, on windows I'm seeing `[FreeTDS][SQL Server]Invalid "CP1252;LC_MONETARY=C;LC_NUMERIC=C;LC_TIME=C" character set specified` when opening a database connection. I'm not explicitly setting anything to CP1252 in my code (but I do Encoding.setLocaleEncoding Encoding.utf8 at the start of main). Did something change somewhere in how ghc sets locale strings?
20:02:28 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:02:51 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:03:19 × Everything quits (~Everythin@77.120.244.38) (Quit: leaving)
20:05:55 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:07:12 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:07:36 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:07:44 → Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
20:09:10 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:09:34 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:10:56 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
20:14:18 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:14:40 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:20:01 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:20:25 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:21:44 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:22:51 × kuribas quits (~user@ptr-17d51em5ayej71s7xap.18120a2.ip6.access.telenet.be) (Remote host closed the connection)
20:23:16 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:23:39 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:25:30 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:25:56 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:27:08 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
20:33:19 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:33:43 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:37:31 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:39:59 → machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
20:41:03 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:41:26 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:41:33 <tomsmeding> sshine: falsify?
20:41:42 → econo_ joins (uid147250@id-147250.tinside.irccloud.com)
20:42:20 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
20:44:20 × target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
20:45:12 → fp joins (~Thunderbi@hof1.kyla.fi)
20:45:12 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
20:47:25 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:47:49 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:49:00 × jespada quits (~jespada@r167-61-127-149.dialup.adsl.anteldata.net.uy) (Ping timeout: 276 seconds)
20:51:21 → jespada joins (~jespada@r186-48-61-216.dialup.adsl.anteldata.net.uy)
20:53:18 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:53:21 × jespada quits (~jespada@r186-48-61-216.dialup.adsl.anteldata.net.uy) (Client Quit)
20:53:51 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
20:54:12 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
20:58:39 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
20:59:55 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:00:19 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:01:13 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 265 seconds)
21:01:32 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
21:01:44 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
21:02:13 → j1n37 joins (~j1n37@user/j1n37)
21:06:34 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:06:57 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:07:20 → Lycurgus joins (~juan@user/Lycurgus)
21:09:06 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:10:30 <Unhammer> … it seems like I can append `;ClientCharset=CP1252` to my connstring to override whatever is going on there. Seems like some locale-related env-vars are being set differently in newer ghc, but I really don't understand why or where that would happen.
21:13:42 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:14:06 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:14:24 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
21:14:58 × fp quits (~Thunderbi@hof1.kyla.fi) (Ping timeout: 252 seconds)
21:19:10 × tromp quits (~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
21:20:31 → jmcantrell joins (~weechat@user/jmcantrell)
21:20:32 × haskellbridge quits (~hackager@syn-096-028-224-255.res.spectrum.com) (Read error: Connection reset by peer)
21:20:40 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:21:04 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:21:59 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
21:24:53 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:25:37 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:25:59 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:26:02 → haskellbridge joins (~hackager@syn-096-028-224-255.res.spectrum.com)
21:26:02 ChanServ sets mode +v haskellbridge
21:26:20 <haskellbridge> <geekosaur> test 2
21:26:55 × haskellbridge quits (~hackager@syn-096-028-224-255.res.spectrum.com) (Remote host closed the connection)
21:27:13 <geekosaur> stuff seems to have not liked my rewiring my network. bouncing the bridge
21:27:45 → haskellbridge joins (~hackager@syn-096-028-224-255.res.spectrum.com)
21:27:45 ChanServ sets mode +v haskellbridge
21:27:50 <haskellbridge> <geekosaur> yeh, that seems to look a bit better
21:29:39 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:30:02 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:30:13 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
21:30:54 <Rembane> \o/
21:32:10 → haritz joins (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8)
21:32:11 × haritz quits (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host)
21:32:11 → haritz joins (~hrtz@user/haritz)
21:33:34 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
21:34:07 <EvanR> bouncing bridge: Tacoma Narrows Bridge (1940)
21:36:00 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:36:23 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:37:36 <monochrom> yikes haha
21:37:59 <monochrom> There was a newer one that bounced when people walked. >:)
21:39:58 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:40:24 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:40:40 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:44:54 × sprotte24 quits (~sprotte24@p200300d16f1d160071ddcdfe558a8c3b.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
21:45:02 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
21:46:51 → ridcully_ joins (~ridcully@p57b52c91.dip0.t-ipconnect.de)
21:47:15 × ridcully quits (~ridcully@pd951f029.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
21:47:56 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:48:21 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:49:14 × dhil quits (~dhil@5.151.29.140) (Ping timeout: 268 seconds)
21:52:54 × jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 260 seconds)
21:55:03 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
21:55:29 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
21:56:04 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:03:01 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
22:03:53 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
22:04:18 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:05:39 × Lycurgus quits (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org))
22:07:57 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
22:08:22 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:09:10 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
22:10:31 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
22:12:59 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
22:13:15 → j1n37 joins (~j1n37@user/j1n37)
22:13:23 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:13:25 × dispater- quits (~dispater@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
22:13:25 × orcus- quits (~orcus@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
22:14:06 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:15:10 → dispater- joins (~dispater@user/brprice)
22:15:41 → orcus- joins (~orcus@user/brprice)
22:18:05 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
22:18:39 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
22:19:01 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:19:09 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
22:21:01 → pavonia joins (~user@user/siracusa)
22:22:25 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
22:24:14 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
22:24:34 × orcus quits (~orcus@user/brprice) (Ping timeout: 252 seconds)
22:24:34 × dispater quits (~dispater@mail.brprice.uk) (Ping timeout: 252 seconds)
22:24:39 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:26:57 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
22:27:24 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:29:56 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:31:33 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
22:31:53 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:35:00 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
22:36:50 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
22:37:11 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:39:27 → emmanuelux joins (~emmanuelu@user/emmanuelux)
22:42:48 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
22:43:09 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:45:39 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:47:44 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
22:50:39 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
22:50:40 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
22:51:00 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
22:54:27 × Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 276 seconds)
22:56:13 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
22:56:37 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:00:54 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
23:01:28 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:02:37 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
23:03:00 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:06:24 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
23:08:51 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
23:09:13 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:10:37 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds)
23:13:56 → machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
23:14:50 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
23:15:14 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:17:14 × xff0x quits (~xff0x@2405:6580:b080:900:effa:612a:1339:418c) (Quit: xff0x)
23:17:16 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:22:04 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
23:22:12 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
23:22:27 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:26:59 → humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
23:27:24 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
23:27:36 → Sgeo joins (~Sgeo@user/sgeo)
23:27:51 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:30:27 → weary-traveler joins (~user@user/user363627)
23:32:26 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
23:32:50 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:32:50 → xff0x joins (~xff0x@ai083248.d.east.v6connect.net)
23:33:04 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:37:29 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
23:37:35 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
23:37:35 × Digit quits (~user@user/digit) (Ping timeout: 252 seconds)
23:40:29 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
23:40:58 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:46:56 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
23:47:19 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:48:37 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:51:09 × acidjnk quits (~acidjnk@p200300d6e71c4f46a4d9c5906f327091.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
23:54:15 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
23:55:48 × sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
23:56:13 → sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
23:59:09 <EvanR> haskell type system could be construed as constructive: you start with nothing and can do nothing until you define new types, then you can create values according to the rules made so far, and that's it, until you define more types. In elixir's upcoming type system and typescript it's destructive. You start with a universe of possible values and the types divide the universe up into smaller and smaller subsets
23:59:48 <EvanR> in some blog somewhere they argue that the first way gives you more stuff and goes farther, though the second way would be nice to have

All times are in UTC on 2025-06-02.