Re: Typed exceptions

[address@hidden (Paul Steckler)]

Neel Krishnaswami wrote:
> Now there's some real information here. The compose function
> might have a type like
> 
>   compose : (a -> b throws x, c -> a throws y) -> (c -> b) throws x+y
> 
> where 'x + y' is the union of x and y. I left this kind of stuff out
> of Needle, mostly because I have zero experience with polymorphic
> effect systems, and the typechecker was hairy enough as is. Matthias
> could likely comment further, because IIRC the PLT MrSpidey tool works
> using set-based analyses.

MrFlow, the forthcoming successor to MrSpidey, uses type for primitives
to guide its analysis.  The assumption is that type schemes represent 
truly parametric-polymorphic functions, so that information from a 
type variable in negative position flows to the same type variable in 
positive position.  So info could flow from your x and y on the left 
to the x+y on the right.

MrFlow uses a closure analysis to do much of what Spidey did via 
SBA, but in less time.

-- Paul