Advice on implementing a contract system?

[LiberalArtist]

I'm looking for advice on beginning the implementation of a contract system (i.e. not in Racket).

I've been using and contributing to Guix, an unprivileged "purely functional" package manager (and full GNU/Linux distribution) implemented in Guile.

Many of Guix's functions and data structures don't check that their arguments meet their implicit contracts, leading to confusing error messages when mistakes are made. Recently, one of the Guix committers brought up this issue and suggested that Guix ought to adopt a mechanism for more conveniently checking arguments—which sounded a lot like contracts. In the subsequent discussion, it emerged that several Guix developers were, in fact, interested in contracts, but I guess the prospect of going from 0 to contracts seemed like a bit of an intimidating barrier to entry.

I tried to sketch out a minimal API for contracts (I'll quote most of that message at the end of this for convenience), and I was encouraged to put together a prototype implementation, but, as I wrote in that message,

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.

So here I am doing that!

I've read several of the contract papers and watched "Inside Racket Seminar: Robby Findler on Contracts" (though not recently), and I think I have at least a reasonable understanding of how the contract system is implemented generally, though, again, I have only peripherally contributed to the implementation of racket/contract.

Broadly, I'm interested in the questions I wouldn't think to ask.

More specifically, for this to be viable for Guix, I think the key challenge is to find a "minimum viable product" that:

1. is immediately useful;
2. has as little overhead as possible; and
3. provides a foundation to grow more complete by the "infectious" process Robby has described by
4. avoiding design decisions that would create problems later.

On the last point, this library would be internal to Guix for the forseeable future, so it has much weaker compatibility requirements than racket/contract—but, on the other hand, Guix has on the order of 800,000 lines of Scheme.

As far as minimization, one question seems to be what kinds of unsoundness can be lived with to start without causing big problems later. We would have no hope of being a "complete monitor" for the foreseeable future, nor would we have impersonators/chaperones for Scheme data in general (something for Guix record types might be possible), and Guile has mutable pairs, which I'm fairly convinced, in the absence of chaperones, will ultimately have to retain the "just say no to set-c{a,d}r!" status quo. I know racket/contract has some unsound contracts (e.g. box/c with #:flat? #t applied to a mutable box), so it seems like a workable pragmatic compromise. On the other hand, there's unsoundness that, with the benefit of hindsight, may be avoidable, like the issue with mutable (byte)strings.

Similarly, I wouldn't even be the right person to attempt any Guile-specific performance tuning, but hard-learned lessons about performance in general would certainly be valuable.

Finally, as promised, here are some more of my earlier thoughts:

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.

[…]

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.

[EmEf]

Have you considered restricting yourself initially to just first-order contract and only a fixed set of basic predicates and predicate combiners?

— boolean? 
— integer? 
— ..
—  [listof string?]
— .. 
— [vectorof real?]
— … 
— procedure? 
— .. recursivon ...

plus a form for attaching contracts to functions as they get exported?

(0) it’s quick to build
(1) you know the cost and it’s quite apparent to any GUIX developer [still non-trivial]
(2) you can separate the contract-checking from the main functionality, making both clear and readable in MOST cases
(3) you get systematically formed error messages
(4) you get first-order blame

Side effects:

(1) it’s simple and easy to understand
(2) you avoid the allocation cost of wrappers for HO objects and blame info
(3) you avoid the cost of repeatedly wrapping (can be bad if you use plain OO style)
(4) you avoid the compiler cost of calling through wrappers

And best of all this is compatible with future extension for ho contracts.

;; - - -

I will also say that as much as I like ho contracts and use them extensively,
making everything a function is bad for any future optimization.

Michael B. Cameron M and I are thinking of designing a hosted contract DSL on top,
via Michael’s special-purpose expanders, and experimenting with a classical optimizer,
perhaps even using Leif’s nano-passes (adapted for syntax of course).

[greghendershott]

I'm not qualified to offer advice here (my only thought was a tiny subset of what @EmEf mentioned, that avoiding higher-order might be a natural inflection point for a version 1.0).

Instead:

Someone in your guix discussions might bring up Clojure spec -- which if not exactly contracts is at least adjacent and shares some goals -- so I wanted to point it out in the unlikely event you didn't already know about it.

[LiberalArtist]

@EmEf

Have you considered restricting yourself initially to just first-order contract

To some extent, yes.

@EmEf

and only a fixed set of basic predicates and predicate combiners?

— boolean? 
— integer? 
— ..
—  [listof string?]
— .. 
— [vectorof real?]
— … 
— procedure? 
— .. recursivon ...

This part seems less viable to me.

To get into more detail, let me return to the motivating example (from Ricardo Wurmus):

As you can probably tell easily by looking at this message, the
“service” field of the operating system configuration looked something
like this:

  (services (append (list a b c %desktop-services) #;oops))

instead of this

  (services (append (list a b c) %desktop-services))

This is because INSTANTIATE-MISSING-SERVICES — and FOLD-SERVICES, and
many more — assumes that it is only passed a plain list of services. It
then proceeds to call SERVICE-KIND on what may or may not be a service.

In Guix, operating-system and service are data types in what arguably amounts to an custom object system implemented by the module (guix records).

An operating-system value declaratively defines a system configuration: what kernel and bootloader to use, what user accounts should exist, etc. A service can be many things; here's an example: (service openssh-service-type (openssh-configuration (accepted-environment '("COLORTERM")) (password-authentication? #t) (permit-root-login 'prohibit-password) (authorized-keys `(("philip" ,bastet_id_ed25519.pub) ("root" ,bastet_id_ed25519.pub)))))

One implication is that we can't have a fixed set of predicates: the contract library shouldn't need to know about the predicate service?. (Also, while the idea of an optimized contract DSL with special-purpose expanders sounds interesting, I know even less about how to implement that—especially in Guile—than how to implement a library like racket/contracts.)

Most of the things we'd want to check are first-order. In particular, Guix promotes a functional style of programming: even when using mutable Scheme datatypes, you aren't supposed to actually mutate them. Especially given that we won't have runtime support for chaperones or impersonators, I'd plan to leave those invariants unchecked.

We probably do want contracts that check function results, but I know how to implement those, at least to the extent of the simple-arrow example from 7.8 Building New Contracts.

I'm not sure how important higher-order functions would be to start with—even fold-services is't actually a higher-order function—though, on the other hand, if I were implementing the simple-arrow combinator, I wouldn't know or care if one of the sub-contracts also used simple-arrow.

Actually, as I'm writing this, it occurs to me that it might be possible to avoid even something like simple-arrow to begin with if the library provided contract attachment forms in the spirit of invariant-assertion and struct-guard/c …

Sooner or later, a high-value objective would be integrating contracts into (guix records), which has some complexity. Datatypes like operating-system and package are "self-referrential records" with support for thunked fields (see The Big Change — 2021 — Blog — GNU Guix).

Drawing again on the motivating example, the buggy operating-system value would have been constructed from an expression like this (which, other than services, includes only the required fields):

(operating-system
  (host-name "example")
  (timezone "Etc/UTC")
  (file-systems %base-file-systems)
  (bootloader (bootloader-configuration
               (bootloader grub-bootloader)
               (targets '("/dev/sda"))))
  (services (append (list a b c %desktop-services) #;oops)))

The definition of operating-system declared services as a "thunked" field, so the constructor macro does not immediately evaluate the expression (append (list a b c %desktop-services) #;oops): instead, it is evaluated when the field is first accessed. "Thunked" fields may make use of syntax parameters like this-operating-system to compute their values based on other parts of the record as a whole. In particular, (guix records) includes an inheritance mechanism (e.g. (operating-system (inherit example-os) ...)), so, as with this/self in an OOP context, the value of this-operating-system may be some derived record, not the one in which the "thunked" field right-hand-side expression was syntactically written. In other words, the expression on the right-hand-side of services is wrapped in a function that may be called multiple times with different arguments.

The tl;dr of all that is that (guix records) seems to ultimately call for "indy-dependent" contracts.

On the one hand, the distinction between "indy-dependent" ->i and "lax-dependent" ->d is exactly the sort of hard-learned lesson that I hope the Guix community can draw from Racket's decades of experience.

On the other hand, I'm increasingly intrigued by the idea of starting with forms along the lines of invariant-assertion and struct-guard/c and truly sticking to flat contracts to start with, leaving all the higher-order complexity for another day.

[robby]

If I were to get to redo racket/contract, the one big change I'd make is to design a (macro-based) DSL for contracts instead of going with a combinator-based approach. Although you won't need to do it for a minimum-viable product, the opportunity to, at a later date, look at an entire contract at compile time and generate better code for it is probably going to be useful.

That is, no one writes things like (apply listof (map -> doms rngs)) or things like that; instead people tend to write out their contracts directly (-> (listof integer?) boolean?) or similar. So the fact that -> and listof are just normal functions isn't really used and it leads to an opportunity cost of being able to generate a function contract "all at once" that's tailored to the specifics of the domain and range of the function.

Of course the contract library is able to do some of this already as it makes -> and listof etc behave like functions but actually be macros but it is a pain and it would be a lot better if there was an explicit (sub)-language designed. Then, all the indirect calls through the late-neg projections could be avoided and performance would be better.

That said, you definitely want to allow arbitrary predicates to just be contracts without having to type a lot of stuff, as that's turned out to be super useful.

[benknoble]

I did just recently write (apply or/c (some list of generated contracts)) for a dependent contract, so there are some uses of the combinator-style behavior. How would you solve that with a macro-based DSL?

[robby]

The change would end up being more about improving the internals of the implementation so that there is less friction internally and it is easier to get better performance for the commonly written contracts. So I wouldn't expect anything that's possible now to become impossible, just that different things might be more awkward in various ways. Put another way, it should be more clearly defined when some position must be in the "contract language" as opposed to just being a subexpression in general. And these two would probably need to go back and forth to each other. Like the arguments to <=/c probably should be allowed to be arbitrary expressions, not just constants, for example.

For the specific question you have here, I think I'd probably chose one of two different answers. There probably could be a variation on or/c that accepts a list as its argument directly, or there would be a general escape where one would explicitly write something that means "racket expression" as a subexpression somewhere and then you'd have to use that generic escape in some way to achieve the effect you have in mind.

And it is good you bring up dependent contracts. Currently, dependency is a spot where things are especially expensive for no good reason. The issue is that the contract combinators are organized internally as curried functions where a lot of work happens on the first application, but that work is all done early on, when building up the contract. This works great until dependent contracts enter the picture, as the expensive work ends up being done whenever the dependent parts are calculated. Here's some timing results that illustrate the difference. The difference, in this particular example, would just go away, I believe (not having tried it ).

#lang racket
(define f1
  (contract (->i ([x integer?]
                  [y (x) (listof (or/c (<=/c 5) (>=/c 105)))])
                 any)
            (λ (x y) x) 'pos 'neg))

(define f2
  (contract (->i ([x integer?]
                  [y (listof (or/c (<=/c 5) (>=/c 105)))])
                 any)
            (λ (x y) x) 'pos 'neg))

(define (try f)
  (collect-garbage) (collect-garbage)
  (time
   (for ([x (in-range 100000)])
     (f 1 '(2)) (f 1 '(2)) (f 1 '(2)) (f 1 '(2))
     (f 1 '(2)) (f 1 '(2)) (f 1 '(2)) (f 1 '(2)))))

(try f1)
(try f2)

[benknoble]

Interesting example: it's obvious to a human they're equivalent, but depending on the internal representation making that decision could be difficult Perhaps the dependent contract combinators need a way warn on unused dependencies that cause such slowdowns?

The escape hatch sounds reasonable: I'm often impressed by how easy it is to drop natural-looking Racket code into Qi forms, so perhaps some inspiration can be taken from there?