[Replying to multiple posts.]

On Fri, Mar 8, 2019 at 1:17 AM Lassi Kortela <xxxxxx@lassi.io> wrote:
> So you'd basically like to write ML/Haskell/Idris-style static type
> definitions for everything defined in the SRFIs (as far as Scheme's
> dynamic nature permits). [...]
>
> The reason I didn't understand what you meant, is I thought we were just
> transcribing the argument signatures as written in the SRFIs into a
> machine-readable form. But you would also like to formalize things that
> are implied but not explicitly written (or are written in prose or
> mathematical symbols, but could be converted to a formal definition for
> a type checker with some manual work).

Exactly.  :)

> So this is a *lot* more of a far
> reaching project than the rest of us were pondering and I think a lot of
> the confusion came from the fact that we didn't understand this.

Yes, it would be a lot of work, but I think it can start somewhere,
and in my view I think one such first step is documentation.  (I.e.
based on these "signatures" one can generate better documentation.)

> For starters, is there a generally agreed-upon way to write the
> types? Type systems are an active field of research and enthusiasts are
> constantly debating which kind (no pun intended :D) is best.

Frankly I have no idea, as I didn't studied this domain in depth.  As
said above a first step would be to generate more "enhanced"
documentation, and permit afterwards some type of static checking like
Erlang's `dialyzer`.

(And part of that generated "enhanced" documentation is the "prose"
which is why I focus on a more structured SRFI document format.)

> Transcribing the definitions written in the SRFI as-is is quite
> straightforward, but once you get into things that could be inferred
> from that information, it becomes less clear how much information to
> include. It's basically an open-ended research/development project. As
> such, I wonder if whether the SRFI repositories are the right place to
> house something that's so researchy/actively developed.

I agree that what I am proposing is perhaps out-of-the-scope of SRFI's.

However at the same time I debate what is the usefulness of the
"partial" signatures you can automatically extract from the HTML, vs
the cost of adding the markup.

> My personal motivation would be just to transcribe the simple things
> written in the SRFIs into a machine-readable form, preferably quite soon
> :) All the other work proposed here is awesome too, but I'm ambivalent
> about how its the timeline and scope fit with the simpler and more
> immediate goals originally proposed.

As hinted in the previous paragraph:  what would be the actual
usefulness of such partial signatures?  How would you use them?

Because if we don't find a good-enough use-case (one that would
counter-weigh the cost of adding this enhanced markup), then perhaps
adding such a markup (although a good idea from a technical point of
view) would not be worth the cost.

On Fri, Mar 8, 2019 at 1:28 AM Arthur A. Gleckler <xxxxxx@speechcode.com> wrote:
>> [...] At the same time, this might necessitate quite a lot of
>> edits to the definitions as the type checker is figured out over the
>> years. The SRFI repos were originally made to track the documents; they
>> would now track both the documents and the exploratory type checking
>> work based on them.
>>
>> What does Arthur as the editor think about this?
>
>
> I'm happy to have the SRFI repositories be the home of these files if they don't change, collectively, more than every few months — or more often when they're new.
>
> [...]
>
> So I do have a limit.  Still, it would be great to have all this information, which applies to all Scheme implementations, gathered together with the corresponding SRFIs.  So let's start with that assumption.

I don't know if the signatures should or shouldn't be part of the
actual SRFI repository.

I think a better place would be in a completely different "common" repository.

> > (BTW, do you know of such a introspection tool?)
>
> Nope. I thought you might have used one to obtain your definitions :)

Nop.  I've studied the documentation, and tried to "formalize" what it
"said" in prose.

On Fri, Mar 8, 2019 at 2:24 AM Lassi Kortela <xxxxxx@lassi.io> wrote:
> > If I recall, Ciprian's format is extensible, so we could start by
> > extracting, one way or another, simple type signatures, then add more
> > information as Ciprian and others produce it.
>
> If we are going to developing the static type signatures in the same
> S-expression file where the straightforward transcribed stuff lives,
> then we just have to come up with some compromise on its format :) We
> could also have them in different S-expression files, but I think it's
> better if we work to find a way to fit everything in one file in such a
> way that everyone is mostly satisfied. It causes less duplication, is
> more likely to be correct, and is probably easier to maintain long-term.

I see nothing wrong with multiple files.  The "automatically
extracted" signatures could live in separate file than the "manually
formalized" signatures.  Moreover there could be a simple tool that
would cross-check any discrepancies between the two.

> The first conundrum with the argument signatures is that the Lisp
> tradition tends to think a function has only one signature (possibly
> with optional args) and the names are the main thing, like:
>
>      (make-vector k [fill])
>
> Whereas the functional tradition likes to emphasize types and break it
> down to the possible type combinations like a case statement:
>
>      (make-vector
>       ((range-length-zero) -> vector-empty)
>       ((range-length-zero any) -> vector-empty)
>       ((range-length-not-zero) -> vector-not-empty)
>       ((range-length-not-zero any) -> vector-not-empty))
>
> Unfortunately, the functional signatures are notoriously hard to read
> for people from other traditions because the types are so detailed and
> the argument names are omitted or de-emphasized.

Please note that the above signature doesn't include argument "names"
because I haven't actually added them in the signature, however the
underlying format does support them.

Also note that I "broke" the "range-length-zero" and
"range-length-not-zero" (which are in fact just integers) for the
following reasons:
* to make it clear that a negative value is not allowed;
* to make it clear that "zero" is a special case;  (however this isn't
such a "special" case for vectors, but for `sqrt` it is quite
important);

  https://vonuvoli.volution.ro/documentation/libraries-html/r7rs/definitions/sqrt.html#definition__r7rs__sqrt

Also in case of `list-copy` I clearly want to markup that a circular
list would raise an error:

  https://vonuvoli.volution.ro/documentation/libraries-html/r7rs/definitions/list-copy.html#definition__r7rs__list-copy

> We would have to find some notation that combines these quite opposing
> traditions. We could also write them separately, but any duplication is
> a chance for discrepancy.

The format I proposed supports both.  (The variant of `make-vector`
above is just a "specialization" of the more "traditional" format.)

> Ciprian, have you already thought a lot about how to combine these
> representations? The syntax you have so far looks like it's directly
> from the functional tradition. Did you come to the conclusion that this
> would be the best one?

As said above it supports both "formats".  However I preferred the
more "explicit" one that covers also the corner cases.  Again taking
the `sqrt` function, we could state that it takes a real number and
returns a complex number, and it would be "mathematically" correct as
any real number is also a complex number.  However if I give it a
positive number I would always receive a positive number, therefore I
made this as an explicit case.

  https://vonuvoli.volution.ro/documentation/libraries-html/r7rs/definitions/sqrt.html#definition__r7rs__sqrt

Ciprian.