I have the following contract on next-prime :
(: next-prime : (case-> (N -> N) (Z -> Z)) )
It says that for all primes p, positive or negative, (next-prime p)
will be an integer.
Furthermore if p is a natural number, then (next-prime p) will also be
a natural number.
This type can't be converted to a contract:
Type Checker: The type of next-prime cannot be converted to a
contract in: (next-prime 4)
My understanding is that a since N is a subset of Z a predicate can't
determine whether
which case to use. Is there an alternative construct, that I can use
in order to get
a contract?
My temporary solution is to provide untyped-next-prime
(: untyped-next-prime : Z -> Z)
(define (untyped-next-prime z)
(next-prime z))
whose type can be converted to a contract.
See details in:
https://github.com/plt/racket/blob/master/collects/math/private/number-theory/number-theory.rkt
--
Jens Axel Søgaard
____________________
Racket Users list:
http://lists.racket-lang.org/users
