3

I don't understand why it is so, referring to : What is the purpose of Rank2Types? -> @dfeuer explanation:

... Requiring an argument to be polymorphic doesn't just allow it to be used with multiple types; it also restricts what that function can do with its argument(s) and how it can produce its result ...

f :: (forall a . [a] -> a) -> IO ()

... In fact, no function returning an element not in the list it is given will typecheck

In any explanation of rank-N types I haven't see this effect (or benefit) described, much of the time it was the story about letting the callee choose the type etc... that is clear for me and easy to grasp but I don't see by which virtue (only of extending the rank) we can control/restrict the function domain (and co-domain)...

if somebody could give a deeper insigth of the rankN mechanism involved here. thx

Noughtmare
  • 9,410
  • 1
  • 12
  • 38
user3680029
  • 179
  • 8
  • `f` must be given a functional argument of type `g :: [a] -> a`, which is short for `forall a. [a] -> a`. So if `g` returns, it must return a value of type `a`, and it knows nothing about `a` because `a` is a type parameter. Can `g` produce a value of type `a` that is *not* from the input list? Another example: `h :: (forall a. a -> a -> a) -> IO ()`. Can the argument of `h` produce a result that is *not* one of its two arguments? (And therefore, which functions are valid arguments to `h`?) – Jon Purdy Sep 08 '21 at 22:39

1 Answers1

7

Just think about it in terms of polymorphic functions you declare on the top-level. A function with the signature like

foo :: [Int] -> Int

has lots of possible implementations like

foo = sum

foo = length

foo _ = 39

but none of these are legal if the signature were

foo :: [a] -> a

because then you can't give an integer as the result – you must provide a result of whatever type the caller demands. So the implementation is much more restricted: the result must come from the input list, because that's the only place you know the elements have type a no matter what the caller actually instantiates this to. Only something like

foo = head

will work then.

Your RankN signature requires its argument to be such a polymorphic function, i.e. the argument can't be a [Int] -> Int but only the more restrictive [a] -> a.

leftaroundabout
  • 117,950
  • 5
  • 174
  • 319
  • thx for your explanation the more I think of it the more I suspect that the list (i.e a container) has to do with it, and make f so restricted and limited (specialized). If we have f :: (forall a . a -> a), with something like "map f [BigEnemy, MediumEnemy, PunyEnemy]" we could without problem sneak an f that could yield a 'BestAlly' (so sthg outside the provided list ) because f will be specialized to Country -> Country – user3680029 Sep 03 '21 at 19:55
  • 2
    N...no, I don't think you've got that right. It doesn't really have anything to do with lists or whatever. – leftaroundabout Sep 03 '21 at 21:44
  • So may be another way f is 'blind' to the outside type definitions it doesn't matter what types are inside the list Country, Planet, Int types f just have to give back something existing in the list even if somewhere else in the program the given type has a much broader def. – user3680029 Sep 04 '21 at 07:31
  • 2
    @user3680029 we have `f :: (forall a . [a] -> a) -> IO ()`. its first argument is referred to as `foo` in this answer. its type is `foo :: [a] -> a` (the `forall` is implied). given a list `[BigEnemy, MediumEnemy, PunyEnemy]`, `foo` gets to do its work. what could that possibly be? when we wrote its definitions, we couldn't use the knowledge about the type of `BigEnemy`, since `foo` must work for all `a`s. some other call could be made as `foo [1,2,3,4]`. the same definition must be able to do its work with that argument as well. – Will Ness Sep 04 '21 at 16:53
  • @user3680029 so `f` could be defined as (in pseudocode) `f foo = if random_bit == 0 then print (foo "123") else print (foo [1.1,2.2,3.3])`. – Will Ness Sep 04 '21 at 16:57
  • @Will Ness, quote " ..... when we wrote its definitions, we **couldn't use the knowledge about the type** of BigEnemy, since foo must work for all `a`" + leftaroundabout "...the result must come from the input list, because that's the only place you know the elements have type a..." starts to work in my mind, I see the logic behind, for f the only way to be non-specific to `a` (work for any a) and along the way produce an `a` is to take one from the "container" (by definition this will always be true). Lot of reasoning just for a rand increase ... – user3680029 Sep 05 '21 at 09:05
  • rank increase (not rand), okay so now it's time to tackle the ST monad – user3680029 Sep 05 '21 at 09:12