What am I doing wrong with this meant-to-be-trivial higher rank polymorphism exercise?
ghc, haskell
Solution
Let's think about what the type of `rank2` means.
rank2 :: (forall a. [a]) -> Bool
rank2 x = null x
The first argument to `rank2` needs to be something of type `forall a. [a]`. The `forall` being outermost here means that whoever gets such a value can pick their choice of `a`. Think of it like taking a type as an extra argument.
So, in order to give something as an argument to `rank2`, it needs to be a list whose elements can be of any type that the internal implementation of `rank2` might want. Since there's no way to conjure up values of such an arbitrary type, the only possible inputs are `[]` or lists containing `undefined`.
Contrast this with `rank1b`:
rank1b :: forall a. [a] -> Bool
rank1b x = null x
Here the `forall` is already outermost, so whoever uses `rank1b` itself gets to pick the type.
A variation that would work would be something like this:
rank2b :: (forall a. Num a => [a]) -> Bool
rank2b x = null x
Now you can pass it a list of numeric literals, which are polymorphic over all `Num` instances. Another alternative would be something like this:
rank2c :: (forall a. [a -> a]) -> Bool
rank2c x = null x
This works because you can indeed conjure up values of type `forall a. a -> a`, specifically the function `id`.
Problem
Over a year ago, I asked the question How to use a proxy in Haskell, and since then I have a small amount of use of the RankNTypes GHC extension. The trouble is every time I try to work with it, I end up with bizarre error messages and hacking around the code until they go away. Or else I give up. Obviously I don't really understand higher rank polymorphism in Haskell. To try to resolve that, I decided to get right down to the simplest examples I could, test all my assumptions and see if I could get myself a Eureka moment. First assumption - the reason higher rank polymorphism isn't a standard Haskell 98 (or 2010?) feature is that, provided you accept some not-that-obvious restrictions that a lot of programmers wouldn't even notice, it isn't needed. I can define rank 1 and rank 2 polymorphic functions that are, at first sight, equivalent. If I load them into GHCi and call them with the same parameters, they'll give the same results. So - simple example functions... ``` {-# LANGUAGE RankNTypes #-} rank0 :: [Int] -> Bool rank0 x = null x rank1a :: [a] -> Bool rank1a x = null x rank1b :: forall a. [a] -> Bool rank1b x = null x rank2 :: (forall a. [a]) -> Bool rank2 x = null x ``` and a GHCi session... ``` GHCi, version 7.4.2: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Prelude> :load example01 [1 of 1] Compiling Main ( example01.hs, interpreted ) Ok, modules loaded: Main. *Main> ``` No errors so far - good start. Next, test each function with an empty list parameter... ``` *Main> rank0 [] True *Main> rank1a [] True *Main> rank1b [] True *Main> rank2 [] True *Main> ``` To be honest, I was a little surprised the `rank1a` and `rank1b` functions worked in this case. The list doesn't know what type elements it contains, the functions don't know either, yet surely the type must be decided to make that call? I was expecting to need to provide an explicit signature somewhere. That's not really the issue ATM though, and the results seem promising. Next up, non-empty lists... ``` *Main> rank0 [1,2,3] False *Main> rank1a [1,2,3] False *Main> rank1b [1,2,3] False *Main> rank2 [1,2,3] <interactive>:10:8: No instance for (Num a) arising from the literal `1' In the expression: 1 In the first argument of `rank2', namely `[1, 2, 3]' In the expression: rank2 [1, 2, 3] *Main> ``` Oh dear - it seems like the rank 2 version doesn't like it when the parameter knows a bit more about it's type. Still, maybe the issue is just that the literals `1` etc are polymorphic... ``` *Main> rank2 ([1,2,3] :: [Int]) <interactive>:11:8: Couldn't match type `a' with `Int' `a' is a rigid type variable bound by a type expected by the context: [a] at <interactive>:11:1 Expected type: [a] Actual type: [Int] In the first argument of `rank2', namely `([1, 2, 3] :: [Int])' In the expression: rank2 ([1, 2, 3] :: [Int]) *Main> ``` The error is different, but it still didn't work and I still don't understand these error messages. Messing around with various theories, one idea I had was that maybe I need to tell GHC to "forget" some of the static type of the list. On that theory, I tried various things including... ``` *Main> [1,2,3] :: [a] <interactive>:12:2: No instance for (Num a1) arising from the literal `1' In the expression: 1 In the expression: [1, 2, 3] :: [a] In an equation for `it': it = [1, 2, 3] :: [a] *Main> ``` OK, GHCi doesn't know what I'm talking about. In case GHCi just needed to know exactly which type to forget, I also tried... ``` *Main> ([1,2,3] :: [Int]) :: [a] <interactive>:15:2: Couldn't match type `a1' with `Int' `a1' is a rigid type variable bound by an expression type signature: [a1] at <interactive>:15:1 Expected type: [a] Actual type: [Int] In the expression: ([1, 2, 3] :: [Int]) :: [a] In an equation for `it': it = ([1, 2, 3] :: [Int]) :: [a] *Main> ``` So much for my hopes of getting an error to the effect that GHCi doesn't know how to `show` a value with a forgotten type. I don't know how to construct a list with a "forgotten" static type and I'm not even sure that makes sense. At this point I'm not trying to do anything useful with higher rank polymorphism. The point here is simply to be able to call the `rank2` function with a non-empty list, and to understand why it's not working exactly the same as the other functions. I want to carry on figuring this out step by step myself, but right now I'm just completely stuck.