From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id ADQ2O+n1HGKNngAAgWs5BA (envelope-from ) for ; Mon, 28 Feb 2022 17:18:49 +0100 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id yJVVOOn1HGJHSAEA9RJhRA (envelope-from ) for ; Mon, 28 Feb 2022 17:18:49 +0100 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 9153EE447 for ; Mon, 28 Feb 2022 17:18:49 +0100 (CET) Received: from localhost ([::1]:50220 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1nOijX-0003oh-Pu for larch@yhetil.org; Mon, 28 Feb 2022 11:18:47 -0500 Received: from eggs.gnu.org ([209.51.188.92]:48688) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1nOijH-0003nJ-LS for guix-devel@gnu.org; Mon, 28 Feb 2022 11:18:31 -0500 Received: from new4-smtp.messagingengine.com ([66.111.4.230]:34553) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1nOijF-0005OV-9J; Mon, 28 Feb 2022 11:18:31 -0500 Received: from compute5.internal (compute5.nyi.internal [10.202.2.45]) by mailnew.nyi.internal (Postfix) with ESMTP id 90E515800C6; Mon, 28 Feb 2022 11:18:26 -0500 (EST) Received: from mailfrontend1 ([10.202.2.162]) by compute5.internal (MEProxy); Mon, 28 Feb 2022 11:18:26 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= philipmcgrath.com; h=cc:cc:content-type:date:date:from:from :in-reply-to:in-reply-to:message-id:mime-version:references :reply-to:sender:subject:subject:to:to; s=fm1; bh=IrLlic9Jt4zfH/ m2s0TCDi2V6sVlT7xHy/dZAodJMxo=; b=LY03OSCmd1GgmgaWbnQdSvA9o/pFmv mNIVD6kaL4xKp0GOUdo+omeRoXCCHWiLvpSNV2JGJq72mzki6dJ/oH35lnOzFiny I1R0ND4kRtFCbJoaXh/eyjyRGARSWnpX9RqLrYjOus5gtdZDgIVAFnTOMMwnoZU+ EJGXXarlx4GeypztbNbhlpFafoga1jxqkfn3af95cvmeuXLXGGO2KlOO7HK8G8ZE V+ZAVOkpNQ5oQiHuQiqu93LFF0o6FuYvPpPwhY8v2GzcCz2AY1DOigGg+MyfGUW0 77xW6jYcEEwcqXkCVIEkMZLONX1TF+X3Xy5CqsCx6kjh9fIHigJJxzRg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=cc:cc:content-type:date:date:from:from :in-reply-to:in-reply-to:message-id:mime-version:references :reply-to:sender:subject:subject:to:to:x-me-proxy:x-me-proxy :x-me-sender:x-me-sender:x-sasl-enc; s=fm2; bh=IrLlic9Jt4zfH/m2s 0TCDi2V6sVlT7xHy/dZAodJMxo=; b=JVUse8ffNJP/WN5OXlN271UvFoaSubo/B si2ArMH++sMka7zo3jj9xbIliRQmqCp15of4KjOX+FButBBRYyEmXZbhrc+g1qNN Z95ivZKuaLyxgExVE4V/yTt+Dc3YmIMwpcfRIfrw4MHyRk75GdH+PAudMr5M7Ptt 4LwXjcjQXoyFyc48i2BMr6QshnjIor4AItPpLvN3a+o2xP4Zds8TzuLhGdViqpJp 5IEj5gBqmCkpV+2tdGSmhUqFQkFwIWQttX+DIqz7g1hXhbY3gcto8yX8BuGKtPNE 0j5ONSP9fCz7g3H8RhfFM8AZAqS0a3BClXaGHgukOW037TjTitm5A== X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvvddruddttddgkeeiucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmne cujfgurhephffvufffkfgjfhggtgesghdtreertddtjeenucfhrhhomheprfhhihhlihhp ucfotgfirhgrthhhuceophhhihhlihhpsehphhhilhhiphhmtghgrhgrthhhrdgtohhmqe enucggtffrrghtthgvrhhnpeegvdfggfefgeffveffieefvdeivdeileeghfekteekkeej jeevieeigffffeeuieenucffohhmrghinhepughishgtohhurhhsvgdrghhrohhuphdphi houhhtuhgsvgdrtghomhdpghhithhhuhgsrdgtohhmpdhnohhrthhhfigvshhtvghrnhdr vgguuhdprhgrtghkvghtqdhlrghnghdrohhrghenucevlhhushhtvghrufhiiigvpedtne curfgrrhgrmhepmhgrihhlfhhrohhmpehphhhilhhiphesphhhihhlihhpmhgtghhrrght hhdrtghomh X-ME-Proxy: Received: by mail.messagingengine.com (Postfix) with ESMTPA; Mon, 28 Feb 2022 11:18:25 -0500 (EST) From: Philip McGrath To: Ricardo Wurmus , Ludovic =?ISO-8859-1?Q?Court=E8s?= Subject: Re: better error messages through assertions Date: Mon, 28 Feb 2022 11:18:16 -0500 Message-ID: <2205364.8dmU9V6fpu@bastet> In-Reply-To: <87mtibdu5l.fsf@gnu.org> References: <87ilthoxvu.fsf@elephly.net> <87k0dv6ahq.fsf@elephly.net> <87mtibdu5l.fsf@gnu.org> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="nextPart3313496.3sTWpJvqYL"; micalg="pgp-sha512"; protocol="application/pgp-signature" Received-SPF: pass client-ip=66.111.4.230; envelope-from=philip@philipmcgrath.com; helo=new4-smtp.messagingengine.com X-Spam_score_int: -15 X-Spam_score: -1.6 X-Spam_bar: - X-Spam_report: (-1.6 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, RCVD_IN_DNSWL_LOW=-0.7, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01, URI_DOTEDU=1.246 autolearn=no autolearn_force=no X-Spam_action: no action X-BeenThere: guix-devel@gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Cc: guix-devel@gnu.org Errors-To: guix-devel-bounces+larch=yhetil.org@gnu.org Sender: "Guix-devel" X-Migadu-Flow: FLOW_IN X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1646065129; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=IrLlic9Jt4zfH/m2s0TCDi2V6sVlT7xHy/dZAodJMxo=; b=PIULPPQV9bsp56ZNm2B+F3+z/0XAcLEBfImD6XbP2bWX37qnlCNP/Q3KY/UQl4nK+WnF4g mB9SaE6yzcTNS5A2Zp9a4P7j4kCIA7Sxdc5oSGelgfuaeaDOXyiu41jpbJZtO6KO8Ntglw cb9AFRjrbZYnt9MVh44Fk0qGBMkyCtm88+C7OqI9ECED55DqDgSkKe344f91WvICArZiZk 1DwVptF9Hvd7RUQpwPmmwjrkfHyEnLzYA1Pir8nNa4kzK3kSwQvM4tXv05XXQ5UKEKHdZJ sN7jSfjG5EgsBykisaSXPBhoyabo9xYPmL6kLyMrxMSdkjqhvysxeRk9aJI60g== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1646065129; a=rsa-sha256; cv=none; b=UPXB4Pxt2W0KSAznlqFOrxV6PhFwaIpV+n/u6/X8TcVCvU7mfsVr2hZdcfPX6YsFIgI99q Dd1+dvN/xRmXnMEWGuGGaeWBY2+WR3U0A88s01yi1z3mwqP3FiDnRLxFc0abyUCurVt4oQ MGhgzdwNAVy4bQYyaR1GJTC+rn+JLbNOvl9yTB0B7/57vQzn9H9qe4gnSPox5YbqyqRxeY Ks7RWm6Sr1OOPtluJlIRWI4q57nnijKZvh4M4uJ3AJuGdnFVpiZLb3cLaAv4Y9FWuDft75 C+BSJvjYbqVXT+NSw9jngCk6b+7X1Ez59GfExBfDoX08VA4wsvBDx6vH7e7cxw== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=philipmcgrath.com header.s=fm1 header.b=LY03OSCm; dkim=fail ("headers rsa verify failed") header.d=messagingengine.com header.s=fm2 header.b=JVUse8ff; dmarc=none; spf=pass (aspmx1.migadu.com: domain of "guix-devel-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-devel-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: -1.79 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=philipmcgrath.com header.s=fm1 header.b=LY03OSCm; dkim=fail ("headers rsa verify failed") header.d=messagingengine.com header.s=fm2 header.b=JVUse8ff; dmarc=none; spf=pass (aspmx1.migadu.com: domain of "guix-devel-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-devel-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: 9153EE447 X-Spam-Score: -1.79 X-Migadu-Scanner: scn0.migadu.com X-TUID: ++0m/FtvNOi2 --nextPart3313496.3sTWpJvqYL Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8"; protected-headers="v1" From: Philip McGrath To: Ricardo Wurmus , Ludovic =?ISO-8859-1?Q?Court=E8s?= Cc: guix-devel@gnu.org, Arun Isaac Subject: Re: better error messages through assertions Date: Mon, 28 Feb 2022 11:18:16 -0500 Message-ID: <2205364.8dmU9V6fpu@bastet> In-Reply-To: <87mtibdu5l.fsf@gnu.org> References: <87ilthoxvu.fsf@elephly.net> <87k0dv6ahq.fsf@elephly.net> <87mtibdu5l.fsf@gnu.org> Hi, On Monday, February 28, 2022 7:59:02 AM EST Ludovic Court=C3=A8s wrote: > Hi! >=20 > Ricardo Wurmus skribis: > > Philip McGrath writes: > >> As a Racketeer, I think you're half way to reinventing contracts. > >=20 > > 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. >=20 > I=E2=80=99d very much like to have contracts. >=20 > For record types, we have =E2=80=9Csanitizers=E2=80=9D right now, which w= e could use to > insert procedural type checks. It wouldn=E2=80=99t be as nice as proper > declarative contracts though, unless we arrange to make them look like > contracts. >=20 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 re= st of a contract system. In the short term, the advantage over: > (assert-type (listof service?) services > "SERVICES must be a list of 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"/"give= n" with "promised"/"produced" in error messages based on the context. A contra= ct combinator will typically give its sub-contract a blame object extended usi= ng `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 par= ty" 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 w= ork 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 beginni= ng. * Forms like `define/contract`, `struct/contract`, and `contract-out` (wh= ich 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 > (=CE=BB (blame) > (define elem-proj+blame > (elem-late-neg (blame-add-context blame "an element of"))) > (=CE=BB (val neg-party) > (unless (list? val) > (raise-blame-error > blame val #:missing-party neg-party > `(expected: "a list" given: "~e") > val)) > (for-each (=CE=BB (elem) > (elem-proj+blame elem neg-party)) > val) > val))))) >=20 > (define/contract numbers > (listof number?) > '(1 2 2.5 3)) >=20 > (define/contract fruits > (listof (or/c 'apple 'banana)) > (list (=CE=BB (x) (x x)))) The resulting error message: > fruits: broke its own contract > promised: (or/c (quote apple) (quote banana)) > produced: # > 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.=20 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 syste= m! If using contracts in Guix is at all appealing, I'd strongly suggest asking for advice at before starting to write cod= e. A few other resources: * "Inside Racket Seminar: Robby Findler on Contracts" 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=3DgXTbMPVFP1M 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 t= wo 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 . * "Oh Lord, Please Don=E2=80=99t 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. =2DPhilip [1]: https://docs.racket-lang.org/reference/Building_New_Contract_Combinato= rs.html#%28def._%28%28lib._racket%2Fcontract%2Fprivate%2Fblame..rkt%29._rai= se-blame-error%29%29 [2]: https://docs.racket-lang.org/reference/Building_New_Contract_Combinato= rs.html#%28def._%28%28lib._racket%2Fcontract%2Fprivate%2Fblame..rkt%29._bla= me-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-ne= g-projection%29%29 [4]: https://docs.racket-lang.org/pict/Basic_Pict_Constructors.html#%28def.= _%28%28lib._pict%2Fmain..rkt%29._dc%29%29 --nextPart3313496.3sTWpJvqYL Content-Type: application/pgp-signature; name="signature.asc" Content-Description: This is a digitally signed message part. Content-Transfer-Encoding: 7Bit -----BEGIN PGP SIGNATURE----- iQIzBAABCgAdFiEE9GWrrNY3rqwUFVXPygNjjfo/HHoFAmIc9cgACgkQygNjjfo/ HHpF/RAAklfhJAgoISDCfITWIxCo5x4lkBwT/5TGtpkH0iavkAJBVPQmh9eB9vFX NukUrZNvdkM7QMACS7M9mwLHZ+YfHXgIAfw2/Vl08zbGbI3hWmYuy9FjV/wHQ+bf NDKfQbc1MkI5D6vQohQRDCGURiRBrc21/yHjyvNj+8NsnZyiYv9oslSc4viY9Ib3 oW7NixwNBrIe5qiCBbavXKya2eGCDkhowHXN2fvRB8u9QVzuTW/CALQ3Do8cuzg5 29XEYrH/unjIJpP1p092cazONDnLIMMJfOUgeF16TZ3vn6vAkKe0gwzJF1HjKyA2 NsgQi/Iopfom17IljZJHQoDqr9tZq/BghAB22Bmolu1Ehg1N7o8UI3lSMV065pre 8zgQ4DIONhJQetEVC2udhJOJPNTDe77Ikp6m8M96EIpUxse+mXhMfe06+HdKViSG vosq0QefBBCXyNtYh8pfN896LDodJLHxpf86eVqQkvDfT+W/juPy3cSKU3CG2nlq B20g33AGWG4zPFm1xkt/Nw6B2AV6B7u7qoFCbpXVZoEd+Ht0j9lnbB0JZQB3eKxR wFlwFn/QbNzwKvByh0zHb6pFR3GWvGFsowULwZJf1ANaDZoJ8i9EtzkUXs4x7C5n yF14mxUdNkiWRUu5Ag3DhuzReS6WdQGydVs0XEwxMzQOFGGbyK4= =6NL1 -----END PGP SIGNATURE----- --nextPart3313496.3sTWpJvqYL--