Newest at the top
| 2025-01-24 15:48:06 +0100 | <dminuoso> | Maybe we should not use these terms at all. |
| 2025-01-24 15:47:45 +0100 | <dminuoso> | (Which begs the question what to call a type has both an existential and universal quantifier inside) |
| 2025-01-24 15:47:11 +0100 | <dminuoso> | Otherwise there would be no distinction between "universal type" and "existential type", and thereby no reason to have two terms. |
| 2025-01-24 15:46:32 +0100 | <dminuoso> | If its encoded via unviersal quantification, I would not call it an "existential type" |
| 2025-01-24 15:46:12 +0100 | <dminuoso> | I think the only sensible definition of "existential type" is one that has an existential quantifier inside it. |
| 2025-01-24 15:45:59 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:3d80:bfe2:3c69:fb84) ubert |
| 2025-01-24 15:45:07 +0100 | <Leary> | Shouldda swapped those args, but you get the picture. |
| 2025-01-24 15:44:29 +0100 | <Leary> | *Foo -> r |
| 2025-01-24 15:43:14 +0100 | <Leary> | kuribas: `Foo` is also effectively "encoded via universal quantification" due to the fact that we need to type any code that interacts with it using only `forall`: `Foo :: forall a. a -> Foo`; `\f -> \case{ Foo x -> f x } :: forall r. (forall a. a -> r) -> r`. |
| 2025-01-24 15:41:04 +0100 | <dminuoso> | Can you make GHC print out quantifiers explicitly with :t ? |
| 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) |