I've seen the first-order case come up a number of times, but not the higher-order one, so it may be best to be conservative and start there to see how it goes.
Robby On Sat, Nov 17, 2012 at 2:09 PM, Eric Dobson <[email protected]> wrote: > Its even simpler than that because the cases in case-> are ordered. There > are some intricacies when the first order checks of non flat contracts > overlap, but with non overlapping first order checks for higher order > contracts or only flat contracts it should be doable. I don't have a lot of > time for TR hacking currently, but if a bug is filed I may get to it at some > point. > > On Nov 17, 2012 11:33 AM, "Robby Findler" <[email protected]> > wrote: >> >> 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 ____________________ Racket Users list: http://lists.racket-lang.org/users
