# [racket-dev] typed racket non-monotonic in scary way?

On 09/07/2012 06:42 PM, John Clements wrote:
>* I was trying to write a function on natural numbers today, and came up with an example that scares me all to bits. This program:
*>*
*>* #lang typed/racket
*>*
*>* (: int->nat (Natural -> Natural))
*>* (define (int->nat n)
*>* (cond [(<= n 0) 13]
*>* [else (- n 1)]))
*>*
*>* Does not type-check, because (- n 1) has type Integer rather than Natural. Well, too bad, but sort of okay. But then:
*>*
*>* #lang typed/racket
*>*
*>* (: int->nat (Integer -> Natural))
*>* (define (int->nat n)
*>* (cond [(<= n 0) 13]
*>* [else (- n 1)]))
*>*
*>* *does* typecheck. AIIEE! As far as I can tell, Integer is a supertype of Natural, so I would expect that things that typecheck with Integer inputs should also typecheck with Natural inputs.
*>*
*>* Please please tell me this is a bug? I can imagine a world where it's not a bug, but the difficulty of using the type system would skyrocket if you have to consider *widening* types as well as narrowing them to get things to work.
*>*
*>* No?
*
I'd report it. The filters on the types of functions like `<=' are
axioms in the type system. Adding such axioms in a way that invalidates
the type system's properties should be regarded as an error.
FWIW, the filters on predicates are more likely to be correct because
their huge `case->' types are less huge. For example, the filter for
`positive?' doesn't seem to make the type system non-monotone:
(: int->nat (Natural -> Natural))
(define (int->nat n)
(cond [(not (positive? n)) 13]
[else (- n 1)]))
This typechecks just fine.
There should be a way to catch this kind of thing with randomized
testing, or (less likely) by analyzing the `case->' types.
Neil ⊥