Re: better error messages through assertions

[Philip McGrath]

Hi,

On Monday, February 28, 2022 7:59:02 AM EST Ludovic Courtès wrote:
> Hi!
> 
> Ricardo Wurmus <rekado@elephly.net> skribis:
> > Philip McGrath <philip@philipmcgrath.com> writes:
> >> As a Racketeer, I think you're half way to reinventing contracts.
> > 
> > Yes, I was in fact thinking of contracts, but shied away from mentioning
> > them :)  The reason is that I think we can cover a lot of distance with
> > just a few simple assertions to avoid plowing ahead on bad arguments.
> 
> I’d very much like to have contracts.
> 
> For record types, we have “sanitizers” right now, which we could use to
> insert procedural type checks.  It wouldn’t be as nice as proper
> declarative contracts though, unless we arrange to make them look like
> contracts.
> 

I'm going to try to sketch what I think is a minimal API for contracts.

Racket's state-of-the-art contract system has many features and nuances. I *do
not* think anyone should try to implement them all in one fell swoop. I'm
hoping there's a way to implement your simple assertions with only a modest
amount of overhead that will provide the right base on which to grow the rest
of a contract system. In the short term, the advantage over:

>     (assert-type (listof service?) services
>                  "SERVICES must be a list of <service> values.")

is that you don't have to write error messages by hand.

You need two types of values:

 1. Contracts, recognized by `contract?`; and
 2. Blame objects, recognized by `blame?`.

In simplest terms, a blame object holds context information for error
reporting. Ultimately, it is used to raise an exception with
`raise-blame-error`[1]: this can support e.g. substituting "expected"/"given"
with "promised"/"produced" in error messages based on the context. A contract
combinator will typically give its sub-contract a blame object extended using
`blame-add-context`[2].

The primitive operation on a contract is `get/build-late-neg-projection`[3]:
by skipping the decades experimenting with other APIs that turned out to
perform less well, you have the opportunity to give this function a better
name. In pseudo-code, `get/build-late-neg-projection` has the contract:

    (-> contract? (-> blame? (-> val neg-party val*)))

That is, given a contract, it returns a function that, when given a blame
object, returns a function that enforces the contract. The enforcer function
accepts the value being checked and the "negative party" and either raises an
exception or returns the checked value, possibly wrapped to enforce higher-
order checks.

(The "negative party" is simultaneously deeply important and something you
could ignore to start with. Simply put, if a module `(server)` provides a
contracted value that is used by a module `(client foo)`, the "negative party"
represents `(client foo)`, e.g. via a source location. It is the only part
that would be different between `(client foo)` and `(client bar)`, so this API
lets everything else be shared.)

The multiple levels of `lambda` let contract combinators do some of their work
ahead of time, improving performance when the contracted value is used.

As a motivating example, here is a very basic definition of the `listof`
contract combinator. Notice in particular:

  * Predicate functions and certain kinds of primitive data are implicitly
    promoted to contracts. This wasn't original to Racket's contract system,
    but the ergonomics are so compelling you might want it from the beginning.

  * Forms like `define/contract`, `struct/contract`, and `contract-out` (which
    is preferred) attach contracts to values. Guix might want
    `define-record-type*/contract`. There is no public API for constructing
    blame objects.

