On Fri, Mar 8, 2019 at 2:36 AM John Cowan <xxxxxx@ccil.org> wrote:
> On Thu, Mar 7, 2019 at 6:17 PM Lassi Kortela <xxxxxx@lassi.io> wrote:
>
>> I think the static checker is a very nice idea but this brings a bit of
>> an impedance mismatch - it's basically an open research problem,
>
>
> It really isn't.  What makes Dialyzer-type tools straightforward is that
> they only verify types to the extent required to reject what is
> provably wrong rather than to accept only what is provably right.

Indeed this is true.  (Although Erlang's `dialyzer` can "propose"
signatures for your code based on what it "sees" in its usage.)

And I think such a use-case, of rejecting what is provably wrong, is
of a lot of help to dynamic-typed languages, especially in cases like:

* take for example the IO functions of R7RS which have as the first
argument the byte-array, then the port, and then the "slice" from that
byte-array;  this is counter intuitive for people coming from other
languages where in almost all cases the "file" is on the first
position;  (and I've been bitten by this issue quite a few times;)

* or perhaps functions which for ergonomy permit multiple optional
arguments, but based on the number of arguments change what their
meanings are;  (I agree this is a bad design practice, but one always
should weigh other factors against "best-practices";)

Ciprian.