Lambda the Ultimate

The Role of Type Equality in Meta-Programming (Emir Pasalic)

Meta-programming, writing programs that write other programs, involves two kinds of languages. The meta-language is the language in which meta-programs, which construct or manipulate other programs, are written. The object-language is the language of programs being manipulated.
We study a class of meta-language features that are used to write meta-programs that are statically guaranteed to maintain semantic invariants of object-language programs, such as typing and scoping. We use type equality in the type system of the meta-language to check and enforce these invariants. Our main contribution is the illustration of the utility of type equality in typed functional meta-programming. In particular, we encode and capture judgments about many important language features using type equality.
Finally, we show how type equality is incorporated as a feature of the type system of a practical functional
meta-programming language.

An interesting investigation by Emir Pasalic into meta programming and its relation to both dependent typing and multi-stage programming, among which an exposé of the development of Omega (see also: Tim Sheard ).

After doing C++ for years, with some Java/C# here and there, I've gotten around to doing some web development and have started playing around with Javascript. With the recent Ajax and "web 2.0" hype, Javascript seems to be getting more attention.

I've been curious about Prototype based Object-oriented languages for a little while now, but have never used one extensively as modern, widely-used implementations (except for Javascript) seem to be rather scarce. Slate seems to be still in development though. Here is a LtU discussion that concentrated on memory concerns and here is a paper on Self.

What are others thoughts on OOPLs. Is the added flexibility that proponents argue needed to be looked at more? What are the pitfalls and advantages? Do languages like Ruby "fake" it well enough? I'd be particularly interested in the psychological criticism given in this (google cache)paper, as well as this paper.

Hi guys,

I would like to share with you a silly experience that happened over the weekend that got me thinking about object orientation/classification and how it affects, (and was affected by) the different ways in how individuals classify and manage bits of information or real objects in the world around themselves.

I recently bought a painting for my girl-friend's lounge, but I didn't get a chance to put it up for her over the weekend, so she got her father to come around to do it for her. He brough along his toolbox (he sells professional tools (Snap-on, KingTony, etc) for a living, so he's a DIY type through and through). Something came up however just as he was about to put the painting up, so he just neatened everything up and left the tools there for me to use.

The art gallery I bought the painting from, kindly and conveniently included a number of frobbitzim, such as hooks, masonry nails, wood screws for the frame, string, etc, all in a little plastic bag.

So last night I get a chance to put the painting up, and lo and behold, the plastic bag with all the goodies is nowhere to be found.

Aggravated, and cursing and muttering, I strip-search the apartment, including her father's toolbox, and the baggie is still nowhere to be found. So Iresort to looking in the trash. There it is, the plastic bag. But empty. And the goodies are not in the trash along with it.

So I go take a close look at the toolbox. My g/f's father decided that, as part of the neatening up, the frobnitses needed sorting as well. His toolbox includes one of those organiser things on the side, so he put the the screws along with their little friends in the screw compartment, the masonry nails along with the existing nails in the nails compartment, and the hooks in the 'misc' compartment, and so on. The string defied classification so it ended up in the bottom of the toolbox. The baggie itself ended up in the trash because it didn't have a purpose anymore.

So here I am aaarghing away, scratching through all the compartments to find MY frobbnitzes, all the while muttering under my breath: why?....why?....why oh why oh why?

All of this was perfectly acceptable to my girlfriend as well, who obviously thinks exactly like her father. To them, it's perfectly logical to classify and group things according to type, instead of according to function. To my way of thinking, the plastic bag was a perfect object that encapsulated all of its members, and the whole's purpose was OBJECT_TYPE_FOR_ERECTING_PAINTING, so leave it be, darnit!

To me it doesn't matter that a screw is of type TScrew, what was important to me was that I had a number of different types that belonged together as a functional whole, grouped according to one singular purpose. The object-oriented programmer in me was screaming inwardly at what I thought to be a very illogical thing to do, but obviously the difference is in human perspective and way of information classification.

I wonder now if OOP is not hard for some programmers to grasp simply because intuitivly they classify information according to type instead of function, and because they think in terms of data pools that are manipulated using functions or operators.

From an aside in a paper on functional graph algorithms, using monads means you have given up on a functional approach. Unfortunately, the procedural approach might be ugly or confusing and we are left still pining for a functional solution. When and how could we use functional approaches and avoid monadic / procedural? What are the limits of our abilities with functional programming?

After spending some time thinking about the static vs. dynamic debate, I clarified my own thinking on the topic by defining some terms. I propose the following names and definitions for your consideration:

• Simple Type - The set of values to which an expression may evaluate. The type of '1 + 1' is {2}.
• Complete Type - the pair containing the set of types to which the free variables in an expression may be bound and the Simple Type of the expression. The Complete Type of 'int f(int x, int y)' is {{int, int}, int}.
• Logical Type - The intended Complete Type of an expression. This concept is a function of a program's design. The Logical Type of 'int operator /(int, int)' is {{int, int - {0}}, int}, even though its Declared Type is identical to that of f above.
• Static Type - The actual Complete Type of an expression as implemented in a particular programming language. The Static Type of 'operator /' is identical to the Logical Type in most PLs, because division by 0 is undefined. Note that the Static Type exists whether it is declared manifestly or explicitly defined or not.
• Dynamic Type - The Complete Type of an expression as determined by a runtime evaluation of the expression. The Dynamic Type is parameterized by a set of argument bindings and evaluations. The Dynamic Type of '!a' is {true} for the evaluation {a = false}. Note that the Dynamic Type of an expression for a given execution of a program may be smaller than the expression's Static Type.
• Declared Type - The Complete Type of an expression as declared in a specific PL. This corresponds to the type signature of an expression in languages with manifest typing. The declared type is usually bigger than both the Dynamic and Static type.
• Explicit Type - A Simple Type as defined independently of an expression. Enumerations and user-defined object types are Explicit Types.

So why all the fuss? Well, I realize that PLT has perfectly good terms and definitions for types, but they aren't convenient to use when discussing the static vs. dynamic debate. Also, I think these terms might help to clarify different positions in the debate (though it's possible they only clarify things in my own mind). So, let me explain what I see as the relevance of these terms.