> #lang racket
> (define (listof elem/c)
>   (let* (;; error if elem/c isn't a contract
>          [elem/c (coerce-contract 'listof elem/c)]
>          [elem-late-neg (get/build-late-neg-projection elem/c)])
>     (make-contract
>      #:name (build-compound-type-name 'listof elem/c)
>      #:late-neg-projection
>      (λ (blame)
>        (define elem-proj+blame
>          (elem-late-neg (blame-add-context blame "an element of")))
>        (λ (val neg-party)
>          (unless (list? val)
>            (raise-blame-error
>             blame val #:missing-party neg-party
>             `(expected: "a list" given: "~e")
>             val))
>          (for-each (λ (elem)
>                      (elem-proj+blame elem neg-party))
>                    val)
>          val)))))
> 
> (define/contract numbers
>   (listof number?)
>   '(1 2 2.5 3))
> 
> (define/contract fruits
>   (listof (or/c 'apple 'banana))
>   (list (λ (x) (x x))))

The resulting error message:

> fruits: broke its own contract
>   promised: (or/c (quote apple) (quote banana))
>   produced: #<procedure:...of-contract-mvp.rkt:27:8>
>   in: an element of
>       (listof (or/c 'apple 'banana))
>   contract from: (definition fruits)
>   blaming: (definition fruits)
>    (assuming the contract is correct)
>   at: /tmp/listof-contract-mvp.rkt:25:17

The most important optimization I left out is providing a specialized first-
order check for use by `or/c`. But even that, in principle, wouldn't have to
be part of an initial implementation.

And, again, you should only need even this much work for a combinator or a
higher-order contract. 

Do note that this is all fresh off the top of my head in about an hour, and
I've only incidentally hacked on the internals of the Racket contract system!
If using contracts in Guix is at all appealing, I'd strongly suggest asking
for advice at <https://racket.discourse.group> before starting to write code.
A few other resources:

  * "Inside Racket Seminar: Robby Findler on Contracts"
    <https://www.youtube.com/watch?v=eUsDKbKtrLs>
    A two-hour video walkthrough/Q&A about the implementation of Racket's
    contract system. Probably the most comprehensive resource that exists on
    how to implement contracts, as opposed to interesting things to do with
    contracts once you've got them.

  * Robby Findler, "Behavioral Software Contracts" (ICFP 2014)
    https://www.youtube.com/watch?v=gXTbMPVFP1M
    Wonderful slides and illustrations help to illuminate some of the more
    difficult concepts.
    In particular, I recommend the section @11:10, "Contracts are not Types",
    which explains some very interesting contracts like the one on `dc`[4]
    that take advantage of contracts being checked *at runtime* to enforce
    very nuanced invariants, somewhat like "dependent types" requiring a
    drawing procedure to restore any changes it makes to Cairo's mutable
    state. This would support examples like Arun's: say, checking that no two
    services are trying to listen on the same TCP port.
    The concept of "boundaries" as a design principle is an important lesson
    learned.
    The source code for the slides (which are a program in `#lang slideshow`,
    of course) is at <https://github.com/rfindler/icfp-2014-contracts-talk>.

  * "Oh Lord, Please Don’t Let Contracts Be Misunderstood"
    Dimoulas, New, Findler, & Felleisen (ICFP 2016)
    https://users.cs.northwestern.edu/~robby/pubs/papers/icfp2016-dnff.pdf
    Focused on pragmatics (as opposed to fancy math), with discussion both of
    how a contract system is put together and of some interesting uses.

I would love to have contracts in Guix, even very rudimentary contracts. If
it's something the community more generally would be interested in, I'd be
glad to help as much as I can.

-Philip

[1]: 
https://docs.racket-lang.org/reference/Building_New_Contract_Combinators.html#%28def._%28%28lib._racket%2Fcontract%2Fprivate%2Fblame..rkt%29._raise-blame-error%29%29
[2]: 
https://docs.racket-lang.org/reference/Building_New_Contract_Combinators.html#%28def._%28%28lib._racket%2Fcontract%2Fprivate%2Fblame..rkt%29._blame-add-context%29%29
[2]: 
https://docs.racket-lang.org/reference/contract-utilities.html#%28def._%28%28lib._racket%2Fcontract%2Fprivate%2Fguts..rkt%29._get%2Fbuild-late-neg-projection%29%29
[4]: 
https://docs.racket-lang.org/pict/Basic_Pict_Constructors.html#%28def._%28%28lib._pict%2Fmain..rkt%29._dc%29%29

signature.asc
Description: This is a digitally signed message part.