[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.