It should be obvious that the goal of a good type system is to enforce the Logical Type of an expression. It should be equally obvious that this goal has a significantly increasing cost with the rising complexity of the expression, all the way up to undecidability. So the compromise of an SC type system (SCTS) is basically the 80/20 rule - do the 20% of the typing work that produces 80% of the benefit. That usually means modelling subtypes with their most general supertype. That is, few to no PLs will statically check the validity of a type Even, because it would impose too great a burden on all expressions involving Even. Rather, the language will usually statically check the supertype of Even and dynamically check the subtype. What this means is that the Static Type of 'Even operator+(Even, Even)' is almost certainly '{{Int, Int}, Int}', even though the Logical and Dynamic Types of the expression are at least 8x smaller. And the Static Type is what the SCTS checks at compile-time.

The fact that the Dynamic Type (and the Logical Type) is often smaller than the Static Type may be what leads the DCTS camp to decide that SCTSs are not really an improvement. On the other hand, contracts can make the Static Type of an expression as small as the Logical Type, though at the cost of runtime checks. The SCTS camp claims that you don't need that level of precision for most tasks, and that even DC coders don't invoke that much precision for most code. By approximating the Logical Type with a suitably simple-to-check supertype, a large number of errors can be eliminated with the help of automated checking from the compiler.

Note that what some people call "latent types" I call "Static Types", because they are just as real and active whether you name them or not. It's just that in DC languages, they are anonymous and implicit. Some people argue that you can create Explicit Types in DCTSs; but those types will not be automatically checked by the compiler, which may or may not be a good thing, depending on the context.

Also, I changed my mind on the meaning of Dynamic Type. I decided that you can't change the type of an expression at runtime, because any information that could be used to make such a change should simply be regarded as an input or free variable of the expression. Therefore, changing the definition of an expression yields a new expression. I think the new definition of Dynamic Type makes more sense and is useful for talking about what actually happens vs. what could theoretically happen.

Now, when it comes to Contracts-as-Type-Enforcers, I maintain my claim that any contract can be checked statically. And that's because the Static Type of an expression is fixed by the definition of the expression itself, and cannot change at runtime. Contracts-as-Assertions are a whole different ballgame, and I have no particular comment on them. However, the cost of converting a contract-declared type into a statically-checked type may be arbitrarily high, which is why contracts are useful. On the other hand, contracts have the flaw that they don't write themselves in a DCTS, whereas they magically do in an SCTS. The fact that they are not perfectly defined in an SCTS should not detract from the fact that they are automatic. In fact, the case should rather be made that runtime contracts ought to be used to *augment* static contracts inserted by the compiler.

Of course, the objection is that sometimes static contracts *overspecify* the type of an expression, and tricks must be performed to expand the type. The reply is that Dynamic types can provide a suitably large type for such instances while still preserving most of the rigor of the static contract system. After that, it boils down to an argument between soft typing and Dynamic. My understanding is that these approaches are the dual of each other. That is, soft typing infers the Static Types in a program that are reasonably small and eliminates the checks for them, leaving the rest of the types to be dynamically checked. That is, softly typed languages *infer the static contracts* and *make explicit the dynamic ones*. Where more static checking is desired, types may be explicitly annotated for better performance. On the other hand, languages with Dynamic *spell out the static contracts* and *infer the dynamic ones* from the uses of the Dynamic type.

It seems to me that the results should be equivalent in the limit, and the only difference is the choice of starting point.

Morning everyone. I have a question about the internals of Lisp (as a family) and I came here hoping someone may be able to answer my question.

