type equivalency

[Tom Pledger]

Andrew J Bromage writes:
 | G'day all.
 | 
 | On Wed, Jun 05, 2002 at 10:35:52PM -0500, Jon Cast wrote:
 | 
 | > > One general rule of strongly-typed programming is: A program is type
 | > > correct if it is accepted by my favourite type checker.  A corollary
 | > > is that what you call a type, I reserve the right to call a
 | > > precondition.
 | > 
 | > If I accepted that, I would be un-defining crucial terms.  That would
 | > destroy the potential for discussion here, no?
 | 
 | I think you might have missed the sarcasm. :-)

There's also a serious interpretation of your rule and corollary:
subtyping.  If your favourite type checker supports subtyping, a type
combined with a precondition yields another type.