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
manifest typing system is at <http://wiki.call-cc.org/man/5/Types>
and is as good as any.  This is not about arbitrary dependent
typing.

-- 
John Cowan          http://vrici.lojban.org/~cowan        xxxxxx@ccil.org
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