Newest at the top
| 2025-01-24 15:50:35 +0100 | <Leary> | The strict definition should be that a universal or existential type has the corresponding quantifier outermost, but in the absense of the latter quantifier and the presence of reasonable encodings thereof, that definition obviously just isn't pragmatic enough. |
| 2025-01-24 15:50:31 +0100 | euleritian | (~euleritia@dynamic-176-006-139-225.176.6.pool.telefonica.de) |
| 2025-01-24 15:49:24 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 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) |