Logs: liberachat/#haskell
| 2025-12-12 11:00:40 | → | Enrico63 joins (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) |
| 2025-12-12 11:02:07 | <Enrico63> | Hi, there. I'd like some clarification on rank-n types. |
| 2025-12-12 11:02:08 | <Enrico63> | The id function has type `forall a. a -> a` which is rank 1, right? |
| 2025-12-12 11:03:53 | <lucabtz> | yes rank 1 |
| 2025-12-12 11:05:25 | <Enrico63> | Instead, if I have `(forall a. a -> a) -> b`, that's rank 2, right? |
| 2025-12-12 11:05:37 | <Enrico63> | (Be damned the formatting, ahhah) |
| 2025-12-12 11:06:02 | <Enrico63> | Well, that's the same as `forall b. (forall a. a -> a) -> b` |
| 2025-12-12 11:06:09 | <Enrico63> | It is rank 2, correct? |
| 2025-12-12 11:07:01 | <mauke> | https://wiki.haskell.org/Rank-N_types |
| 2025-12-12 11:07:52 | <Enrico63> | I come _from_ that page |
| 2025-12-12 11:08:52 | <mauke> | well, it's what I would've used to answer your question :-) |
| 2025-12-12 11:09:41 | <Enrico63> | Yeah, I don't quite get what's unclear to me, so I asked those previous questions to have something to hinge on |
| 2025-12-12 11:10:10 | <mauke> | (the answer is yes) |
| 2025-12-12 11:12:00 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-12-12 11:12:08 | <haskellbridge> | <loonycyborg> I personally found the trick to understanding rank-n is that they're about polymorphic functions that can take other polymorphic functions. |
| 2025-12-12 11:12:31 | × | trickard quits (~trickard@cpe-83-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-12 11:12:37 | <Enrico63> | loonycyborg, yeah, I'm also (halfway) there |
| 2025-12-12 11:12:39 | <haskellbridge> | <loonycyborg> With rank 1 all variables are set at outer scope and you won't be passing any polymorphic functions. |
| 2025-12-12 11:13:44 | <Enrico63> | Whereas rank 2 means that the implementation (i.e. the inner scope) chooses the type variable of the inner forall |
| 2025-12-12 11:15:05 | <Enrico63> | I kind of get that. I suppose I want to do a quiz to make sure I have truly understood, rather than memoized some patterns |
| 2025-12-12 11:15:15 | → | trickard_ joins (~trickard@cpe-83-98-47-163.wireline.com.au) |
| 2025-12-12 11:16:06 | <lucabtz> | i think rank N means it has rank N-1 as its arguments, the base case rank 0 being a monomorphic value/function |
| 2025-12-12 11:16:30 | <mauke> | forall b. ((forall a. a -> b) -> b) -> b |
| 2025-12-12 11:16:59 | <mauke> | is that rank-2? |
| 2025-12-12 11:17:12 | <Enrico63> | mauke, that is rank 3? |
| 2025-12-12 11:17:20 | <mauke> | according to the wiki page, it's rank 2 |
| 2025-12-12 11:18:04 | <Enrico63> | Umpf |
| 2025-12-12 11:18:21 | <mauke> | but then, according to that page (forall a. a) -> Int is rank 1 |
| 2025-12-12 11:18:26 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-12 11:18:40 | <mauke> | this doesn't feel right |
| 2025-12-12 11:18:53 | <Enrico63> | Yeah, how's that? `Int -> Int` is rank 0, right? |
| 2025-12-12 11:19:07 | <Enrico63> | `forall a. a -> a` (e.g. the type of id) is rank 1 |
| 2025-12-12 11:19:13 | × | pabs3 quits (~pabs3@user/pabs3) (Ping timeout: 246 seconds) |
| 2025-12-12 11:19:41 | <Enrico63> | and the caller "chooses" the `a` |
| 2025-12-12 11:20:26 | <Enrico63> | then in `(forall a. a -> a) -> b`, where there's an implicit `forall b.` in front of everyting, b is chosen by the caller, but a is chosen by the implementation |
| 2025-12-12 11:20:59 | <Enrico63> | so that means `(forall a. a -> a) -> b` is rank 2, to my understanding. How is `(forall a. a) -> Int` any different in this respect? |
| 2025-12-12 11:21:21 | <mauke> | the wiki page defines "rank" as the number of foralls in the type |
| 2025-12-12 11:22:31 | <lucabtz> | mauke: it doesnt though, it says forall a. a -> (forall b. b -> a) is rank 1 |
| 2025-12-12 11:22:31 | <Enrico63> | *which are nested and cannot be merged with a previous one* |
| 2025-12-12 11:22:53 | <mauke> | lucabtz: that one is mergeable |
| 2025-12-12 11:23:08 | <lucabtz> | yeah you were missing what Enrico63 added :P |
| 2025-12-12 11:23:18 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-12 11:23:33 | <mauke> | that still leaves (forall a. a) -> Int at rank 1 |
| 2025-12-12 11:23:47 | <Enrico63> | It should be rank 2, I understand |
| 2025-12-12 11:24:48 | trickard_ | is now known as trickard |
| 2025-12-12 11:25:31 | <Enrico63> | For instance, this compiles |
| 2025-12-12 11:25:31 | <Enrico63> | foo :: (forall a. a) -> Int |
| 2025-12-12 11:25:32 | <Enrico63> | foo x = x + 1 |
| 2025-12-12 11:26:10 | <Enrico63> | which means that the implementation of foo is choosing a=Int, which could not be the case if foo was rank 1, because the caller would choose a. |
| 2025-12-12 11:26:11 | <Enrico63> | No? |
| 2025-12-12 11:28:10 | <Enrico63> | Anyway, going to the exercises I found on the book "Thinking with Types" that I'm reading, `Int -> forall a. a -> a` is rank 1, correct? |
| 2025-12-12 11:30:52 | <mauke> | this looks much better: https://stackoverflow.com/questions/22362196/what-is-n-in-rankntypes |
| 2025-12-12 11:31:19 | <mauke> | Enrico63: yes, that's a H98 type (by floating out the forall) |
| 2025-12-12 11:31:28 | <merijn> | Enrico63: This is the clearest example of Rank1 vs RankN I cooked up a few years ago: https://gist.github.com/merijn/77e3fa9757658e59b01d |
| 2025-12-12 11:32:20 | <mauke> | yeah, when I search for "rank-n type", most results are examples like ^ |
| 2025-12-12 11:32:33 | <mauke> | which is useless if I want to know the actual definition of "rank" |
| 2025-12-12 11:32:43 | → | pabs3 joins (~pabs3@user/pabs3) |
| 2025-12-12 11:32:46 | <merijn> | sure |
| 2025-12-12 11:32:58 | <mauke> | the SO page I found is better, but includes two incompatible answers :-) |
| 2025-12-12 11:33:18 | <merijn> | then again, in practice there's very little value in knowing the exact rank of a type :p |
| 2025-12-12 11:33:30 | → | Square2 joins (~Square@user/square) |
| 2025-12-12 11:33:37 | <merijn> | In practice the value is understanding "why does this not compile and how can I make it do what I want" :p |
| 2025-12-12 11:34:01 | <merijn> | Especially since GHC doesn't even distinguish between Rank2 and RankN |
| 2025-12-12 12:01:13 | × | __monty__ quits (~toonn@user/toonn) (Ping timeout: 264 seconds) |
| 2025-12-12 12:02:19 | → | __monty__ joins (~toonn@user/toonn) |
| 2025-12-12 12:02:46 | × | pabs3 quits (~pabs3@user/pabs3) (Ping timeout: 244 seconds) |
| 2025-12-12 12:04:28 | → | pabs3 joins (~pabs3@user/pabs3) |
| 2025-12-12 12:16:13 | → | Katarushisu joins (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
| 2025-12-12 12:20:57 | → | Googulator50 joins (~Googulato@team.broadbit.hu) |
| 2025-12-12 12:24:43 | × | Googulator quits (~Googulato@team.broadbit.hu) (Ping timeout: 272 seconds) |
| 2025-12-12 12:27:35 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 240 seconds) |
| 2025-12-12 12:29:25 | × | lucabtz quits (~lucabtz@user/lucabtz) (Ping timeout: 264 seconds) |
| 2025-12-12 12:30:17 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
| 2025-12-12 12:35:12 | → | lucabtz joins (~lucabtz@user/lucabtz) |
| 2025-12-12 12:35:24 | <lucabtz> | isnt the definition as rank N has as parameters rank N-1 types correct? |
| 2025-12-12 12:36:47 | → | xff0x joins (~xff0x@2405:6580:b080:900:d3a9:b169:555e:b9ec) |
| 2025-12-12 12:38:55 | × | Enrico63 quits (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) (Quit: Client closed) |
| 2025-12-12 12:44:11 | × | tromp quits (~textual@2001:1c00:3487:1b00:dd4:56d:fd02:60e2) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-12-12 12:55:30 | × | lucabtz quits (~lucabtz@user/lucabtz) (Quit: leaving) |
| 2025-12-12 12:56:23 | × | Googulator50 quits (~Googulato@team.broadbit.hu) (Ping timeout: 272 seconds) |
| 2025-12-12 12:59:13 | → | lucabtz joins (~lucabtz@user/lucabtz) |
| 2025-12-12 13:02:24 | → | lucabtz_ joins (~lucabtz@user/lucabtz) |
| 2025-12-12 13:03:39 | <merijn> | Yes, but then pinning down exactly what that means isn't always obvious in Haskell given that the source language doesn't always match the one with explicit foralls directly |
| 2025-12-12 13:04:34 | × | lucabtz quits (~lucabtz@user/lucabtz) (Ping timeout: 246 seconds) |
| 2025-12-12 13:06:30 | <lucabtz_> | though the only foralls which can be implicit are the ones at the top level no? |
| 2025-12-12 13:07:05 | lucabtz_ | is now known as lucabtz |
| 2025-12-12 13:12:55 | → | fp joins (~Thunderbi@2001:708:150:10::7e06) |
| 2025-12-12 13:17:41 | × | fp quits (~Thunderbi@2001:708:150:10::7e06) (Ping timeout: 244 seconds) |
| 2025-12-12 13:24:02 | × | trickard quits (~trickard@cpe-83-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-12 13:24:15 | → | trickard joins (~trickard@cpe-83-98-47-163.wireline.com.au) |
| 2025-12-12 13:27:31 | → | fp joins (~Thunderbi@130.233.70.102) |
| 2025-12-12 13:29:35 | → | stef204 joins (~stef204@user/stef204) |
| 2025-12-12 13:31:33 | → | Enrico63 joins (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) |
| 2025-12-12 13:40:57 | × | Everything quits (~Everythin@172-232-54-192.ip.linodeusercontent.com) (Quit: leaving) |
| 2025-12-12 14:03:54 | → | tromp joins (~textual@2001:1c00:3487:1b00:dd4:56d:fd02:60e2) |
| 2025-12-12 14:06:49 | → | karenw joins (~karenw@user/karenw) |
| 2025-12-12 14:08:37 | → | euphores joins (~SASL_euph@user/euphores) |
| 2025-12-12 14:20:54 | → | Square joins (~Square4@user/square) |
| 2025-12-12 14:26:44 | × | ouilemur quits (~jgmerritt@user/ouilemur) (Ping timeout: 260 seconds) |
| 2025-12-12 14:30:16 | → | ouilemur joins (~jgmerritt@user/ouilemur) |
All times are in UTC.