[plt-scheme] static checking, mrflow?

Robert Nikander wrote:
>It's page says "coming soon" -- how soon?

It's not dead, but it's in need of a rewrite...  I've been saying
"soon" for a long time now :-)

>If there are no docs or intro papers, can someone tell me 
>what it does, or point to some papers that describe the theory that it 
>implements?

There are quite a few papers about 0CFA.  Look for example at Olin
Shivers's older papers for a start.

>Does it subsume the idea of a type system?

There are equivalencies between some flow analyses and some type
systems, in general.  In practice MrFlow is often able to keep track
of the shape of data structures more precisely than an ML-like type
system.  For example MrFlow will be able to differenciate between
(cons 1 '()) and (cons 1 (cons 2 '())), so it will flag
(cadr (cons 1 '())) as a potential error but will accept
(cadr (cons 1 (cons 2 '()))).  An ML-like type system would simply
type both (cons 1 '()) and (cons 1 (cons 2 '())) as "list of ints" and
would then type-check (cadr (cons 1 '())) just fine (it's a category
of errors your usual ML-like type system is just not attempting to
detect, though more powerful type systems exist that can do that, see
for example Dependent ML).

>Will it infer or allow annotations for function types, like the 
>following imagined notation for `map':
>
>map : ('a ... -> 'b) (list 'a) ...

Eventually it will understand Robby's contract language, so putting a
contract on a function at a module interface will make MrFlow use the
contract instead of the functions's code.  At least that's the plan.
See our POPL'06 paper for the gory details.  Currently though, for
primitives like map, MrFlow uses an internal type-like description
that vaguely resembles what you have above, except restricted to a
known number of arguments (i.e. MrFlow doesn't currently have any
internal equivalent of your "..." notation).

>Will it catch this type error?
>
>(map string-append (list "a" "b") (list 1 2))

Yes.  The error message tells you that "(union 1 2) not a subtype of
string".

>Or this error?
>
>(map string-append (list "a" "b") (list "1"))

No.  MrFlow can keep track of the length of (list "a" "b") and of
(list "1"), but the type-like internal description of map used by
MrFlow does not attempt to compare those two lengths.  For that you'd
need a type-like description language that is similar to what you have
in dependent type systems.  One day maybe...

Note: even for a correct expression like
(map string-append (list "a" "b") (list "1" "2"))
MrFlow would compute for the result of the whole expression the type
"list of strings", not the type "list of strings of length 2", for the
same reason: computing the more precise result would require the
description of map to use something akin to a dependent type.

Philippe