From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Andrea Corallo Newsgroups: gmane.emacs.devel Subject: Re: Declaring Lisp function types Date: Mon, 18 Mar 2024 05:02:23 -0400 Message-ID: References: Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="23959"; mail-complaints-to="usenet@ciao.gmane.io" User-Agent: Gnus/5.13 (Gnus v5.13) Cc: emacs-devel@gnu.org To: Arthur Miller Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane-mx.org@gnu.org Mon Mar 18 10:03:40 2024 Return-path: Envelope-to: ged-emacs-devel@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1rm8uB-00061b-UR for ged-emacs-devel@m.gmane-mx.org; Mon, 18 Mar 2024 10:03:40 +0100 Original-Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1rm8tC-0000jA-PD; Mon, 18 Mar 2024 05:02:38 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1rm8t9-0000iv-LI for emacs-devel@gnu.org; Mon, 18 Mar 2024 05:02:36 -0400 Original-Received: from fencepost.gnu.org ([2001:470:142:3::e]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1rm8t8-00033H-22; Mon, 18 Mar 2024 05:02:35 -0400 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=gnu.org; s=fencepost-gnu-org; h=MIME-Version:Date:References:In-Reply-To:Subject:To: From; bh=fYubADn3GNGv84lThr6jJhwhZAorsXkPKTc5sE7Owuc=; b=sQY0gvczQFFDdZhecr4a +x4jZQ8wyAq1pTa8rDAHmUNcO26InLAUMSrikumH2JulKwII2OSi+HjmPRezmUCGs65lGIuVrN4Vp r8zvNPOI1E+0nVRC2oJSW9W8Mocbkegzxm1vdUw9uIHnNsimzYHYZ7cIJuOXQpLN7GKDlTgf2kUjt E4rWB0WfE+2k0TGD+rKqPswgGSAd4C71c8PEQdep35U0/XlPv/y4bNW31+/ZxrGYieQDtBQSK5m2y CCwVHJgGk5VKTqwbevecNUe65srqRhBq/OZNvaBZIDLRSUqlSpfMSsa+uLZJRLnpaRTIsJG13uosV Xp8NKa6lPgweKQ==; Original-Received: from acorallo by fencepost.gnu.org with local (Exim 4.90_1) (envelope-from ) id 1rm8sz-0008WU-NP; Mon, 18 Mar 2024 05:02:33 -0400 In-Reply-To: (Arthur Miller's message of "Sat, 16 Mar 2024 08:46:24 +0100") X-BeenThere: emacs-devel@gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: "Emacs development discussions." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-devel-bounces+ged-emacs-devel=m.gmane-mx.org@gnu.org Original-Sender: emacs-devel-bounces+ged-emacs-devel=m.gmane-mx.org@gnu.org Xref: news.gmane.io gmane.emacs.devel:317161 Archived-At: Arthur Miller writes: > Stefan Monnier via "Emacs development discussions." > writes: > >>>> (declaim (ftype (function (integer integer) integer) sum)) >>>> ;; ^^inputs ^^output [optional] >>>> (defun sum (a b) >>>> (declare (integer a b)) >>>> (+ a b)) >>> >>> Non-starter for me: the separation into two steps makes it unclear what >>> the declaration applies to (e.g. when re-running the above code, does >>> the `declaim` apply to the old definition (the one active when the >>> `declaim` is executed)=C2=AE the the one that's about to be installed)? >>> >>>> ;;2 >>>> (defun sum (a b) >>>> (declare (integer a b)) >>>> (+ a b)) >>> >>> None starter because of how we defined `declare`, where we'd have to >>> define every existing type as a valid declaration idenitifer. >>> >>>> ;;3 through 'defstar' (a CL library not in the standard) >>>> (defun* sum ((a integer) (b integer)) >>>> (+ a b)) >>>> ;;4 again through 'defstar' >>>> (defun* (sum -> integer) ((a integer) (b integer)) >>>> (+ a b)) >>> >>> Acceptable, with some tweaks to better fit my favorite bikeshed color. >>> >>>> (defun sum (a b) >>>> (declare (ftype (function (integer integer) integer))) >>>> (+ a b)) >>> >>> The `f` of `ftype` is redundant with the following `function`, so we >>> could shorten that to: >>> >>> (defun sum (a b) >>> (declare (ftype (integer integer) integer)) >>> (+ a b)) >>> >>>> (defun sum (a b) >>>> (declare (function (integer integer) integer)) >>>> (+ a b)) >>> >>> It's cute, I guess. Whether to prefer `function`, `ftype`, or Adam's `= type`, >>> is largely a "bikeshed color" choice. I do prefer the latter two >>> because we already know that this is a function, whereas we don't know >>> that this is a *type* (and they're shorter, to boot). >>> >>> Later you said: >>>> Fact is, we already use the form (function (ATYPES) RTYPE) as type >>>> specifier for functions. So (ftype (function (ATYPES) RTYPE)) would be >>>> the most correct form semantically, where `ftype` (or `type` or really >>>> what we prefer) would be the declaration which takes the type specifier >>>> as argument. >>> >>> Of course (declare (ftype (integer integer) integer)) >>> would still end up generating something like >>> >>> (foo-declare-type 'sum '(function (integer integer) integer)) >> >>My fear it's this is a bit more convoluted and this extra step makes it >>less understandable/justifiable. I like the symmetry of having >>'function' both in the input (the declaration) and the output (the final >>type itself). Maybe my background as physicist makes symmetry too >>central for me? :) >> >>> so I see no semantic issue with using `ftype` or `type` here, unless >>> there are functions whose type could take another form than (function >>> )? Are you thinking of types like >>> (or (function (int) int) (function (float) float))? >> >>That's a good example why it would be good to be able to accept the type >>specifier as a declaration with no tricks. On the specific case I'm not >>sure we want to support this in the inner machinery (at least for now). >> >>> More important I think is to document what such annotations mean and >>> what they should look like (currently, this is not super important, >>> because the annotations live together with the code that uses them, but >>> if we move them outside of `comp.el`, the "contract" needs to be made >>> more explicit). >>> >>> - How they interact with `&optional` and `&rest` (or even `&key` for >>> `c-defun`). >> >>ATM we already support in type specifiers `&optional` and `&rest`: >> >>(subr-type (native-compile '(lambda (x &optional y &rest z)))) =3D> >>(function (t &optional t &rest t) null) >> >>Not sure we want to handle &key as well as it looks to me not very >>native to the elisp machinery. OTOH cl-defun just expands to the native >>elisp call convention. >> >>> - What will/could happen if one of the arguments does not have the >>> specified type? >> >>I think if ones does a declaration has to declare the type of all >>arguments (rest should be optional). >> >>> - What will/could happen if the result does not have the >>> specified type? >> >>I think we want to complete it with the inferred return type if we have >>it or t otherwise. >> >>> - Do we have types to say "arg unused" or "no return value"? >> >>We don't have "arg unused" because the function type (or signature) is >>like the contract with the outside word, it should not matter how (and >>if) and arg is used inside. >> >>OTOH we have "no return value" and it's nil >> >>(subr-type (native-compile '(lambda (x) (error x)))) =3D> >>(function (t) nil) >> >>> - Can we have higher-order function types, like >>> >>> (function (proc (function (proc string) void)) void) >>> >>> and if so, again, what does it mean in terms of what can happen if the >>> runtime values don't actually match the announced types (e.g. what >>> happens (and when) if we pass a function that has the "wrong type")? >> >>I don't kwnow if we want to allow this to be future proof, ATM certanly >>the compiler does not use it and I don't think it could help code >>generation. OTOH might be nice for documentation? >> >>As a note: AFAIR SBCL doesn't go beyond something like: >>(function (integer function) function) >> >>That if arguments/ret values are functions it forgets the inner details >>of their type specifier. >> >>Anyway I certanly agree we should better document this once it's shaped, >>and I'll try my best. >> >>But generally speaking I've the feeling there might be other cases we >>don't see ATM where accepting directly the type specifier as valid >>declaration graciously/naturally solves potential issues we could hit >>otherwise. >> >>Thanks > > Please, if you can, just (re)use SBCL syntax. It makes life easier > for those who are already familiar. Those who are not have to learn > something new anyway, so for them it does not matter. > > Great work, thank you working so much with this. Hi Arthur, I agree on the principle, but unfortunately as mentioned using the CL syntax in the Emacs declare machinery is problematic for how this second one is constructed. I think is not a realistic option. Thanks Andrea