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

 From: Eric Dobson (eric.n.dobson at gmail.com) Date: Sat Nov 17 15:09:02 EST 2012 Previous message: [racket] A type that can't be converted to a contract Next message: [racket] A type that can't be converted to a contract Messages sorted by: [date] [thread] [subject] [author]

```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>
```

 Posted on the users mailing list. Previous message: [racket] A type that can't be converted to a contract Next message: [racket] A type that can't be converted to a contract Messages sorted by: [date] [thread] [subject] [author]