Newest at the top
| 2025-01-24 15:38:55 +0100 | <dminuoso> | Leary: I just wanted to use GADTSyntax to avoid some confusion. |
| 2025-01-24 15:38:36 +0100 | <dminuoso> | Leary: Sure or that. |
| 2025-01-24 15:38:19 +0100 | <Leary> | dminuoso: That should be `(exists a. a)`; you wouldn't even need GADTSyntax to write it. |
| 2025-01-24 15:37:47 +0100 | <yahb2> | Foo :: a -> Foo |
| 2025-01-24 15:37:47 +0100 | <dminuoso> | % :t Foo |
| 2025-01-24 15:37:45 +0100 | <yahb2> | <no output> |
| 2025-01-24 15:37:45 +0100 | <dminuoso> | % data Foo = forall a. Foo a |
| 2025-01-24 15:37:36 +0100 | <yahb2> | <no output> |
| 2025-01-24 15:37:36 +0100 | <dminuoso> | % :set -XExistentialQuantification |
| 2025-01-24 15:37:22 +0100 | <dminuoso> | Instead it uses a very strange notation where you put the `forall a` into a strange spot, there by impying that. |
| 2025-01-24 15:36:53 +0100 | <dminuoso> | `data Foo where Foo :: exists a. a -> Foo` |
| 2025-01-24 15:36:36 +0100 | <dminuoso> | So the language extension *is* called ExistentialQuantification, and if it had been faithful, it would have allowed to write: |
| 2025-01-24 15:36:16 +0100 | <dminuoso> | That one is a bit funny. |
| 2025-01-24 15:36:13 +0100 | <kuribas> | Foo is not a function type. |
| 2025-01-24 15:35:59 +0100 | <kuribas> | a is existential in Foo. |
| 2025-01-24 15:35:47 +0100 | <kuribas> | "data Foo = forall a. Foo a" is an existential type. |
| 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? |