Logs: liberachat/#haskell
| 2021-08-03 05:08:22 | → | cocreature joins (~moritz@2a03:b0c0:3:d0::c8:f001) |
| 2021-08-03 05:08:22 | → | beaky joins (~beaky@2a03:b0c0:0:1010::1e:a001) |
| 2021-08-03 05:08:25 | → | pie_ joins (~pie_bnc@user/pie/x-2818909) |
| 2021-08-03 05:08:27 | → | ouroboros joins (~ouroboros@user/ouroboros) |
| 2021-08-03 05:08:30 | → | biberu joins (~biberu@user/biberu) |
| 2021-08-03 05:08:31 | → | vemek joins (~vemek@2a03:b0c0:2:d0::d98:1) |
| 2021-08-03 05:08:31 | → | hook54321 joins (sid149355@user/hook54321) |
| 2021-08-03 05:09:48 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 258 seconds) |
| 2021-08-03 05:11:04 | <glguy> | Axman6, I need to restart stuff periodically for it to get kernel and IRCd updates |
| 2021-08-03 05:11:41 | → | barrucadu joins (~barrucadu@carcosa.barrucadu.co.uk) |
| 2021-08-03 05:12:13 | <Axman6> | needs more unikernels |
| 2021-08-03 05:12:21 | <glguy> | Axman6, if you're interested in stuff like that, set usermode +w to get the broadcasts |
| 2021-08-03 05:12:51 | × | amirouche quits (~amirouche@2a01:4f8:c0c:d9c2::1) (Changing host) |
| 2021-08-03 05:12:51 | → | amirouche joins (~amirouche@user/amirouche) |
| 2021-08-03 05:12:57 | <Axman6> | how do I make that the default in glirc? |
| 2021-08-03 05:13:07 | <glguy> | add it to your connect-cmds |
| 2021-08-03 05:13:19 | <Axman6> | :thumbsup: |
| 2021-08-03 05:13:28 | <glguy> | "umode +w" |
| 2021-08-03 05:14:23 | × | Axman6 quits (~Axman6@user/axman6) (Remote host closed the connection) |
| 2021-08-03 05:14:38 | → | Axman6 joins (~Axman6@user/axman6) |
| 2021-08-03 05:15:32 | <Axman6> | noice |
| 2021-08-03 05:16:56 | → | bitmapper joins (uid464869@id-464869.tooting.irccloud.com) |
| 2021-08-03 05:25:37 | → | steven1 joins (~steven@172.92.136.203) |
| 2021-08-03 05:26:17 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-08-03 05:27:20 | <steven1> | hello, does anyone have a reference/explanation on the relationship between universally quantified types and existantial types? I've seen in a couple cases we can implement existential types in haskell using rank 2 types but I didn't understand how it works |
| 2021-08-03 05:27:52 | <steven1> | this paper makes a passing reference to 'the usual interchange laws between existentiaial and universal quantifiers' but I don't know what they are https://arxiv.org/pdf/1309.5135.pdf |
| 2021-08-03 05:28:28 | <shachaf> | Hmm, I think it's simplest to think of it in terms of dependent types, if you're familiar with that. |
| 2021-08-03 05:28:40 | <steven1> | I know there's de morgan's law to convert the negation of one into the other but I don't think that's what we're doing in haskell usually |
| 2021-08-03 05:28:46 | <steven1> | shachaf: hmm not really |
| 2021-08-03 05:28:49 | <steven1> | only a little bit |
| 2021-08-03 05:28:54 | <shachaf> | Well, you only need a little bit. |
| 2021-08-03 05:29:47 | <shachaf> | So in something like Agda, universal quantifiers are represented as dependent functions from a type, and existential quantifiers are represented as a dependent pair -- have you seen that? |
| 2021-08-03 05:30:04 | <shachaf> | E.g. id : (a : Type) -> a -> a |
| 2021-08-03 05:30:05 | <steven1> | right, I watched richard eisenberg's series on implementing a length-indexed vector and I know in that he created something like an existential type for `filter` |
| 2021-08-03 05:30:32 | <steven1> | not sure about dependent pairs |
| 2021-08-03 05:30:38 | <shachaf> | Existentials might be represented like this: (a : Type, (a, a -> Int)) |
| 2021-08-03 05:31:00 | <shachaf> | A tuple where the first element is a type and the second element is a value that uses that type. |
| 2021-08-03 05:31:10 | <shachaf> | In Haskell you'd write (exists a. (a, a -> Int)) |
| 2021-08-03 05:31:22 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 250 seconds) |
| 2021-08-03 05:31:24 | <shachaf> | (Well, in fake Haskell.) |
| 2021-08-03 05:31:32 | <steven1> | ok, this construction looks similar to what I saw in the paper |
| 2021-08-03 05:31:53 | <shachaf> | Does this make sense? |
| 2021-08-03 05:32:13 | <steven1> | how would I express it using forall? |
| 2021-08-03 05:32:22 | <shachaf> | That's the next bit. |
| 2021-08-03 05:32:44 | <shachaf> | So if you have any type T in Haskell, it's isomorphic to (forall r. (T -> r) -> r), right? |
| 2021-08-03 05:33:14 | <steven1> | hm that's not clear to me |
| 2021-08-03 05:33:41 | <shachaf> | OK, I think that comes first. |
| 2021-08-03 05:33:58 | <shachaf> | Imagine you have to implement f :: forall r. (Int -> r) -> r |
| 2021-08-03 05:34:16 | <shachaf> | Can you write an implementation? |
| 2021-08-03 05:34:29 | <steven1> | f g = g 0 ? |
| 2021-08-03 05:34:38 | <shachaf> | Right. |
| 2021-08-03 05:34:48 | <shachaf> | Or in general f g = g n, for some n : Int. |
| 2021-08-03 05:34:57 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-03 05:35:07 | <shachaf> | But there has to be a specific Int, since you know nothing else about r. You just have to pass g an Int to get an r. |
| 2021-08-03 05:35:15 | <steven1> | yep |
| 2021-08-03 05:35:52 | <shachaf> | So you can write functions :: Int -> forall r. (Int -> r) -> r and :: (forall r. (Int -> r) -> r) -> Int and show they're inverses, I guess with parametricity. |
| 2021-08-03 05:36:09 | <steven1> | so maybe it can be something like f :: forall r proxy. (proxy a -> r) -> r |
| 2021-08-03 05:36:21 | <steven1> | that way we don't need a value with that type |
| 2021-08-03 05:36:31 | <shachaf> | Well, the whole point is that you *do* need a value with that type. |
| 2021-08-03 05:36:56 | <shachaf> | A (forall r. (T -> r) -> r) is a slightly weird (continuation-passing style) representation of a T. |
| 2021-08-03 05:37:08 | <steven1> | got it |
| 2021-08-03 05:37:44 | <shachaf> | So now if we have (exists a. Foo a) |
| 2021-08-03 05:38:06 | <shachaf> | We can think of it as a tuple, ((a : Type), Foo a) |
| 2021-08-03 05:38:21 | <steven1> | yep |
| 2021-08-03 05:38:36 | <steven1> | and you point is that we have a way to represent the type now |
| 2021-08-03 05:38:41 | <shachaf> | And do this CPS thing to get forall r. (((a : Type), Foo a) -> r) -> r |
| 2021-08-03 05:39:04 | <shachaf> | And that's still a representation of the same value |
| 2021-08-03 05:39:30 | <shachaf> | Now we have a function that takes a tuple as an argument, so we can just curry it. |
| 2021-08-03 05:39:32 | → | thyriaen joins (~thyriaen@dynamic-078-055-141-033.78.55.pool.telefonica.de) |
| 2021-08-03 05:39:51 | <shachaf> | Can you write the curried version? |
| 2021-08-03 05:39:57 | × | slowButPresent quits (~slowButPr@user/slowbutpresent) (Quit: leaving) |
| 2021-08-03 05:40:48 | <steven1> | forall r. (forall a. Foo a -> r) -> r since the Type argument becomes a type lambda? |
| 2021-08-03 05:41:17 | <shachaf> | Right, the exists turns into a forall when you curry it. |
| 2021-08-03 05:41:27 | <shachaf> | And that's the standard rank-2 representation for existentials. |
| 2021-08-03 05:42:34 | <steven1> | wow that's interesting. thanks for this |
| 2021-08-03 05:42:53 | <shachaf> | Maybe this is a little contrived as a path to get to this. |
| 2021-08-03 05:43:48 | × | jjhoo quits (~jahakala@dsl-trebng21-58c18f-56.dhcp.inet.fi) (Ping timeout: 268 seconds) |
| 2021-08-03 05:43:55 | <steven1> | btw where did you pick up this stuff? I tried searching around but couldn't find answers before |
| 2021-08-03 05:44:37 | <shachaf> | From the aether. |
| 2021-08-03 05:45:00 | bradparker_ | is now known as bradparker |
| 2021-08-03 05:45:21 | <shachaf> | (I have no idea!) |
| 2021-08-03 05:45:41 | <steven1> | haha understandable. I think a lot of this stuff just gets absorbed from exposure |
| 2021-08-03 05:50:40 | → | jneira joins (~jneira@212.8.115.226) |
| 2021-08-03 05:51:54 | V__ | is now known as V |
| 2021-08-03 05:54:22 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
| 2021-08-03 05:58:33 | <Axman6> | I feel like that's one of the reasons I struggle with pointing people to good resources to learn haskell, beucase I learnt so much in here |
| 2021-08-03 05:59:07 | <steven1> | followup question: since the construction that we did is purely mechanical, what's stopping GHC from supporting an `exists` syntax? I guess the call site might have to change too? |
| 2021-08-03 06:00:21 | <steven1> | Axman6: right, it's hard to find resources sometimes. Actually I was considering writing up a post about this since others may have the question too (I will credit you for the help shachaf if I do) |
| 2021-08-03 06:00:58 | <steven1> | seems that this is a trivial thing for some people but I don't think it's something I would have been able to come up with on my own |
| 2021-08-03 06:01:06 | <shachaf> | Well, "implicit" existential types are trickier than explicit. |
| 2021-08-03 06:01:23 | <shachaf> | I think YHC or UHC or something supported exists syntax, but I'm not sure what it did exactly. |
| 2021-08-03 06:01:40 | <shachaf> | If you can figure out all the behaviors you can propose it, I guess! |
| 2021-08-03 06:01:55 | <shachaf> | GHC does support explicit existential types, though. |
| 2021-08-03 06:02:11 | <shachaf> | You can write "data Thing = forall a. Thing a (a -> Int)" and so on. |
| 2021-08-03 06:02:32 | <Axman6> | what would foo :: exists a. a -> String even mean... you jhve to find the right a? |
| 2021-08-03 06:02:42 | <steven1> | right, but I'm thinking of a syntax for `exists a. Thing a` |
| 2021-08-03 06:02:48 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2021-08-03 06:02:55 | <shachaf> | Or "data Thing where { Thing :: forall a. a -> (a -> Int) -> Thing }" |
| 2021-08-03 06:03:09 | <shachaf> | The similarity between that and the construction above isn't a coincidence! |
| 2021-08-03 06:03:28 | × | shriekingnoise quits (~shrieking@186.137.144.80) (Quit: Quit) |
All times are in UTC.