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.

Here's my favorite example from the Dialyzer paper at

I'm giving it as three rewrite rules in sort-of-Scheme syntax, where _

means "anything":

(define AND

(matching-rules ()

((AND #f _) #f)

((AND _ #f) #f)

((AND #t #t) #t)))

Conventional Hindley-Milner typing will type this function

as bool -> bool -> bool, but the true type is _ -> _ -> bool.

This still permits run-time crashes, as when you write

(AND #t 32), but it comes closer to the truth of what

really will work than Hindley-Milner. As another example,

success typing will type `car` as pair -> _, which means

that (car 6) will be rejected by the analyzer out of hand,

since that could not *possibly* work.

For starters, is there a generally agreed-upon way to write the
types?

There are many examples which differ only in details. Chicken's

and is as good as any. This is not about arbitrary dependent

typing.

We are lost, lost. No name, no business, no Precious, nothing. Only empty.

Only hungry: yes, we are hungry. A few little fishes, nassty bony little

fishes, for a poor creature, and they say death. So wise they are; so just,

so very just. --Gollum