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

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 <eric.n.dobson at gmail.com> 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" <robby at eecs.northwestern.edu>
> 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
>> <jensaxel at soegaard.net> 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