[racket] Typed racket puzzle (ii)

From: Anthony Cowley (acowley at seas.upenn.edu)
Date: Wed Aug 17 09:40:55 EDT 2011

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

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."


Posted on the users mailing list.