Newest at the top
| 2025-01-23 15:32:54 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-01-23 15:30:06 +0100 | Googulator91 | Googulator |
| 2025-01-23 15:29:21 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-23 15:28:34 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-01-23 15:26:17 +0100 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-01-23 15:25:57 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-23 15:19:38 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-01-23 15:19:38 +0100 | taleseeker | (~taleseeke@185.107.44.16) (Quit: irc: cannot access '/proc/taleseeker': No such file or directory) |
| 2025-01-23 15:17:52 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 272 seconds) |
| 2025-01-23 15:17:00 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-23 15:16:18 +0100 | euleritian | (~euleritia@dynamic-176-006-148-054.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-23 15:15:54 +0100 | euleritian | (~euleritia@dynamic-176-006-148-054.176.6.pool.telefonica.de) |
| 2025-01-23 15:15:22 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-01-23 15:15:20 +0100 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 272 seconds) |
| 2025-01-23 15:13:29 +0100 | <ncf> | (using the syntax of the first-class existentials GHC proposal) |
| 2025-01-23 15:13:17 +0100 | <ncf> | SomeFoo :: (exists a. Foo a /\ a) -> SomeFoo |
| 2025-01-23 15:13:07 +0100 | <ncf> | the former could be rewritten, in pseudo-haskell, |
| 2025-01-23 15:12:47 +0100 | <ncf> | AnyFoo :: (forall a. Foo a => a) -> AnyFoo |
| 2025-01-23 15:12:39 +0100 | <ncf> | data AnyFoo where |
| 2025-01-23 15:12:37 +0100 | <ncf> | please note the difference with |
| 2025-01-23 15:12:32 +0100 | zero | yin |
| 2025-01-23 15:12:28 +0100 | <ncf> | SomeFoo :: forall a. Foo a => a -> SomeFoo |
| 2025-01-23 15:12:24 +0100 | <ncf> | er sorry |
| 2025-01-23 15:12:00 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 2025-01-23 15:10:36 +0100 | <ncf> | the syntax is precisely what confuses you here |
| 2025-01-23 15:10:27 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-23 15:10:03 +0100 | <merijn> | I forgot the syntax, since it's been awhile, you get the idea |
| 2025-01-23 15:09:51 +0100 | <ncf> | in GADT syntax |
| 2025-01-23 15:09:47 +0100 | <ncf> | SomeFoo :: forall a. Foo a => SomeFoo |
| 2025-01-23 15:09:36 +0100 | <ncf> | data SomeFoo where |
| 2025-01-23 15:09:31 +0100 | <ncf> | this is shorthand for |
| 2025-01-23 15:09:23 +0100 | <ncf> | note that the universal context is outside of the constructor |
| 2025-01-23 15:09:08 +0100 | <ncf> | data SomeFoo = forall a. Foo a => SomeFoo a |
| 2025-01-23 15:08:57 +0100 | <ncf> | no |
| 2025-01-23 15:08:35 +0100 | <merijn> | ncf: The only way to represent existentials in GHC is via `newtype SomeFoo = SomeFoo (forall a . Foo a => a)` |
| 2025-01-23 15:08:31 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2025-01-23 15:07:59 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2025-01-23 15:07:33 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-23 15:07:11 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-23 15:05:50 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 2025-01-23 15:05:27 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-01-23 15:04:42 +0100 | CiaoSen | (~Jura@2a05:5800:223:9800:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds) |
| 2025-01-23 15:04:26 +0100 | <ncf> | forall a. Num a => a does not produce a type. it accepts a type |
| 2025-01-23 15:03:42 +0100 | <ncf> | i don't see any existentials here, church-encoded or not |
| 2025-01-23 15:03:40 +0100 | Guest44 | (~Guest44@2409:40f4:101c:dd54:1dc9:6365:96b5:504a) (Ping timeout: 240 seconds) |
| 2025-01-23 15:03:09 +0100 | <Leary> | Well, one of us is confused, because I'm pretty sure nothing is existential here. |
| 2025-01-23 15:02:37 +0100 | <merijn> | Don't blame me for having to write existentials with forall rather than exists, blame the Simon's and GHC team :p |
| 2025-01-23 15:01:53 +0100 | taleseeker | (~taleseeke@185.107.44.16) |
| 2025-01-23 15:01:47 +0100 | <merijn> | Leary: It *is* an existential, but haskell encodes those as hidden foralls |
| 2025-01-23 15:01:31 +0100 | <merijn> | [forall a . Num a => a] has the *exact* same restrictions as IORef |