[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
