Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why doesn't forall (RankNTypes usage) apply by default?

Tags:

haskell

ghc

I am not so familiar with forall, but recently read this question: What does the `forall` keyword in Haskell/GHC do?

In one of the answers is this example:

 {-# LANGUAGE RankNTypes #-}
 liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
 liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

The explanation is good and I understand what forall is doing here. But I'm wondering, is there a particular reason why this isn't the default behaviour. Is there ever a time where it would be disadvantageous?

Edit: I mean, is there are a reason why the forall's can't be inserted by default?

like image 471
Peter Hall Avatar asked Apr 12 '12 17:04

Peter Hall


2 Answers

Well, it's not part of the Haskell 2010 standard, so it's not on by default, and is offered as a language extension instead. As for why it's not in the standard, rank-n types are quite a bit harder to implement than the plain rank-1 types standard Haskell has; they're also not needed all that frequently, so the Committee likely decided not to bother with them for reasons of language and implementation simplicity.

Of course, that doesn't mean rank-n types aren't useful; they are, very much so, and without them we wouldn't have valuable tools like the ST monad (which offers efficient, local mutable state — like IO where all you can do is use IORefs). But they do add quite a bit of complexity to the language, and can cause strange behaviour when applying seemingly benign code transformations. For instance, some rank-n type checkers will allow runST (do { ... }) but reject runST $ do { ... }, even though the two expressions are always equivalent without rank-n types. See this SO question for an example of the unexpected (and sometimes annoying) behaviour it can cause.

If, like sepp2k asks, you're instead asking why forall has to be explicitly added to type signatures to get the increased generality, the problem is that (forall x. x -> f x) -> (a, b) -> (f a, f b) is actually a more restrictive type than (x -> f x) -> (a, b) -> (f a, f b). With the latter, you can pass in any function of the form x -> f x (for any f and x), but with the former, the function you pass in must work for all x. So, for instance, a function of type String -> IO String would be a permissible argument to the second function, but not the first; it'd have to have the type a -> IO a instead. It would be pretty confusing if the latter was automatically transformed into the former! They're two very different types.

It might make more sense with the implicit foralls made explicit:

forall f x a b. (x -> f x)           -> (a, b) -> (f a, f b)
forall f a b.   (forall x. x -> f x) -> (a, b) -> (f a, f b)
like image 92
ehird Avatar answered Nov 10 '22 21:11

ehird


I suspect that higher rank types aren't enabled by default because they make type inference undecidable. This is also why, even with the extension enabled, you need to use the forall keyword to get a higher-rank type - GHC assumes that all types are rank-1 unless explicitly told otherwise in order to infer as much type information as possible.

Put another way, there's no general way to infer a higher-rank type (forall x. x -> f x) -> (a,b) -> (f a, f b), so the only way to get that type is by an explicit type signature.

Edit: per Vitus's comments above, rank-2 type inference is decidable, but higher-rank polymorphism isn't. So this type signature is technically inferrable (although the algorithm is more complex). Whether the extra complexity of enabling rank-2 polymorphic type inference is worthwhile is debatable...

like image 24
John L Avatar answered Nov 10 '22 21:11

John L