Valid expressions for `using headers`

#1

According to the spec

If an import ends with  `using headers` , resolve the  `headers`  import and use the resolved expression as additional headers supplied to the HTTP request.

It gives the example of

For example, if normalizedRequestHeaders in the above judgment was:

[ { mapKey = "Authorization", mapValue = "token 5199831f4dd3b79e7c5b7e0ebe75d67aa66e79d4" }
]
... then the HTTPS request for https://authority directory file would include the following header line:

Authorization: token 5199831f4dd3b79e7c5b7e0ebe75d67aa66e79d4

However, it doesn’t seem to enumerate what expressions are considered valid to be used as HTTP headers. Some digging around in the Haskell code led me to this:

-- | Given a well-typed (of type `List { header : Text, value Text }` or
-- `List { mapKey : Text, mapValue Text }`) headers expressions in normal form
-- construct the corresponding binary http headers; otherwise return the empty
-- list.
toHeaders :: Expr s a -> [HTTPHeader]
toHeaders (ListLit _ hs) = Data.Foldable.toList (Data.Foldable.fold maybeHeaders)
  where
      maybeHeaders = mapM toHeader hs
toHeaders _ = []

toHeader :: Expr s a -> Maybe HTTPHeader
toHeader (RecordLit m) = do
    TextLit (Chunks [] keyText  ) <-
        Dhall.Map.lookup "header" m <|> Dhall.Map.lookup "mapKey" m
    TextLit (Chunks [] valueText) <-
        Dhall.Map.lookup "value" m <|> Dhall.Map.lookup "mapValue" m
    let keyBytes   = Data.Text.Encoding.encodeUtf8 keyText
    let valueBytes = Data.Text.Encoding.encodeUtf8 valueText
    return (Data.CaseInsensitive.mk keyBytes, valueBytes)
toHeader _ = do
    empty

This should surely be documented in the spec? (Or else it is and I haven’t found it!)

Happy to put together a PR to update the spec with what is documented in the Haskell code if necessary!

#2

It is specified, but only formally, in this judgment:

(Ξ”, parent) Γ— Ξ“β‚€ ⊒ requestHeaders β‡’ resolvedRequestHeaders ⊒ Γ₁
Ρ ⊒ resolvedRequestHeaders : H
H ∈ { List { mapKey : Text, mapValue : Text }, List { header : Text, value : Text } }
resolvedRequestHeaders β‡₯ normalizedRequestHeaders
parent </> https://authority directory file using normalizedRequestHeaders = import
canonicalize(import) = child
referentiallySane(parent, child)
Γ₁(child) = eβ‚€ using responseHeaders
  ; Append normalizedRequestHeaders to the above request's headers
corsCompliant(parent, child, responseHeaders)
(Ξ”, parent, child) Γ— Γ₁ ⊒ eβ‚€ β‡’ e₁ ⊒ Ξ“β‚‚
Ξ΅ ⊒ e₁ : T
──────────────────────────────────────────────────────────────────────────  ; * child βˆ‰ Ξ”
(Ξ”, parent) Γ— Ξ“β‚€ ⊒ https://authority directory file using requestHeaders β‡’ e₁ ⊒ Ξ“β‚‚

Specifically in this line:

H ∈ { List { mapKey : Text, mapValue : Text }, List { header : Text, value : Text } }

In other words, the type can either be List { mapKey : Text, mapValue : Text } or List { header : Text, value : Text } (for backwards compatibility)

#3

Thanks @Gabriel439! Sorry I missed that!

Is the Haskell implementation not more permissive than that? It looks to me like it would allow eg

[ { header = "foo", mapValue = "bar" ]

?

Again, happy to create a PR to fix if I have read it correctly and apologies if not!

#4

@TimWSpence: Yes, that is a bug in the Haskell implementation.

#5

@Gabriel439 Glad to know I’m not going crazy :sweat_smile: I’ll try to knock together a PR tonight to fix it. Thanks for the quick responses and sorry to spam you with messages!

2 Likes