I just recently watched the Rainer videos again, and I was completely amazing at the reflective, or maybe the proper word is introspective capabilities of Lisp, espicially while a program was running. So I finally decided that I wanted to know how this was possible, and why it was implemented in more languages to such a scale. What portions of Lisp contribute to this? Is there one specific feature, or is it more like a group of features?

Thank you everyone.

-M.

I recently found that the name I had chosen for the language I am creating had already been taken. So now I am in search of a new name. I realized that a number of the LtU readers create and name their own languages in the course of their language tinkering/research. I thought we my enjoy discussing some name related issues.

First, the way I see it there are two schools of names. First there are names for languages that are never meant to be mainstream. Second there are names chosen expressly with the intention that the language be mainstream. Of course language designers often misjudge whether their language will be mainstream or not. I imagine that languages not meant for the mainstream are easier to name because the name isn’t as important.

Some discussion questions:

1. Do you agree that whether a language is intended for mainstream use at the time of naming affects the name?
2. What makes a good name? A bad name
3. What do you think of names which are simple words seemingly unrelated to programming? I.e. Perl, Ruby, Java, Python etc.
4. What do you think the many gemstone language names? Perl, Ruby, Opal etc
5. What do you think of the letter names and their variants? C C++ C# etc.
6. Can you reuse the name of an obscure language for a new mainstream language? (but which languages are obscure enough)
7. How do you pick a language name?
8. Does any of this really matter?

The charming people over at Slashdot are presently discussing how SQL could be improved. The usual trolls and bad jokes are of course present. But there are also a few interesting discussions, as well as references to LINQ and Tutorial D.

I recently put together video-iPod compatible feed of the classic SICP lectures.
Grab the feed: http://feeds.feedburner.com/SICP
(video RSS adventures documented here)

Although my previous post, translational vs. denotational semantics, failed to stimulate any discussion, hopefully this one will.

Consider the following excerpt from Brian Meek's well-written The static semantics file.

[...]

term = factor | term, multiplying op, factor;

and

term = factor, [multiplying op, factor];

apparently mean the same (square brackets = zero or more repetitions). However, the recursive version better expresses the associativity from left to right. [...]

[...] The order of evaluation of an expression like a + b * c is undoubtedly semantic (linked to code generation, see later) but the use of recursion above only hints at the semantics (to use a phrase from a later electronic correspondent); it is descriptive, not prescriptive. The difference is that the expression can be generated by either rule (or by one implying right to left associativity). [...] The semantics gets put in at code generation and that can be done from any of the equivalent definitions. [...] [I]t appears to me to be the nearest approach among the examples put forward to anything which could be termed "static semantics"; it is perhaps a borderline case.

This seems a bit "off" to me. First of all, how "a + b * c" is parsed is a question of operator precedence, not operator associativity. Second, and more importantly, it seems to me that parsing is clearly a syntactic issue unless you view the semantics of a language as being defined with respect to its concrete rather than abstract syntax.

Such a view can be reconciled with the more traditional "semantics is defined with respect to abstract syntax" view in the following manner. Let language L's "broad" semantic function be defined as the composition of L's parser with L's "narrow" semantic function. Another (perhaps weirder) way to look at it is to view the parser as defining a language in its own right, with the abstract syntactic domain of L being the parser's semantic domain. To put this all in Haskell-ish notation,

parser :: ConSynDom -> AbsSynDom

narrow :: AbsSynDom -> SemDom

broad :: ConSynDom -> SemDom

broad = narrow . parser

Another way of looking at this is that syntax can of course be viewed as merely discriminating between valid and invalid sentences, or it can be viewed as including the parsing of sentences if they are valid. The former, "boolean" role for syntax pushes parsing issues somewhere else, perhaps into pragmatics, perhaps into semantics, or, perhaps into some ill-defined area called "static semantics." This last option is of course what Meek is writing about.

So, if all we're looking for from a grammar is whether it can generate a sentence or not (the "boolean" role) then, as Meek mentions, it need not deal with ambiguities arising from issues like operator precedence and associativity. Maybe this "boolean" role is what Meek calls a "descriptive" role. The grammar merely describes what valid sentences look like. But I'm having problems relating how a "prescriptive" role includes parsing. Would this mean that an unambiguous grammar, i.e. one capable of parsing, is "prescriptive" in the sense that it tells you where you "should" have put parentheses? Seems like a stretch.

Anyway, my final take is this: I think I agree with Meek in the big picture. Different languages draw the syntax/semantics line in different places, but it is always there, and there is nothing useful in between called "static semantics." One of the ways in which you can move the line so that the semantics is bigger is to define the syntax ambiguously with regard to operator precedence or associativity. Then these issues must be defined by the semantics. In the extreme, you could define the syntax of a traditional textual language merely by the character set its programs are expected to be in, leaving everything else to semantics. But in practice this is not a useful way to define a language.