Type quantifiers in Haskell functions

Question

Suppose I have two Haskell functions of the following types, with ExplicitForAll activated,

f :: forall a. (a -> Int)
g :: forall a. (Int -> a)

It seems to me that the type of g is isomorphic to Int -> (forall a. a), because for example the type of g(2) is forall a. a.

However, the type of f doesn't look isomorphic to (forall a. a) -> Int. f is a polymorphic function, it knows what to compute on each input type a, in mathematics I guess it would rather be a family of functions ; but I don't think it can handle a single argument that has all types.

Is it a rule of typed lambda calculus that type quantifiers distribute on functions target types, but not on functions source types ?

Does the type (forall a. a) -> Int exist in Haskell, possibly restrained to a type class (forall a. SomeClass a => a) -> Int ? Is it useful ?

Answer 1

weird :: (forall a. a) -> Int is unnecessarily specific.

undefined is the only value that has type forall a. a, so the definiton would have to be weird _ = someInteger, which is just a more restrictive version of const.

Answer 2

A ∀ a . is basically just an extra implicit argument, or rather, a specification of how type-constraints pertaining to that argument should be handled. For instance,

f :: ∀ a . Show a => (a -> Int)
g :: ∀ a . Show a => (Int -> a)

are in essence functions of two arguments,

f' :: ShowDictionary a -> a -> Int
g' :: ShowDictionary a -> Int -> a

or even dumber,

type GenericReference = Ptr Foreign.C.Types.Void -- this doesn't actually exist

f'' :: (GenericReference -> String) -> GenericReference -> Int
g'' :: (GenericReference -> String) -> Int -> GenericReference

Now, these are just monomorphic (or weak-dynamic typed) functions. We can clearly use flip on them to obtain

f''' :: GenericReference -> (GenericReference -> String) -> Int
g''' :: Int -> (GenericReference -> String) -> GenericReference

The latter can simply be evaluated partially with any Int argument, hence g is indeed equivalent to γ :: Int -> (∀ a . Show a => Int -> a).

With f''', applying it to some void-pointered argument would be a recipe to disaster, since there's no way for the type system to ensure that the actually passed type matches the one the Show function is prepared to handle.