[racket] A type that can't be converted to a contract

From: Jens Axel Søgaard (jensaxel at soegaard.net)
Date: Sat Nov 17 14:18:44 EST 2012

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


Posted on the users mailing list.