haskell - What am I doing wrong with this meant-to-be-trivial higher rank polymorphism exercise? -

over year ago, asked question how use proxy in haskell, , since have small amount of use of rankntypes ghc extension. trouble every time try work it, end bizarre error messages , hacking around code until go away. or else give up.

obviously don't understand higher rank polymorphism in haskell. try resolve that, decided right down simplest examples could, test assumptions , see if myself eureka moment.

first assumption - reason higher rank polymorphism isn't standard haskell 98 (or 2010?) feature that, provided accept not-that-obvious restrictions lot of programmers wouldn't notice, isn't needed. can define rank 1 , rank 2 polymorphic functions are, @ first sight, equivalent. if load them ghci , call them same parameters, they'll give 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 ghci session...

ghci, version 7.4.2: http://www.haskell.org/ghc/  :? 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 far - start. next, test each function empty list parameter...

*main> rank0 [] true *main> rank1a [] true *main> rank1b [] true *main> rank2 [] true *main> 

to honest, little surprised rank1a , rank1b functions worked in case. list doesn't know type elements contains, functions don't know either, yet surely type must decided make call? expecting need provide explicit signature somewhere.

that's not issue atm though, , 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 (num a)       arising literal `1'     in expression: 1     in first argument of `rank2', namely `[1, 2, 3]'     in expression: rank2 [1, 2, 3] *main> 

oh dear - seems rank 2 version doesn't when parameter knows bit more it's type. still, maybe issue literals 1 etc polymorphic...

*main> rank2 ([1,2,3] :: [int])  <interactive>:11:8:     couldn't match type `a' `int'       `a' rigid type variable bound           type expected context: [a] @ <interactive>:11:1     expected type: [a]       actual type: [int]     in first argument of `rank2', namely `([1, 2, 3] :: [int])'     in expression: rank2 ([1, 2, 3] :: [int]) *main> 

the error different, still didn't work , still don't understand these error messages.

messing around various theories, 1 idea had maybe need tell ghc "forget" of static type of list. on theory, tried various things including...

*main> [1,2,3] :: [a]  <interactive>:12:2:     no instance (num a1)       arising literal `1'     in expression: 1     in expression: [1, 2, 3] :: [a]     in equation `it': = [1, 2, 3] :: [a] *main> 

ok, ghci doesn't know i'm talking about. in case ghci needed know type forget, tried...

*main> ([1,2,3] :: [int]) :: [a]  <interactive>:15:2:     couldn't match type `a1' `int'       `a1' rigid type variable bound            expression type signature: [a1] @ <interactive>:15:1     expected type: [a]       actual type: [int]     in expression: ([1, 2, 3] :: [int]) :: [a]     in equation `it': = ([1, 2, 3] :: [int]) :: [a] *main> 

so hopes of getting error effect ghci doesn't know how show value forgotten type. don't know how construct list "forgotten" static type , i'm not sure makes sense.

at point i'm not trying useful higher rank polymorphism. point here able call rank2 function non-empty list, , understand why it's not working same other functions. want carry on figuring out step step myself, right i'm stuck.

let's think type of rank2 means.

rank2 :: (forall a. [a]) -> bool rank2 x = null x 

the first argument rank2 needs of type forall a. [a]. forall being outermost here means whoever gets such value can pick choice of a. think of taking type argument.

so, in order give argument rank2, needs list elements can of any type internal implementation of rank2 might want. since there's no way conjure values of such arbitrary type, possible inputs [] or lists containing undefined.

contrast rank1b:

rank1b :: forall a. [a] -> bool rank1b x = null x 

here forall outermost, whoever uses rank1b gets pick type.

a variation would work this:

rank2b :: (forall a. num => [a]) -> bool rank2b x = null x 

now can pass list of numeric literals, polymorphic on num instances. alternative this:

rank2c :: (forall a. [a -> a]) -> bool rank2c x = null x 

this works because can indeed conjure values of type forall a. -> a, function id.