[Grace-core] Types of blocks

[Michael Homer]

On Wed, Aug 24, 2011 at 12:49 PM, Kim Bruce <kim at cs.pomona.edu> wrote:
> These results make sense to me and I'd expect the same results in Grace.  If we added union types to Grace then we could use the union of the result types as the answer, which would give a more exact typing.  Note that this is really a matter of how we type an "if" statement not a block.  If's and matches are where these would show up.

Does this mean "return" is a syntax error inside blocks? If not, *how
does it affect the type*? If they all go to the top type then
obviously not at all, but otherwise there might be.

This rendition of the third block misses the point:
>  { (a : String, b : Boolean, c : Boolean) => if (c) { a } else if (b) { a } else { a.size } }
> res7: (String, Boolean, Boolean) => Any = <function3>
The original block contains two statements, one of which may prevent
the other from executing at all. If the type of a block is determined
strictly by the type of the last statement, that must have a different
type than the one with the return as a branch of the if-then-else.

If a return statement does not contribute to the type at all, then the
first and second blocks have the same type String | Number; if it is
treated as a return value of Unit (which is never accessible), the
second and third have the same type Unit | String | Number; if the
mere *presence* of a return statement affects the type then the
second, third, and fourth have the same type, but otherwise the first
and fourth do.

1: { a : String, b : Boolean, c : Boolean -> if (b) then { a } else {
a.size } } -> String | Number
2: { a : String, b : Boolean, c : Boolean -> if (c) then { return a }
elseif (b) then { a } else { a.size } } -> Unit | String | Number OR
String | Number
3: { a : String, b : Boolean, c : Boolean -> if (c) then { b := c }
elseif (b) then { a } else { a.size } } -> Unit | String | Number
4: { a : String, b : Boolean, c : Boolean -> if (c) then { return a }
; if (b) then { a } else { a.size } } -> Unit | String | Number OR
String | Number
And a new one, showing that it isn't really about the type of "if":
5: { a : String, b : Boolean, c : Boolean -> if (c) then { return b }
; def d : String | Number = a ; d } -> Unit | String | Number OR
String | Number

There is also the possibility that "containing a return statement" is
a distinguished type of its own, which would be a third option for
those blocks.

In essence: how deeply do I need to inspect the block in order to
determine the type? My hope was for "not very", but that makes for
some wrinkles like those that may be undesirable.
-Michael