[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Whither MrFlow?




SBA is Set Based Analysis, the theoretical framework for MrSpidey and
MrFlow. We used two different varieties as Paul explained. The basic
idea is that you set up inequations between the expected sets of values
that flow out of an expression and into function parameters. Then you 
solve those inequations. The result is a conservative estimate of the sets
of values in your program. 

HM is the theoretical framework for type inference in SML and OCAML.  Your
language comes with a type language but the programmer is allowed to skip
type annotations for variables. The programming environment, usually the
front-end of the compiler, restores the missing types. To do that, you set
up equations between type variables that are assigned to expressions and
parameters. The type constructors are from the given type language. You
solve the equations (with an adaptation of Gaussian elimination to the type
algebra). The result is a principal type for each type variable.

The first difference between the two is that SBA infers sets of values, HM
infers types. I do think that one could turn SBA into a type inference in
the sense of ML but (TMK) nobody has done so. 

The second difference between the two is that solving inequations is a
directional process and solving equations is a non-directional process. 
If you get an unexpected "thing" (aka error), this becomes important. 
With SBA you can explain the "thing" via a flow diagram, that is, a path
from a value to the site of conflict. That's because your solution contains
the flow path. With HM you cannot, because your solution does not contain
the flow path. It is therefore on occasion extremely tricky to understand
and debug type errors. In particular, because it is a type error and not a
bad value inference, you cannot run the program and therefore you cannot
use the dynamic debugger to understand the problem. 

Due to historical reasons, typing and type inference are much more
ingrained in programmers and much more wide spread. Using a static debugger
`a la Spidey or Flow (very soon) requires different training. 

-- Matthias