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

[Jens Axel Søgaard]

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

[Robby Findler]

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.)

[Eric Dobson]

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.

[Robby Findler]

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

[Neil Toronto]

On 11/17/2012 12:18 PM, Jens Axel Søgaard 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?

Vincent and I worked this out at the hackathon. There's now a very
general but currently undocumented solution.

Most of the special functions have types that can't be converted to
contracts. For example, the gamma function has the type

(: gamma (case-> (One -> One)
(Integer -> Positive-Integer)
(Flonum -> Flonum)
(Real -> (U Positive-Integer Flonum))))

This could in principle be converted, but there are higher-order
`case->' types in the math library that couldn't without running some
serious theorem-proving. There probably always will be types that can't
be converted to contracts, such types for functions that accept
predicates (e.g. (Any -> Boolean : Real)).

I swear I will document this soon (it's on my TODO list!), but here's
the general solution:

(require typed/untyped-utils)

(require/untyped-contract
"private/functions/gamma.rkt"
[gamma (Real -> Real)])

(provide gamma)

A Typed Racket module that imports `math/special-functions' will see
gamma's original type, but its contract for untyped code is converted
from the stated type (Real -> Real).

This should work for any type that TR can prove is a subtype of the
original. Currently, `require/untyped-contract' can only be used in
untyped Racket.

FWIW, this solution is only possible now that Racket has submodules.

The best place to use this is in "math/number-theory.rkt"... which I see
is already using it for factorial and friends. You're all set.

Neil ⊥

[Jens Axel Søgaard]

2012/11/17 Eric Dobson <eric.n...@gmail.com>:

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

I have filed a bug report.

/Jens Axel

[Robby Findler]

Wouldn't it be better to use the dependent contract (when that works)?
As an import to TR it definitely seems better, since it wouldn't be
checking the right thing otherwise. (As an export from TR, I guess it
doesn't matter.)

Robby

[Jens Axel Søgaard]

2012/11/17 Neil Toronto <neil.t...@gmail.com>:

> The best place to use this is in "math/number-theory.rkt"... which I see is
> already using it for factorial and friends. You're all set.

Worked like a charm.

Thanks,
Jens Axel

[Neil Toronto]

Yes. More automated is always better, for saving effort and reducing
redundant annotations.

I see this in three ways:

* A stop-gap solution

* A last resort for types that can't be converted without importing Coq

* A way to squeeze better performance out of the typed/untyped boundary
when it really counts

As an example of the last, `gamma' is exported to untyped code with the
type (Real -> Real), when it could have the more specific type (Real ->
(U Positive-Integer Flonum)), which has a slower contract check.

I don't know if performance "really matters" here, but I figured I'd
consider it since I was already re-annotating.

Neil ⊥