[Grace-core] Types of blocks

[Kim Bruce]

On Aug 22, 2011, at 12:08 AM, Michael Homer wrote:

> 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.

Each block has a signature that is our representation of function types.  If it has parameters a:A, b: B and returns a result of type C then
the type is Function(A,B,C) (informally), which translates to an objecttype with an apply method with parameters of type A, B and return type C.
> 
> 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)?

In general you would take the sup of the return types (which happily exists in a structurally typed language).  The return type of a block is the type of the last statement in the block (treating a stand-alone expression as a statement).

Most commands will have type Unit.  E.g., the statement x:= 12 will have type Unit, not Number.  Similarly, a bare return statement will return a value of type Unit.  Our interpreter doesn't actually have return statements.
> 
> 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?

I would say no to that.  However, I would be tempted to allow something like 
	[T]{a:T -> ...}
though you'd probably be more likely to actually name it:
def f[T] = {a:T -> ...}

At any rate, I would worry much about these -- ignore them for now.

> How is that
> typed, and where does inference go through them? Especially, how does
> the "apply" method turn out in this case?

There would be no type inference.  Do you have a compelling example as to why we should include this?
> 
> 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.

I think the generics should be relatively straightforward, and we discovered (much to our surprise) that we didn't need to reify the type parameters because they just got substituted in structurally.
> 
> 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/
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core