Incorrect signature for `extract-field`.

Lazerbeak12345 commented 2 years ago

What version of Racket are you using?

racket-8.6.0.12

What program did you run?

Program A:

#lang typed/racket/base
(require
  (only-in typed/net/url get-pure-port/headers netscape/string->url make-http-connection)
  (only-in typed/net/head extract-field))
(define theUrl (netscape/string->url "https://example.com"))
(define-values (port headers) (get-pure-port/headers theUrl #:connection (make-http-connection)))
(define location (extract-field #"location" headers))
(displayln location)

Program B is the same, but replace the bytestring #"location" with the string "location"

What should have happened?

~~A should run, B should error in the exact way it does.~~

A should have a type error, B should run.

If you got an error message, please include it here.

Error message for A: (should be a type error)

. . extract-field: contract violation
  expected: string field for string header
  given: #"location"
  argument position: 1st
  other arguments...:

Unwanted error for B

. Type Checker: type mismatch
  expected: Bytes
  given: String in: "location"

Lazerbeak12345 commented 2 years ago

Ah. I should also add, this isn't an issue in untyped racket, and that's why I reported it here instead of in the relevant networking package

sorawee commented 2 years ago

I agree that this is a bug in Typed Racket, but I don't follow why program A and B should work the way you expect it to be.

In particular, program A results in the same error when I run in untyped Racket.

The issue, as I understand, is that extract-field can consume either string or bytes for both arguments, but both arguments must agree in the type. That is, either string + string or bytes + bytes, but not bytes + string or string + bytes.

So I think program B (string + string) should be allowed, and program A (bytes + string) should be disallowed.

Lazerbeak12345 commented 2 years ago

Ah, you're right. I don't know why I had that misunderstanding. Program B is the one to be desired.

Lazerbeak12345 commented 2 years ago

Corrected OP

Lazerbeak12345 commented 2 years ago

Here's the offending line:

https://github.com/racket/typed-racket/blob/4165b6baa0c79e7391d990d76d74c483592145c1/typed-racket-more/typed/net/head.rkt#L8

Here's the docs for this function

This signature would be optimal, but it it "cannot be converted into a contract" because it "has two cases of arity 2"

[extract-field (case-> [Bytes Bytes -> (Option Bytes)]
                       [String String -> (Option String)])]

Lazerbeak12345 commented 2 years ago

Further, there are actually string->byte functions and visa-versa available. If we must, we could allow only String or only Bytes, and require manual type conversion.

sorawee commented 2 years ago

You probably want to use the intersection type here?

Lazerbeak12345 commented 2 years ago

If I swap case-> for ∩ then it gets this error instead (On program B)

. Type Checker: Type (∩ (-> Bytes Bytes (U Bytes False)) (-> String String (U False String))) could not be converted to a contract: Intersection type contract contains more than 1 non-flat contract: (∩ (-> Bytes Bytes (U Bytes False)) (-> String String (U False String))) in: (∩ (Bytes Bytes -> (Option Bytes)) (String String -> (Option String)))

Lazerbeak12345 commented 2 years ago

A union type doesn't work either. (Error for program B)

. Type Checker: type mismatch
  expected: Bytes
  given: String in: "location"
. Type Checker: type mismatch
  expected: Bytes
  given: String in: headers
. Type Checker: Summary: 2 errors encountered in:
  "location"
  headers

sorawee commented 2 years ago

Perhaps support only one of them then? Say, string + string.

Btw, if I have to convert this to contract by hand, it probably would be something like:

(->i ([x (or/c string? bytes?)]
      [y (x) (if (string? x) string? bytes?)])
     [result (x y) (or/c #f (if (string? x) string? bytes?))])

Lazerbeak12345 commented 2 years ago

Btw, if I have to convert this to contract by hand, it probably would be something like: ...

yes, that looks correct to me, as a contract.

Perhaps support only one of them then? Say, string + string.

In that case, it really comes down to which you would like to support. The old type signature only supports Bytes as the first argument, so if we did Bytes Bytes it would remain compatible.

Lazerbeak12345 commented 2 years ago

There's a concern I have here.... I was making the changes to prepare for a PR, and I noticed this about the file:

These functions assume the both header and keys are String

empty-header
validate-header
remove-field
insert-field
replace-field
append-headers
standard-message-header
data-lines->data
extract-addresses
assemble-address-field

As we know, extract-field (currently) makes the assumption that the key is always a Bytes

Further, extract-all-fields uses (U String Bytes) for every instance, meaning some would-be-unnecessary checks have to be made on it's output. Arguably this needs to change as well, but I don't think we need to address it.

So it looks like there's three ways to go with extract-field:

Switch to Bytes Bytes -> (Option Bytes), maintaining compatibility with any current code, but not having direct compatibility with other functions provided by this library
Switch to String String -> (Option String), breaking current code, but remaining consistent with the rest of the current typings for the library
Switch to (U String Bytes) (U String Bytes) -> (U String Bytes False) (I don't recommend this, since the two args must be the same, or else face runtime errors)

I'm not "in charge" of typed/racket or of net/head so I'll just have to leave this decision to someone who is. Either way, I'm willing to send the PR once the decision has been made.

Lazerbeak12345 commented 2 years ago

I've sent a PR that should do it - assuming we take the first approach.

racket / typed-racket