higher rank types are killed?

[Ingo60]

Take the following example, which serves to demonstrate higher rank functions:

foo :: (forall a.[a]->[a]) -> ([Int], [Bool])
foo f = (f [1,2], f [true,false])

This code checks just fine in the compiler. However, in the online REPL it gives nonsensical messages:

frege> bar :: (forall b.[b]->[b]) -> ([Int], [Bool]); bar f = (f [0x1,0x2], [true, false]) 
 4: Type [b]->[b]
 inferred from  bar is not as polymorphic as
 expected type  forall b.[b] -> [b]

I also tried this with :{, :}, no difference. An interesting aspect is that the alternate definition does work:

frege> foo (f::forall a.[a]->[a]) = (f [1,2], f [true,false])
frege> foo reverse
([2, 1], [false, true])

[mmhelloworld]

This is due to REPL trying to assign the script to a variable to identify whether the script is an expression. The same code outside REPL in a normal Frege program also fails. For example, the following code fails with the same compilation error:

module HelloWorld where

bar :: (forall b.[b]->[b]) -> ([Int], [Bool]); bar f = (f [0x1,0x2], [true, false])
foo = bar

REPL runs the lexer phase with that assignment to see if the script is an expression. In this case it succeeds and then at the later point it fails to compile as in the above program. If the REPL can identify that as not an expression or if the above regular Frege program results in successful compilation, it will succeed. For example, In the following code in REPL, with the import in front, it is not identified as an expression so the assignment won't happen and it succeeds.

frege> import Data.List;bar :: (forall b.[b]->[b]) -> ([Int], [Bool]); bar f = (f [0x1,0x2], [true, false])
frege> bar id
([1, 2], [true, false])

[Ingo60]

I have found some bugs in the handling of higher rank typed code, see the latest Issues in frege. Maybe we can delay this one until they're fixed, as it is not that important.

We might also want to treat foo = bar specially, because in the eta-expanded form this is indeed a type error when bar is higher rank and there is no annotation available for foo.

[mmhelloworld]

We might also want to treat foo = bar specially, because in the eta-expanded form this is indeed a type error

My type-fu is at very much beginner level. How is that a type error? If you can point me to some papers, that would also be great. By the way, the same (foo = bar) works fine in Haskell.

[Ingo60]

I guess it is because they actually do treat it specially. (I'll ask this on SO next time.) Without considering special cases, HM type inference cannot infer a higher rank type for anything. Hence, the type inferred for foo will by necessity be not polymorphic enough.

The following also results in type error in Haskell (GHCi 7.4.2, with :set -XRankNTypes):

foo f = bar f

The point is that the argument f can not get the polymorphic type needed through type inference. So even in Haskell one would need a type signature for foo to make it check.

[mmhelloworld]

I got it now, thanks! So now we need to figure out how to resolve this as a declaration instead of assigning to a variable which lexer and parser seem to agree and then getting treated as an expression that later on fails with typechecker.

[Ingo60]

I'll post a fix in a few minutes that enhances typechecking in the case where the left hand side is a single identifier and the right hand side is a partial application of a higher rank function up to, but excluding, the polymorphic function argument or just that function.

Hence if we have

 bar :: Bool -> (forall.[a]->[a]) -> [b] -> [b]

the following is ok:

 foo = bar       -- foo :: Bool -> (forall.[a]->[a]) -> [b] -> [b]
 baz = bar true  -- baz :: (forall.[a]->[a]) -> [b] -> [b]

while this is wrong:

wrong f = bar true f

This is just like it works in GHC, according to my tests.

[Ingo60]

P.S. one can, of course, also pass the function argument, but it must not contain a lambda/case-bound name.

Hence:

good = baz true reverse

but, of course, good is then not higher rank itself.