Newest at the top
| 2025-12-12 12:34:01 +0100 | <merijn> | Especially since GHC doesn't even distinguish between Rank2 and RankN |
| 2025-12-12 12:33:37 +0100 | <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 12:33:30 +0100 | Square2 | (~Square@user/square) Square |
| 2025-12-12 12:33:18 +0100 | <merijn> | then again, in practice there's very little value in knowing the exact rank of a type :p |
| 2025-12-12 12:32:58 +0100 | <mauke> | the SO page I found is better, but includes two incompatible answers :-) |
| 2025-12-12 12:32:46 +0100 | <merijn> | sure |
| 2025-12-12 12:32:43 +0100 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 2025-12-12 12:32:33 +0100 | <mauke> | which is useless if I want to know the actual definition of "rank" |
| 2025-12-12 12:32:20 +0100 | <mauke> | yeah, when I search for "rank-n type", most results are examples like ^ |
| 2025-12-12 12:31:28 +0100 | <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 12:31:19 +0100 | <mauke> | Enrico63: yes, that's a H98 type (by floating out the forall) |
| 2025-12-12 12:30:52 +0100 | <mauke> | this looks much better: https://stackoverflow.com/questions/22362196/what-is-n-in-rankntypes |
| 2025-12-12 12:28:10 +0100 | <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 12:26:11 +0100 | <Enrico63> | No? |
| 2025-12-12 12:26:10 +0100 | <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 12:25:32 +0100 | <Enrico63> | foo x = x + 1 |
| 2025-12-12 12:25:31 +0100 | <Enrico63> | foo :: (forall a. a) -> Int |
| 2025-12-12 12:25:31 +0100 | <Enrico63> | For instance, this compiles |
| 2025-12-12 12:24:48 +0100 | trickard_ | trickard |
| 2025-12-12 12:23:47 +0100 | <Enrico63> | It should be rank 2, I understand |
| 2025-12-12 12:23:33 +0100 | <mauke> | that still leaves (forall a. a) -> Int at rank 1 |
| 2025-12-12 12:23:18 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-12 12:23:08 +0100 | <lucabtz> | yeah you were missing what Enrico63 added :P |
| 2025-12-12 12:22:53 +0100 | <mauke> | lucabtz: that one is mergeable |
| 2025-12-12 12:22:31 +0100 | <Enrico63> | *which are nested and cannot be merged with a previous one* |
| 2025-12-12 12:22:31 +0100 | <lucabtz> | mauke: it doesnt though, it says forall a. a -> (forall b. b -> a) is rank 1 |
| 2025-12-12 12:21:21 +0100 | <mauke> | the wiki page defines "rank" as the number of foralls in the type |
| 2025-12-12 12:20:59 +0100 | <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 12:20:26 +0100 | <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 12:19:41 +0100 | <Enrico63> | and the caller "chooses" the `a` |
| 2025-12-12 12:19:13 +0100 | pabs3 | (~pabs3@user/pabs3) (Ping timeout: 246 seconds) |
| 2025-12-12 12:19:07 +0100 | <Enrico63> | `forall a. a -> a` (e.g. the type of id) is rank 1 |
| 2025-12-12 12:18:53 +0100 | <Enrico63> | Yeah, how's that? `Int -> Int` is rank 0, right? |
| 2025-12-12 12:18:40 +0100 | <mauke> | this doesn't feel right |
| 2025-12-12 12:18:26 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-12 12:18:21 +0100 | <mauke> | but then, according to that page (forall a. a) -> Int is rank 1 |
| 2025-12-12 12:18:04 +0100 | <Enrico63> | Umpf |
| 2025-12-12 12:17:20 +0100 | <mauke> | according to the wiki page, it's rank 2 |
| 2025-12-12 12:17:12 +0100 | <Enrico63> | mauke, that is rank 3? |
| 2025-12-12 12:16:59 +0100 | <mauke> | is that rank-2? |
| 2025-12-12 12:16:30 +0100 | <mauke> | forall b. ((forall a. a -> b) -> b) -> b |
| 2025-12-12 12:16:06 +0100 | <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 12:15:15 +0100 | trickard_ | (~trickard@cpe-83-98-47-163.wireline.com.au) |
| 2025-12-12 12:15:05 +0100 | <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 12:13:44 +0100 | <Enrico63> | Whereas rank 2 means that the implementation (i.e. the inner scope) chooses the type variable of the inner forall |
| 2025-12-12 12:12:39 +0100 | <haskellbridge> | <loonycyborg> With rank 1 all variables are set at outer scope and you won't be passing any polymorphic functions. |
| 2025-12-12 12:12:37 +0100 | <Enrico63> | loonycyborg, yeah, I'm also (halfway) there |
| 2025-12-12 12:12:31 +0100 | trickard | (~trickard@cpe-83-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-12 12:12:08 +0100 | <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 12:12:00 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |