[racket] Typed racket puzzle (ii)

On Wed, Aug 17, 2011 at 8:12 AM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
> Here's how to see why you need that. To say that (A -> B) is a subtype
> of (C -> D), you're saying that you can use (A -> B) anywhere you need
> (C -> D).  But some program that expects a (C -> D) function might
> pass it a C, of course, so your new replacement function must accept
> all of the Cs.  Therefore, A needs to accept all of the Cs, which
> means that A must be a subtype of C.

Contravariance strikes again! A typo concludes a good explanation: C
must be a subtype of A.

C <: A      B <: D
-------------------------
A -> B <: C -> D

Norman, one resource on this topic with an ML flavor is
<http://www.cis.upenn.edu/~bcpierce/sf/Subtyping.html>

Writing the natural deduction rule and staring at it every minute you
talk about contravariance is de rigueur.

Jon Postel summed up contravariance by thinking about HTML: "Be
liberal in what you accept, and conservative in what you send."

Anthony