Type quantifiers in Haskell functions

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 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 ?


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

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


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.


This is a copy of Chi's comment above, it explains the theoretical part by interpreting functions as logical implications (Curry-Howard correspondence) :

Type quantifers can be swapped with arrows as in logic: the proposition p -> forall a. q(a) p -> forall a. q(a) is equivalent to forall a. p -> q(a) forall a. p -> q(a) provided p does not depend on a . If Haskell had existential types, we would have the isomorphism (forall a. p(a) -> q) ~ ((exists a. p(a)) -> q) . It commutes with products too (forall a. pa, forall a. qa) ~ forall a. (pa, qa) (forall a. pa, forall a. qa) ~ forall a. (pa, qa) . On sums it's trickier.

I also link the specs of RankNTypes. It does enforce the rules of "floating out" type quantifiers and defines the type (forall a. SomeClass a => a) -> Int .

链接地址: http://www.djcxy.com/p/95252.html

上一篇: RxJava2去抖功能在RecyclerView中无法正常工作

下一篇: 在Haskell函数中输入量词