[racket-users] Re: Combining contract checking with normalization?

[Robby Findler]

I have certainly have thought that developing a library along these lines
is a good idea for many years!

Robby

On Sun, Mar 6, 2022 at 9:47 AM Alexis King  wrote:

> Hello,
>
> As a user of the Racket contract system, I sometimes find myself thinking
> about the potential utility of “coercing” or “canonicalizing” contracts. In
> Racket programs, we often idiomatically allow values to be provided to a
> function in a non-canonical form for the sake of convenience. One example
> is the commonly-used path-string? contract, which is morally equivalent
> to using path? but allows the caller to omit an explicit use of
> string->path. Another example is the commonly-used failure-result/c
> contract, which allows the caller to omit wrapping non-procedures in a
> thunk.
>
> While this idiom does make life easier for one party to the contract, it
> ultimately just transfers the burden of canonicalizing the value to the
> other party. This is unfortunate, because it results in a duplication of
> both logic and work:
>
>-
>
>Code to canonicalize the value must be written separately and kept in
>sync with the contract, which is error-prone.
>-
>
>The value ends up being inspected twice: once to determine if it
>satisfies the contract, and a second time to convert it to canonical form.
>
> (In the nomenclature of a popular blog post I wrote a few years ago, these
> contracts are validating, not parsing
> .)
>
> In theory, it is perfectly possible to implement a canonicalizing contract
> using the current contract system. However, such a contract has several
> practical downsides:
>
>-
>
>It is necessarily an impersonator contract, not a chaperone contract.
>This prevents its use in places that demand a chaperone contract, such as
>the *key* argument to hash/c.
>-
>
>It moves actual logic into the contract itself, which means using the
>uncontracted value directly is less convenient. This encourages placing the
>contract boundary close to the value’s definition to create a very small
>contracted region (e.g. via define/contract), even though blame is
>generally more useful when the contract boundary corresponds to a boundary
>between higher-level components (e.g. via contract-out).
>-
>
>There is no way to write such contracts using the combinators provided
>by racket/contract, so they must be implemented via the lower level
>make-contract/build-contract-property API. This can be subtle to use
>correctly, and it makes it unlikely that contract violations made by the
>contract itself will be blamed properly according to the “indy” blame
>semantics used by ->i.
>
> All this is to say that the current contract system clearly discourages
> this use of contracts, which suggests this would be considered an abuse of
> the contract system. Nevertheless, the coupling between validating values
> and converting them to a normal form is so enormously tight that allowing
> them to be specified together remains incredibly compelling. I therefore
> have two questions:
>
>1.
>
>Has this notion of “canonicalizing” contracts been discussed before,
>whether in informal discussions or in literature?
>2.
>
>Is there any existing work that explores what adding such contracts to
>a Racket-style, higher-order contract system in a principled fashion might
>look like?
>
> Thanks in advance,
> Alexis
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAL3TdOMO3%2BEApMTyTmjxhzOZJ%2BUGE5P6h%3Dx1xTqDi7AgB3mggQ%40mail.gmail.com.

[racket-users] Combining contract checking with normalization?

[Alexis King]

Hello,

As a user of the Racket contract system, I sometimes find myself thinking
about the potential utility of “coercing” or “canonicalizing” contracts. In
Racket programs, we often idiomatically allow values to be provided to a
function in a non-canonical form for the sake of convenience. One example
is the commonly-used path-string? contract, which is morally equivalent to
using path? but allows the caller to omit an explicit use of string->path.
Another example is the commonly-used failure-result/c contract, which
allows the caller to omit wrapping non-procedures in a thunk.

While this idiom does make life easier for one party to the contract, it
ultimately just transfers the burden of canonicalizing the value to the
other party. This is unfortunate, because it results in a duplication of
both logic and work:

   -

   Code to canonicalize the value must be written separately and kept in
   sync with the contract, which is error-prone.
   -

   The value ends up being inspected twice: once to determine if it
   satisfies the contract, and a second time to convert it to canonical form.

(In the nomenclature of a popular blog post I wrote a few years ago, these
contracts are validating, not parsing
.)

In theory, it is perfectly possible to implement a canonicalizing contract
using the current contract system. However, such a contract has several
practical downsides:

   -

   It is necessarily an impersonator contract, not a chaperone contract.
   This prevents its use in places that demand a chaperone contract, such as
   the *key* argument to hash/c.
   -

   It moves actual logic into the contract itself, which means using the
   uncontracted value directly is less convenient. This encourages placing the
   contract boundary close to the value’s definition to create a very small
   contracted region (e.g. via define/contract), even though blame is
   generally more useful when the contract boundary corresponds to a boundary
   between higher-level components (e.g. via contract-out).
   -

   There is no way to write such contracts using the combinators provided
   by racket/contract, so they must be implemented via the lower level
   make-contract/build-contract-property API. This can be subtle to use
   correctly, and it makes it unlikely that contract violations made by the
   contract itself will be blamed properly according to the “indy” blame
   semantics used by ->i.

All this is to say that the current contract system clearly discourages
this use of contracts, which suggests this would be considered an abuse of
the contract system. Nevertheless, the coupling between validating values
and converting them to a normal form is so enormously tight that allowing
them to be specified together remains incredibly compelling. I therefore
have two questions:

   1.

   Has this notion of “canonicalizing” contracts been discussed before,
   whether in informal discussions or in literature?
   2.

   Is there any existing work that explores what adding such contracts to a
   Racket-style, higher-order contract system in a principled fashion might
   look like?

Thanks in advance,
Alexis

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAA8dsad%2BZHLQTBK-oa5UZJfV7t33Fk0Q0L5rTG-CBnzMqH3haA%40mail.gmail.com.