[Grace-core] Types of blocks

[Michael Homer]

Hi,
I've begun working on typechecking in my implementation, and have a
(primarily nominal) static checker working almost everywhere. There
are no generics so far, but I've begun thinking about how the typing
of blocks will work. To begin with, just how do they work? I have been
presuming they are genericised in the parameters and return type
somehow, but exactly how that should look is a little hazier,
particularly if a) blocks can be variadic or b) there is a meaningful
common supertype of blocks.

As well, there are a couple of points about where those types come
from: what exactly is inferred? It seems like the most obvious result
is the disjunction of all possible return types, but there are other
sensible answers too. What about a block containing a "return"
statement (which hence "returns" nothing at all)?

Can blocks take generic parameters? By that I mean code like this:
    { a : T -> Proxy.new(a) }
where "T" is a fresh type identifier. Is that permissible? How is that
typed, and where does inference go through them? Especially, how does
the "apply" method turn out in this case?

I am also interested in how generics and reified types will work more
generally, but as I said I haven't started implementing them at all
yet.

If anybody wants to look at what's there, my typechecker does run in
the JavaScript version [1], and currently supports the types Number,
String, and Boolean, along with any user types defined with "type X =
{ ... }", and union types with A | B. Values can move freely in and
out of type Dynamic, with no casting and currently no runtime checking
either. It checks the existence of methods and that argument and
parameter types match, along with assignments, but does only very
limited structural matching. There are test cases at the bottom
showing how it behaves.
-Michael

[1] http://ecs.vuw.ac.nz/~mwh/minigrace/js/