This has come up enough times that maybe TR should convert contracts of the form:
(case-> (-> <flat> ...) (-> <flat> ...)) into a dependent contract that checks the two 'flat' things? (I guess you'd have to have an ordering on types in case they overlap, but I presume you have this already.) On Sat, Nov 17, 2012 at 1:18 PM, Jens Axel Søgaard <[email protected]> wrote: > 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 ____________________ Racket Users list: http://lists.racket-lang.org/users
