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 .
上一篇: RxJava2去抖功能在RecyclerView中无法正常工作
下一篇: 在Haskell函数中输入量词