[TYPES] Free theorems for maps of higher rank and polarized systems?

[Ahn, Ki Yung]

I have some questions on free theorems for maps, which most people may 
believe, but having difficulty to cite where actual proof is written 
down, or an instance of a more general theorem, or whether it has ever 
been actually proved. I'd greatly appreciate pointers to related papers.


Question 1. Proper citation for free theorems for fmap
   (fmap is Haskell-ish term for generic maps) for rank 1
   (* -> *) and rank 2 (such as (* -> *) -> (* -> *))?

Wadler's "Theorems for free!" papers discusses map for lists.

But everyone seem to believe it holds for arbitrary structure of rank 1, 
that is, F : * -> *. We can formalize this idea in Fw as follows:

If there exists
   fmap : forall (f:*->*)(a:*)(b:*). (a -> b) -> f a -> f b
then (1) any such fmap satisfy the expected property of fmap, i.e.,
   fmap id = id
   fmap f . fmap f = fmap g
and  (2) also such fmap is unique.

Similar statement could be made for rank 2 version of this.
These generic maps of also called as monotonicity witness.

Papers on monotonicity that I've seen doesn't exactly proves (1) but 
since they use monotonicity witness to encode iterations or folds, I 
think it may be considered as indirect proof of the properties in (1). 
But it would be nice to know if you have seen proofs of statements in 
the form above as (1), and also for uniqeness (2), I'd appreciate the 
pointers to such literature.

Matthes' CSL'98 paper discusses that monotonicity witness for rank 2 has 
not been proved yet and it is an open question. Has this been proved 
afterwards for rank 2 or higher?



Question 2. Are fully(?) positively polarized type constructors monotone 
in general?

We can track polarities of the use of type constructor variables in Fw 
and label and have extra annotation +,-, or 0 (means it can be used in 
both + and - positions) at kinds (e.g., +* -> *, -* -> *, 0* -> *). 
Systems like Fixw in CSL 04 paper by Abel and others is an example of a 
polarized system. Then, in such systems, I conjecture that type 
constructors of kinds +* -> *, +(+* -> *) -> (+* ->*) that have + 
polarities everywhere must always have monotonicity witness.

This is a slightly more general version of strictly positivity because 
it considers negative of negative position to be positive. If you have 
seen anyone proved this, again, I would very much appreciate pointers to 
those materials.

Thanks in advance.

Ki Yung