Newest at the top
| 2025-01-24 15:33:27 +0100 | <dminuoso> | s/too is an /too has an/ |
| 2025-01-24 15:32:12 +0100 | <dminuoso> | If an existential type is any quantified type where an `∃a. ...` could appear in, then `id` too is an existential type because we could encode it in terms of an existential quantifier. |
| 2025-01-24 15:31:20 +0100 | <dminuoso> | Not quite sure whether we can give a clean and accurate definition of what "an existential type" is exactly. |
| 2025-01-24 15:30:55 +0100 | <dminuoso> | Except that you encode it via the above isomorphism. |
| 2025-01-24 15:30:47 +0100 | <dminuoso> | We do not have existential quantification. |
| 2025-01-24 15:30:43 +0100 | <dminuoso> | kuribas: Let me rephrase: |
| 2025-01-24 15:30:33 +0100 | <kuribas> | We do have existential types. |
| 2025-01-24 15:27:49 +0100 | <dminuoso> | Yes we do not have `∃x.` .. but then again we do not really have existential codes (except for those encoded via universal quantification) |
| 2025-01-24 15:27:38 +0100 | <merijn> | Actually ∀ totally is valid haskell with -XUnicodeSyntax :p |
| 2025-01-24 15:27:20 +0100 | <dminuoso> | kuribas: Half of it is. |
| 2025-01-24 15:26:56 +0100 | <kuribas> | dminuoso: that's not valid haskell syntax |
| 2025-01-24 15:24:10 +0100 | Googulator | (~Googulato@host-88-132-146-182.prtelecom.hu) (Ping timeout: 240 seconds) |
| 2025-01-24 15:22:09 +0100 | <dminuoso> | ncf: Oh, I indeed mixed this one up. |
| 2025-01-24 15:19:38 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-01-24 15:15:12 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-24 15:12:43 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 264 seconds) |
| 2025-01-24 15:11:46 +0100 | Arsen_ | Arsen |
| 2025-01-24 15:11:41 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-24 15:07:57 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-24 15:05:33 +0100 | KicksonButt | (~quassel@187.21.174.221) |
| 2025-01-24 15:05:14 +0100 | KicksonButt | (~quassel@187.21.174.221) (Client Quit) |
| 2025-01-24 15:00:56 +0100 | KicksonButt | (~quassel@187.21.174.221) |
| 2025-01-24 14:56:29 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds) |
| 2025-01-24 14:56:26 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2025-01-24 14:40:19 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-24 14:39:19 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-24 14:38:30 +0100 | Everything | (~Everythin@195.138.86.118) Everything |
| 2025-01-24 14:28:41 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-01-24 14:22:24 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-24 14:20:13 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-24 14:20:08 +0100 | <ncf> | yes |
| 2025-01-24 14:19:11 +0100 | <kuribas> | well (forall a. Num a => a) |
| 2025-01-24 14:18:51 +0100 | <ncf> | no |
| 2025-01-24 14:18:25 +0100 | <kuribas> | ncf: it is with impredicative types enabled? |
| 2025-01-24 14:18:12 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-24 14:16:10 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-24 14:02:47 +0100 | iamsleepy | (~weechat@2a01:4f9:3070:feff:a9de:dfff:cd7f:fdcd) iamsleepy |
| 2025-01-24 14:02:23 +0100 | iamsleepy | (~weechat@2a01:4f9:3070:feff:9969:2d95:7b68:eef5) (Read error: Connection reset by peer) |
| 2025-01-24 14:01:07 +0100 | visilii | (~visilii@46.61.242.99) |
| 2025-01-24 13:59:48 +0100 | visilii | (~visilii@46.61.242.99) (Read error: Connection reset by peer) |
| 2025-01-24 13:52:49 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-24 13:52:24 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2025-01-24 13:46:28 +0100 | jespada | (~jespada@2800:a4:2288:4600:a43e:beb4:c592:b90b) jespada |
| 2025-01-24 13:42:35 +0100 | Googulator | (~Googulato@host-88-132-146-182.prtelecom.hu) |
| 2025-01-24 13:33:54 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-24 13:33:10 +0100 | dysthesis | (~dysthesis@user/dysthesis) (Remote host closed the connection) |
| 2025-01-24 13:30:55 +0100 | <ncf> | (∃a. ... a ...) -> r is not |
| 2025-01-24 13:30:51 +0100 | <ncf> | dminuoso: (∃a. ... a ...) is an existential type |
| 2025-01-24 13:29:57 +0100 | <ncf> | forall a. Num a is not a type |
| 2025-01-24 13:29:28 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |