Re: Declaring Lisp function types

[Arthur Miller]

Andrea Corallo <acorallo@gnu.org> writes:

> Arthur Miller <arthur.miller@live.com> writes:
>
>> Stefan Monnier via "Emacs development discussions."
>> <emacs-devel@gnu.org> 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)® 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
>>>> <args> <rettype>)?  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)))) =>
>>>(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)))) =>
>>>(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.

Allright, that is unfortunate, but I understand, thanks for the clarification.

/best regards

> Thanks
>
>   Andrea