Lambda the Ultimate

Fair point.

Naked Objects is certainly generic but not terribly practical - see Fixing a Generic UI (Clothing Naked Objects).

I tend to agree that the term polytypic programming is late to the game and only useful as a vague umbrella concept.

If we need to create terms for categories of generic programming, then I think it would be better to start by explicitly classifying existing genericity techniques, e.g. type genericity (polymorphism, with an emphasis on state rather than methods), invocation genericity (method or behaviour polymorphism), structural genericity (Visitor or Bulider or Clone patterns) or algorithmic genericity (C++ templates or Java generics) or representation genericity (e.g. everything is an object or a string, possibly annotated with a type).

Another dimension of classification could include the implementation aspects - dynamic lookup (polymorphism), introspection-orientation, common data and schema formats (e.g. XML and XML Schema).

Under this classification, Naked Objects is simply polymorphism with introspection (assisted by naming conventions).

Hi Tim! Long time, no talk. It's a shame things didn't work out for me to join Epic, but I continue to look forward to forthcoming Unreal technology. :-)

One thing that I've always found fascinating about UnrealScript is that, like Java to some extent, it's a statically-typed language, but without full type erasure: it obviously supports some level of reflection and/or introspection, and all this while being well-integrated with C++ so that you can have native functions, latent functions, and so forth. I remember trying to explain to my stepson why it was impressive that, from the Unreal console, you can say something like "summon xweapons.redeemerpickup" and have a Redeemer pop into the world in front of you. So I'm wondering if you have any (more) comments about reflection and introspection, type erasure, etc. in the context of your current thoughts on type theory and language design. Perhaps more specifically, to the extent that your thinking is influenced by Ontic and doesn't make a strong distinction between types and values in the first place, what do "type erasure" and/or "reflection/introspection" even mean? And how would all of this be integrated with C++? Or would answering these questions give away too much of the farm?

But in Rails, the persistence layer must exist *first*, in order to derive the the domain object definitions, which is the reverse of what was described for Naked Objects: "persistence layer can be generated completely automatically from the domain object definitions."

Nitro (well, Og, actually) generates the persistence layer (usually a database and tables) from the domain object definitions (the Ruby code for the models).

(Though I wonder if we have different ideas of what "persistence layer" and "domain object definitions" map to.)

So the main point I take from this is that arbitrary introspection/reflection should be disallowed. That seems reasonable. PLT Scheme has one take on it with it's inspectors.

However, reading the posts the prior posts the main criticisms boil down to: you need more customisation than these automated procedures provide. This is where, I think, PL theory can make the largest contribution.

Imagine the process of constructing a GUI from a type definition. This process is a fold over the type. Simple stuff. Now how about customisation? We want to replace some parameters of the fold with our own functions. Again, fairly simple. Now what if there are dependencies between elements? We might need to alter the traversal order, and so on. Structuring all of this cleanly is what we can get from the theory. Strategic programming, and Stratego are the first places I'd look for ideas.

A lot of application development is just writing a nice front-end to a database (say, about 90% of websites are just this). If this could be made this really easy, and yet really customisable, it would be a great tool.

Noel: Imagine the process of constructing a GUI from a type definition. This process is a fold over the type. Simple stuff. Now how about customisation? We want to replace some parameters of the fold with our own functions. Again, fairly simple. Now what if there are dependencies between elements? We might need to alter the traversal order, and so on. Structuring all of this cleanly is what we can get from the theory.

This sounds like Oleg Kiselyov's work on General Ways to Traverse Collections. I still think his "Zipper qua delimited continuation reified as a data structure" is the most important CS result of 2005. I'm still waiting on an O'Caml implementation, however, as I don't yet understand the module system well enough to develop my own. I really should keep trying, though.

I think there is bit more here than just a universal traversal. Composition is the main additional problem. I don't want to specify my traversal as one monolithic lump. I want to specify individual rules which might require bottom-up and top-down traversal and have some smart system combine them into one uber-fold. Perhaps Oleg addresses this -- I haven't read all his work -- but it isn't in the work I have read. I seems like a neat problem very related to existing work in deforestation, so I wouldn't be surprised if someone has implemented it.

But, given just a value of some arbitrary type, one should not be able to extract its "type", since that notion violates many universal properties (such as the subtyping property).

That doesn't make sense to me, but I am a caveman when it comes to PLT. Perhaps "the subtyping property" explains why I'm being dumb. Pattern matching isn't considered evil so why shouldn't I be able to get the metadata for something and then have my code take different paths based on that? (The main argument I can think of: a better design is to make that kind of stuff more explicit at the regular type level, rather than relying on metadata.) As long as the code isn't trying to change the metadata it should be safe, no?

PDF

deriving Typeable does what you're thinking?

So the intuition here is that if I declare a type "deriving Typeable", then I'm explicitly choosing to expose its internal details. But abstract datatypes not declared that way remain abstract such that it's physically impossible for an outside function to break the abstraction barrier.

Actually, Typeable just provides a way to compare two types for equality. To do introspection, you need Data.

In other words, a value of type ∃a.a is completely opaque; a value of type ∃a. Typeable a ⇒ a lets you check whether a is a type you're familiar with, but doesn't give you any extra information if it isn't; and ∃a. Data a ⇒ a lets you look at the internal structure.