Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Feature Request] Ellipses for Parametric Contracts #4979

Open
Tuplanolla opened this issue Apr 22, 2024 · 2 comments
Open

[Feature Request] Ellipses for Parametric Contracts #4979

Tuplanolla opened this issue Apr 22, 2024 · 2 comments

Comments

@Tuplanolla
Copy link

I would like to endow apply and other such procedures
with more precise contracts, as seen below.

(define/contract apply/contract
  (parametric->/c (src ... dst)
    (-> (-> src ... dst)
        (list/c src ...)
        dst))
  apply)

Alas, I cannot, because parametric->/c does not support ... or
any other mechanism for binding arbitrarily many type parameters.
It seems that I have to ignore the domain completely, as shown below.

(define/contract apply/contract
  (parametric->/c (dst)
    (-> (unconstrained-domain-> dst)
        list?
        dst))
  apply)

Is this the best I can do right now?
Could support for ellipses be added in the future?

@usaoc
Copy link
Contributor

usaoc commented Apr 25, 2024

It seems to me that this pseudo-contract has two problems:

  1. The ellipsis ... actually identifies
    • the number of arguments the procedure accepts, and
    • the number of elements in the list;
  2. (list/c src ...) cannot make sense (remember that list/c is nothing more than a procedure).

Put these together, it doesn’t seem possible to make sense of what the ellipsis ... means. What exactly is the pseudo-contract trying to express, anyway? That if we have a list with n elements, then we should wrap those elements in opaque structs (negative position), and unwrap them when they are supplied to the procedure (positive position), as well as checking that the procedure accepts n arguments? If arity checking is all you need, then I think doing that alone is fine, otherwise you’re checking in extra that apply is, well, applying.

The short answer is that contracts are not types, that’s it.

@usaoc
Copy link
Contributor

usaoc commented Apr 25, 2024

Just for reference, I think this issue is asking for an equivalent of this Typed Racket program in terms of contracts:

#lang typed/racket/base
(: my-apply (All (t s ...)
              ((s ... -> t) (List s ...) -> t)))
(define (my-apply proc args)
  (apply proc args))

(my-apply + (list 1 2 3))

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants