Newest at the top
| 2024-05-01 22:36:54 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-05-01 22:31:27 +0200 | madeleine-sydney | (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Konversation terminated!) |
| 2024-05-01 22:28:22 +0200 | k`` | (~k``@152.1.137.158) (Remote host closed the connection) |
| 2024-05-01 22:25:21 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Quit: Leaving) |
| 2024-05-01 22:23:01 +0200 | SteelBlueSilk | (~SteelBlue@user/SteelBlueSilk) |
| 2024-05-01 22:23:01 +0200 | SteelBlueSilk | (~SteelBlue@c-98-42-249-36.hsd1.ca.comcast.net) (Changing host) |
| 2024-05-01 22:23:01 +0200 | SteelBlueSilk | (~SteelBlue@c-98-42-249-36.hsd1.ca.comcast.net) |
| 2024-05-01 22:20:23 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 264 seconds) |
| 2024-05-01 22:16:24 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-05-01 22:16:01 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-01 22:15:26 +0200 | Luj | (~Luj@2a01:e0a:5f9:9681:d999:72f4:b788:a2bb) |
| 2024-05-01 22:15:08 +0200 | Luj | (~Luj@2a01:e0a:5f9:9681:627d:73c1:73b3:2561) (Quit: Ping timeout (120 seconds)) |
| 2024-05-01 22:13:27 +0200 | <monochrom> | (OK I am not teaching rank-2 types yet, so "caller chooses" has sufficed so far.) |
| 2024-05-01 22:12:28 +0200 | <monochrom> | Maybe I should teach that in my course too. (Currently I teach "caller chooses", "callee chooses".) |
| 2024-05-01 22:11:00 +0200 | <monochrom> | Yeah, that. |
| 2024-05-01 22:10:18 +0200 | <lyxia> | Instead of thinking in terms of rigid/"polymorphic" type variables, think in terms of input/output. newSTRef :: forall s. a -> ST s (STRef s a) takes a type s as an input. All of the ST functions except runST take s as an input. runST takes a function which takes a type s as an input, which means that runST (somehow) produces an s to be able to call that function. |
| 2024-05-01 22:10:10 +0200 | <monochrom> | The words "the result of the newSTRef" is ambiguous. The wrong interpretation leads to the wrong conclusion. |
| 2024-05-01 22:09:11 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2024-05-01 22:08:49 +0200 | <monochrom> | "(forall s. ST s (STRef s [Int]))" stays fully polymorphic. I thought you knew that's what the "forall" is doing. |
| 2024-05-01 22:07:15 +0200 | <mauke> | because the action you're passing to runST doesn't try to return an STRef. it just returns a list |
| 2024-05-01 22:06:36 +0200 | <mauke> | that still uses runST at type (forall s. ST s [Int]) -> [Int] |
| 2024-05-01 22:05:45 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-05-01 22:05:34 +0200 | <Guest67> | The new one, where the type signature is (forall s. ST s (STRef s [Int])) -> [Int] |
| 2024-05-01 22:05:00 +0200 | <mauke> | in your original code, a = [Int] |
| 2024-05-01 22:04:57 +0200 | <monochrom> | Which version of goo now? |
| 2024-05-01 22:04:03 +0200 | <Guest67> | So that part makes sense. But then why can I apply goo, which now requires s to be fully polymorphic, to the result of the newSTRef? I'm implicitly choosing 's' by choosing 'a', so the result is no longer fully polymorphic in s right? |
| 2024-05-01 22:02:54 +0200 | <mauke> | if the caller gets to choose 'a', it implicitly also chooses 's', and that's illegal |
| 2024-05-01 22:02:23 +0200 | tessd | (~test@evw199.neoplus.adsl.tpnet.pl) (Remote host closed the connection) |
| 2024-05-01 22:02:03 +0200 | <mauke> | (like if 'a = STRef s [Int]') |
| 2024-05-01 22:01:42 +0200 | <mauke> | this causes a conflict if 'a' includes 's' |
| 2024-05-01 22:01:23 +0200 | <mauke> | from a "who gets to choose" point of view, the caller of runST gets to choose 'a', but 's' has to be left polymorphic (as demanded by runST) |
| 2024-05-01 21:59:35 +0200 | <geekosaur> | outside those parenthses, s doesn't exist |
| 2024-05-01 21:59:26 +0200 | <geekosaur> | the second is that it delimits where s is meaningful: inside the parentheses where the forall occurs |
| 2024-05-01 21:59:08 +0200 | <geekosaur> | the first one we already discussed: "must accept any type for s" |
| 2024-05-01 21:58:50 +0200 | <geekosaur> | it does two things |
| 2024-05-01 21:58:46 +0200 | <geekosaur> | okay, let's go back to that forall |
| 2024-05-01 21:58:32 +0200 | <Guest67> | I don't want it to be legal, I'm moreso curious about why it is the case that it prevents that from happening |
| 2024-05-01 21:58:14 +0200 | <monochrom> | The rank-2 type is designed to ban that. |
| 2024-05-01 21:57:51 +0200 | <monochrom> | The purpose of runST is to never leak out mutable variables. So why should "runST (make a mutable variable and return it)" be legal? |
| 2024-05-01 21:57:29 +0200 | <geekosaur> | but newSTRef oproduces a value whose type includes an s |
| 2024-05-01 21:57:28 +0200 | <mauke> | because we're trying to return a result of type STRef s [Int] |
| 2024-05-01 21:57:10 +0200 | <mauke> | and in that example, the 'a' would have to contain an 's' somehow |
| 2024-05-01 21:57:07 +0200 | <geekosaur> | because outside the runST, s has no type |
| 2024-05-01 21:57:01 +0200 | <ncf> | s would escape its scope |
| 2024-05-01 21:56:54 +0200 | <mauke> | but the type of runST is (forall s. ST s a) -> a |
| 2024-05-01 21:56:50 +0200 | <monochrom> | Before I answer that, I ask back why would anyone want that to be legal? |
| 2024-05-01 21:56:42 +0200 | <mauke> | that one I don't have a good understanding/explanation of |
| 2024-05-01 21:55:43 +0200 | <Guest67> | But if that's the case, why can't I do runST $ newSTRef [1..10] |
| 2024-05-01 21:54:06 +0200 | <mauke> | 's' can still be arbitrary |
| 2024-05-01 21:53:41 +0200 | <mauke> | newSTRef just links up the STRef with its surrounding context (that is, it forces the two 's' parameters to be the same) |