Newest at the top
| 2025-01-15 18:38:40 +0100 | aku | (aku@65.108.245.241) eagleflo |
| 2025-01-15 18:38:09 +0100 | Tetard | (~Tetard@94.187.134.188) |
| 2025-01-15 18:34:52 +0100 | Igloo | (~ian@81.2.99.210) Igfoo |
| 2025-01-15 18:33:17 +0100 | Guest78 | (~Guest78@37.228.251.150) |
| 2025-01-15 18:26:17 +0100 | sprotte24 | (~sprotte24@p200300d16f35c200f4f310a9fb58ced0.dip0.t-ipconnect.de) |
| 2025-01-15 18:25:59 +0100 | euleritian | (~euleritia@dynamic-176-006-134-015.176.6.pool.telefonica.de) |
| 2025-01-15 18:25:40 +0100 | euleritian | (~euleritia@77.23.250.232) (Ping timeout: 260 seconds) |
| 2025-01-15 18:20:53 +0100 | euleritian | (~euleritia@77.23.250.232) |
| 2025-01-15 18:20:48 +0100 | euleritian | (~euleritia@dynamic-176-006-134-015.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-15 18:20:48 +0100 | aku | (aku@65.108.245.241) (Remote host closed the connection) |
| 2025-01-15 18:19:12 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 2025-01-15 18:15:20 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:2087:967c:17ca:ee1d) (Quit: ubert) |
| 2025-01-15 18:10:40 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2025-01-15 18:10:40 +0100 | lbseale | (~quassel@user/ep1ctetus) ep1ctetus |
| 2025-01-15 18:08:10 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2025-01-15 18:08:01 +0100 | euleritian | (~euleritia@dynamic-176-006-134-015.176.6.pool.telefonica.de) |
| 2025-01-15 18:07:59 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-01-15 18:01:27 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f02edd754543fe6660f.dip0.t-ipconnect.de) acidjnk |
| 2025-01-15 17:53:01 +0100 | akegalj | (~akegalj@142-231.dsl.iskon.hr) (Ping timeout: 252 seconds) |
| 2025-01-15 17:52:01 +0100 | ian_ | (~ian@81.2.99.210) (Quit: BIAB) |
| 2025-01-15 17:52:00 +0100 | kenran | (~void@user/kenran) (Remote host closed the connection) |
| 2025-01-15 17:48:48 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-15 17:47:24 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2025-01-15 17:46:59 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-15 17:46:06 +0100 | euleritian | (~euleritia@77.23.250.232) (Read error: Connection reset by peer) |
| 2025-01-15 17:43:57 +0100 | alp | (~alp@2001:861:8ca0:4940:1e61:879a:b0ec:434f) |
| 2025-01-15 17:39:22 +0100 | YoungFrog | (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) youngfrog |
| 2025-01-15 17:39:01 +0100 | YoungFrog | (~youngfrog@2a02:a03f:c9db:fc00:cec4:708e:faa4:70c5) (Quit: ZNC 1.7.x-git-3-96481995 - https://znc.in) |
| 2025-01-15 17:36:36 +0100 | euleritian | (~euleritia@77.23.250.232) |
| 2025-01-15 17:36:18 +0100 | euleritian | (~euleritia@dynamic-176-006-134-015.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-15 17:35:10 +0100 | sprotte24 | (~sprotte24@p200300d16f35c200f4f310a9fb58ced0.dip0.t-ipconnect.de) (Client Quit) |
| 2025-01-15 17:35:10 +0100 | sprotte24 | (~sprotte24@p200300d16f35c200f4f310a9fb58ced0.dip0.t-ipconnect.de) |
| 2025-01-15 17:16:27 +0100 | ft | (~ft@p4fc2a354.dip0.t-ipconnect.de) ft |
| 2025-01-15 17:10:29 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f02edd754543fe6660f.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-01-15 17:08:09 +0100 | <pounce> | (inhabitants because without K there isn't necessarily _one_) |
| 2025-01-15 17:07:23 +0100 | <tomsmeding> | in haskell the proof could be `undefined` |
| 2025-01-15 17:07:19 +0100 | <pounce> | the only inhabitants of a = a are generated by refl. there's no bot |
| 2025-01-15 17:07:16 +0100 | <tomsmeding> | right, that's a thing in agda |
| 2025-01-15 17:06:57 +0100 | <pounce> | you don't need to 'use' the proof |
| 2025-01-15 17:06:52 +0100 | <Leary> | It's /statically/ verified. Haskell's `Refl` requires pattern matching for soundness only because it's lifted. |
| 2025-01-15 17:06:50 +0100 | <pounce> | tomsmeding: if you have an inhabitant of the equality proof then it already holds |
| 2025-01-15 17:06:34 +0100 | Guest78 | (~Guest78@37.228.251.150) (Quit: Client closed) |
| 2025-01-15 17:06:25 +0100 | <tomsmeding> | but how can an equality proof be erased if you're depending on it to hold? |
| 2025-01-15 17:05:46 +0100 | <pounce> | i _think_ so. i usually use --without-k which doesn't allow all dot patterns for equality |
| 2025-01-15 17:05:06 +0100 | <tomsmeding> | pounce: if you pattern-match on a Refl in agda, can you still mark that argument as erased? |
| 2025-01-15 17:04:50 +0100 | <tomsmeding> | a zero-bit equality is just ensuring that there's no unnecessary runtime overhead in reifying the proof, whereas an erased equality is praying that the proof would have also held in production |
| 2025-01-15 17:03:56 +0100 | <tomsmeding> | Leary: but surely an erased equality is not quite the same as a zero-bit equality? |
| 2025-01-15 17:03:23 +0100 | <Leary> | tomsmeding: See this thread for a few examples: https://discourse.haskell.org/t/unboxed-equality/9929 |
| 2025-01-15 17:01:25 +0100 | alecs | (~alecs@nat16.software.imdea.org) (Ping timeout: 248 seconds) |
| 2025-01-15 17:01:00 +0100 | <tomsmeding> | (any other uses, that is) |