Re: Declaring Lisp function types

[Andrea Corallo]

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.

Thanks

  Andrea