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?
John
smime.p7s
Description: S/MIME cryptographic signature
_________________________ Racket Developers list: http://lists.racket-lang.org/dev
