[racket] A type that can't be converted to a contract
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20121117/90f43eee/attachment.html>