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 ⊥
On 11/17/2012 01:27 PM, Robby Findler wrote:
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
On Sat, Nov 17, 2012 at 2:18 PM, Neil Toronto <[email protected]> wrote:
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 ⊥
____________________
Racket Users list:
http://lists.racket-lang.org/users
____________________
Racket Users list:
http://lists.racket-lang.org/users
