Lambda the Ultimate

Nominal types, such as classes and interfaces, give us names to "hang" other names on - methods, data member names, nested types and classes, etc. Interfaces/mixins/traits provide some challenges vs. the well known single inheritance "v-table" of virtual methods, but I found an interesting IBM paper on efficient execution of interface defined methods.

So my question is: What about structural types? The structural types used for (among other things) the "static duck typing" that Scala most recently has brought to general attention?

What is a means for a) correct and b) efficient execution of method resolution, data member access, etc.?

To make it interesting, consider two examples.

-- One structurally typed argument
fun print-name(thing : { .name(-> Str) }) =
  print(thing.name());

-- Arg is List of structurally typed things
fun print-names(things : [ { .name(-> Str) } ]) =
   for x <- things in 
       print(x.name());

I considering the first case and thought that the compiler could pass a hidden function parameter, or some indexes that provide a route to a method in a table of the parameter.

But then I considered the second case, and my (relatively speedy) scheme fell apart. In the second case, any given item in the list could (1) be some object whose class defines a virtual or final .name method, noting that final methods don't typically show up in vtable/RTTI type data; (2) it might be an object that implements a .name method required by an interface; (3) it might be an object who gets an actual .name method definition from a mixin/trait; (4) or it could be some object itself instantiated (via new) directly from some unnamed structural type.

I don't see a way to distinguish this mess of cases until runtime, particularly in the second example of a list of structurally typed objects, and how to compile such code for efficient execution.

I tried CiteSeerX but didn't turn up any papers directly addressing approaches to analysis and compilation.

Any pointers? Thanks VERY much in advance.

Scott

p.s. (I'm very interested in this question because I think an answer might also help me to efficiently compile a set of general, functional record operators and record type operators described in a paper by Cardelli.)

Scott

Hi all,
I have a weird question that I've been trying to solve.

I've been reading about lambda calculus, specifically the different augmentations of lambda calculus. The ones that most interest me are the ones with some sort of state, like a store (mu). So my question is:

Given a term, t, in the (untyped) lambda calculus (or in a typed calculus which features full abstraction), is it decidable whether or not it ever modifies the state (updates some value in the store, etc).

My gut says that it's not decidable for all terms, but I want to PROVE it.

-Kevin