Lambda the Ultimate

I know that LLVM has arbitrary-length integers that could be used for tagged pointers as follows, for example:


type TaggedPointer = [i30,i2]

function taggedPointer<T>(p: @T) {
cast<TaggedPointer>(p)
}


This would require a bit of boilerplate code, but adding a language construct to appeal to programmers assuming the bit-width of pointers.... seemed wrong somehow. With subtyping and physical subtyping now cleanly separated in the type system, it's certainly a good idea in search of an elegant implementation.

Could you clarify what you mean by declarative memory assignments? Googling the term brings up neurology papers.

adding a language construct to appeal to programmers assuming the bit-width of pointers.... seemed wrong somehow.

For most code, it is wrong. But there's a lot of low-level code out there that does need these sorts of representation, like language runtimes, garbage collectors and page mapping logic as found in kernels. For instance, Haskell sometimes uses 2 low-order bits to represent a sum tag.

This is why BitC includes a standard optimization in the spec for representing certain tagged pointers, although even BitC's implementation is rudimentary at best (it can't solve the Haskell sum tags for instance).

Like I said, it's one really hard abstraction to represent safely, which is why I always look for it first in any new systems language.

Could you clarify what you mean by declarative memory assignments?

Sorry, I just literally mean assigning a fixed memory location. In C/C++:

int* p = (int*)0x23aef4b;

Been a few years, but in Ada, it's something like:

p'Address := 0x23aef4b;

Assigning fixed addresses is required in driver code that integrates directly with hardware.

Edit: if pointer alignment were tracked in the type system, this would allow for word-sized tagged unions. This way the compiler could verify that X low-order bits are available for 2^X cases contained in those bits.

Well, now that subtyping and physical subtyping are cleanly separated in the language, rewriting the numerical types to just specify their bit-width (eg: int16 for signed 16-bit, nat32 for unsigned 32-bit) would work. I would just have to define width-subtyping correctly over integers and make a special case for the long integer to FP128 subtyping. The width-subtyping there could also enable physical subtyping on integers... nice.

As to assigning fixed addresses, it's doable via escape-hatch in Deca. You would CAST from the integer form of the address to an appropriate pointer type. CAST is Deca's unsafeCoerce: it will let you subvert the type system arbitrarily, make it believe any assertion of safety that you please, but on your head be the consequences of your own mistakes.

I would call that the philosophy behind Deca: "you can shoot yourself in the foot... provided you turn off the safety first."

As to assigning fixed addresses, it's doable via escape-hatch in Deca. You would CAST from the integer form of the address to an appropriate pointer type.

Yes, I realize this is unsafe and difficult to support properly, which is why when any new safe systems language comes along, I always look up how it handles this case. For instance, it would be "safe" to allow a coercion from an int to a typed pointer provided you can statically guarantee that no other operations can accidentally alias that location and view it as an incompatible type, ie. via an offset from some other address, or another fixed address that overlaps with an incompatible type.

Regarding subtyping on integers, I'm not sure what that's supposed to address. Do you foresee it addressing word-sized tagged unions, like this C fragment:

struct Tagged {
  union {
    int integer;   //tag = 1
    void *pointer; //tag = 0
  } bits : 31;
  int tag : 1;
};

Preferably, the Tagged.bits.pointer would also specify the type pointed to.

Eli Gottlieb: Oh, and without LtU, I would never have seen Ben Lippmeier's Disciple language and associated papers, which were THE chief inspiration for doing the extra work of having proper regions and effects in Deca.

Then, as far as I'm concerned, LtU has fulfilled its raison d'étre.

By (deliberately?) misspelling « être », you raise an important and relevant point. Should the French orthography be overhauled to rely on the inference of l’accent circonflexe a là Hindley-Milner — much the same way that the diaeresis ¨ is routinely inferred in the English reëlection and coöperation or the Russian ёрш (usually spelled ерш) — or should the French continue to require the explicit presence of this (type) annotation? Telle est la question. It is true that l’accent circonflexe serves an occasional useful purpose of being the sole distinction between two different words, e.g.:

1. il eut mangé de la brioche;
2. qu’il eût mangé de la brioche.

But is it really needed? In the dark ages spanning the period between the Visigoths and Guillaume le Conquérant, the use of l’accent circonflexe was aimed at making French more palatable to the speakers of English. To wit, île → isle, forêt → forest, hôtel → hostel, hâte → haste, etc. But nowadays, it's about as redundant as explicit type declarations in Java.

Re: comment 68743: “LtU has fulfilled its raison d'étre [sic]”.

LtU’s raison d’être is its repeatedly demonstrated ability to turn any discussion into a PR campaign for the greater use of (static) typing, n’êt-il pas vrai ?

...of you to assume my error was deliberate. :-)

As for the rest, I personally am delighted when there's research that seems to really delve into what not having a type system can offer. My current poster-child for this is John Shutt's Kernel work. My slogan now is "take the phase distinction seriously or don't have one." What continues to be logically incoherent is the claim that dynamic typing has any positive benefit over static typing that isn't isomorphic to researching (non)computability itself. I also can't help it with respect to LtU if the preponderance of PLT research reflects the fact.

Is there no reason for a systems-programming language beyond C anymore, itself doomed to maintenance and legacy tasks while everyone lives on in virtual realities (sorry, I mean machines), or did virtual machines and very-high-level applications languages become dominant because nobody could agree on what the hell to do with systems programming?

I'm passing the buck: let's ask the people who did or are doing BitC, Cylone, Clay, Tart, and Rust. Then let's talk to the folks at UCSD who were doing a "Liquid Types" project as an extension to C for systems programming, and the folks at Portland State University doing Habit, Haskell-for-kernels. And I've heard rumors of a certain other institution (which I'm not naming because I haven't seen a public announcement of the project, but that may be my own ignorance) getting a big grant for highly-secured systems programming languages. And Galois certainly does well for themselves.

Assuming my answer to this question of "modern systems programming" is completely and utterly insufficient, how can we dismiss the question itself when we hear through scientific peer-reviewers and funders that they would all like to see someone take a stab at that question?

Many years ago I read a presentation entitled, "Systems Software Research is Irrelevant". Tell that to a researcher I took a course under, named Emery Berger, who has made his career on systems research. Hell, tell it to the "How to have a bad research career" presentation I also read, one of whose bullet points was "DO NOT do a systems project!".

It seems like there's unfilled demand for better systems software and better languages and runtimes for producing it. Unfortunately, for some reason the Problem of Systems Software continues to be consider "solved". Of course, Plan 9 was very good ;-), but it came out right in time to kill itself as the shift from timesharing to personal computers happened.

...or did virtual machines and very-high-level applications languages become dominant because nobody could agree on what the hell to do with systems programming?

Something like that. I would lay much of the blame on automatic garbage collection, which while extremely useful, created a hard dividing line that sucked language innovation away from systems languages.

One of the challenges here is that the target audience has a severe case of Stockholm Syndrome - they're so used to the pathological ecosystem they've learned to live with that they can't imagine why anything else would be needed.

A great fraction of systems programmers uses languages from the 1970s and no one cares.

No one also cares about capability security and native sandboxing on Smartcards. Instead we have JVM technology there for code loaded from 3rd parties with its considerable overhead. There is zero research about those topics, except from some companies which do it by themselves. There is an increasing number of university projects that deals with hacking cars, trains and planes. Scary, no? Unlike PCs where software always put pressure on customers buying new generations of hardware there isn't any such pressure in the embedded sector. Since it employs armies of testers anyway it may be of little surprise that it is relatively open minded towards formal methods.

No, systems software research is far from done, but the 10th billion language that targets x86 is probably not so urgently needed as many programmers might think.

A great fraction of systems programmers uses languages from the 1970s and no one cares.

You could have said this in the early 1990s about the possibility of languages like Java and Python. Turns out that although it was possible to have the perception "no one cares" at that time, once better alternatives were available, a majority cared.

No, systems software research is far from done, but the 10th billion language that targets x86 is probably not so urgently needed as many programmers might think.

Again, same issue.

In any case, this all seems rather off-topic in this thread. Since LtU is a site devoted to discussion of programming languages, a PL version of the quote by New Scientist editor Alun Anderson applies. New programming languages with interesting feature sets are inherently interesting, and if you don't agree...

New programming languages with interesting feature sets are inherently interesting, and if you don't agree...

I studied mathematics as a "brotlose Kunst" for a couple of years. So this has my sympathy. And yes, maybe someone still finds something new even in overcrowded fields and searching under the lamp.

This language has actually ended up spawning a few possibly-new ideas: multi-method type-classes (which need a lot of work), a design pattern that uses implicit parameters to capture modules from the environment (which seems kinda trivial), and the use of subtyping-esque mechanisms to control the mutability of slots across pointers (this one's the most well-fleshed-out and researchy).

When everything is solved, go find harder problems. Hence systems programming languages instead of regular PL (not everything is solved in PL, but its increasing subspecialization is a sign).

Hamming's book is a great treatment of this topic.

Really great stuff. I do have to admit, the issue of whether this work will be scientifically relevant has occasionally kept me up o' nights. Well, it would have if I wasn't exhausted from sleep deprivation.

On the other hand, it did throw off that last idea that I'm typing up into a little draft of a pretend workshop paper right now. I've thought a bit about it, and I've realized that one's actually pretty relevant to both PL and systems folks. Mutability and synchronization are big issues everywhere.

I do have to admit, the issue of whether this work will be scientifically relevant has occasionally kept me up o' nights.

When Hamming started to work in the early 1940s you could still know everyone by name who worked as a theoretical physicist, not to talk about the borders of 'communication', a term which wasn't even used in science before Shannon introduced it, and math. Scientists were just discovered to be an important strategic resource for the wealth and competition of nations who could actually be produced, as "organization men" [1] instead of being individual and accidental geniuses.

When I studied, the whole perception was already organized. The "important problems" were known and famous and many people flocked on them, often in global cooperation and individual competition. This also happened in the "pure" sciences which were not capital intensive "Big Science" in the way Los Alamos, the lunar landing project of the NASA or the LHC are. Superstring theory is a lively example and it was a great fashion in the 1990s - doing speculative mathematical-physical research was not much debated as it became a decade later. In some sense the research network already answers the question about what is important and what is not and this can be measured in terms of citations, public attention, financial grants and human resources which can be acquired using grant money. Since the network answers the nightly questions for you, you don't have to.

I'm not sure if young researchers don't get all those capitalist science management and marketing aspects much better than I did. I can't remember that me and my friends reflected the science and research market at all, speculating about what was "promising", which communities are probably interested and so on. It was still all romantic heroism: great people who are doing extraordinary things. That's actually a very beautiful, mythic tradition, which is kept alive through story telling a la Hamming. We felt not quite like stooges, as Hamming did early in his career, but also other-directed without knowing what to oppose to and the only way we found to rebel against it was to drop off.

[1] I refer to William Whyte's famous sociological study from 1956.

It's probably not really important and we don't urgently need any new programming language anyway but it would be interesting from an artistic point of view.

I disagree, it is still important. In what language are you going to write your safe language runtime and garbage collector, if not a systems language that can perform safe bit-twiddling on pointers?

In one that allows the use of something like an "unsafe/systems" package.

Some examples, Modula-2, Modula-2+, Modula-3, Oberon, Ada, D.

The point is to eliminate the unsafety entirely. Isolating unsafety is a great first step, but not quite enough. Other than typed assembly language, I don't think there's a "systems language" in existence that safely deals with tagged pointers. Actually, I'm not even sure whether typed assembly language supports this usage.

As it seems this has been done already in the 60's with ALGOL, unfortunately it did not catch on.

I am all for safer systems programming languages.

Many of the security exploits we suffer, are a consequence of C and to lesser extent C++ use.

I am a firm believer that if a more type safe language would be used, there would not exist so many security issues.

The problem is that it takes generations to bring the programmers to new paradigms.

The problem is that it takes generations to bring the programmers to new paradigms.

That's not so much a "problem" as it's merely a constraint.

i mean, shouldn't it be? in this day and age, shouldn't even grandmas be interested in things that don't leak their credit card #s? why hasn't spark ada taken over everything by now? :-)

But we all know that security doesn't sell well, so it's no surprise that managers don't take into account security when selecting a language.

Spark Ada cares for not storing credit card information as plain text in a data base? Sounds like a pretty cool language feature.

I would call it the next tier up of PLT rigor from Deca, Clay, BitC, Cyclone. None of this set offer theorem-proving capabilities or dependent typing; ATS thus has the honor of being the only Agda competitor for systems programming.

I was thinking of the low-level aspects of ATS (linear types, destructive pattern matching, non-mandatory garbage collection) rather than the dependent type / proof aspect, which is indeed less relevant. I don't think the focus of ATS is on theorem proving, and thus I wouldn't call it an "Agda competitor" (even if Agda itself is on the edge between a programming and a proof system; at least I certainly wouldn't call ATS a Coq competitor).

I think the possibilities offered by ATS in this low-level area are quite nice, and only partially related to the expressiveness of the dependent type layer -- I'm not sure which low-level parts really rely on it, though I can certainly see it being helpful to avoid eg. some dynamic bound checking.

ATS thus has the honor of being the only Agda competitor for systems programming.

No it doesn't! Edwin Brady's Idris is quite adequate for the job. There's a new version out, I warmly recommend checking it out. The implementation is usable and Idris syntax will probably appeal more than the ATS one to people with a Haskell background.

As I claimed above, ATS is *not* an Agda competitor. I agree that Idris can be seen as an Agda competitor, but on the other hand I wouldn't claim it is about "systems programming" in the sense used by Eli here, where you try to write programs without any dynamic memory allocation. I would rather describe it as a (less proof-theoretically sophisticated) Agda with a viable C FFI rather than a viable Haskell FFI; at least the previous version that I had looked at.

ATS is much lower-level than that: it allows to avoid GC, to manipulate unboxed binary data, and even to perform pointer arithmetic. You could consider rewriting a C program entirely in ATS, you can write a kernel driver in ATS today (or rather, in 2007). I'm not sure that's why Idris is aiming at.

PS: there is a lot of ambiguity around what "systems programming" mean. In this thread I am interested in "systems programming" in the sense of "the kind of C code you write for embedded systems or OS kernel development", but there are more high-level views of "resource-conscious software layers that are below the end-user programs the user interact with", a bit like the Go tribe advertise. I suppose both are equally reasonable use of the term, but it's still interesting to make a distinction between languages following the low-level or the high-level vision.

You could consider rewriting a C program entirely in ATS

In the story submission form, there's a "Path alias" field that determines this. It's possible the field only appears for admins, though, not sure about that.

I hadn't considered using the LtU node id as an alternative calendar for the history of programming languages... That's such a post-node-4424 idea!

There are still people suffering through node-4424.

why do people still compare new system programming langages to C instead of Ada?

For the reason you mentioned, C is much much more popular. The speed of hardware is defined in terms of how well it executes C code.

It is precisely the feature rich aspects that make me not even sure I'd consider Ada to be a systems language. C conversely has features that are reflective of what hardware can do, not what programers want to do.

Please forgive amateur work by an undergraduate.

When I got out of last Spring semester, I went home and basically slept for a week. Then, over the summer, I managed to catch up on most of the papers I had missed or not been able to understand.

Effect systems? Check.
Type-classes? Check, though I eventually decided to use implicit parameters instead (but with Deca's scoping rules instead of Scala's, and a notion of final implicits that can't be overridden). Of course, the funny thing about type-classes and multimethods is how alike they are, and yet how utterly different. I want to eliminate a feature in favor of an equivalent or more powerful feature, but I can't.

"Allocation isn't a real side-effect" is a paraphrasing of the popular view in "mainstream" PL, such as Haskell, where allocation is performed ALL THE TIME without the IO or St monads becoming involved, for some strange reason. In truth, allocation looks like a side effect to the allocator itself, but looks pure to the client of allocation.

My paper *did* get rejected, and in fact about 10% of the criticism in the reviews *actually* clued me in to errors. On the upside, the arXiv copy got noticed and I was asked if I might resubmit to some conference when I fixed things. That's done, and by now I'm experiencing the "knowledge rises, expectations fall" effect described in PhD Comics. This iteration of the paper will probably be rejected (almost all papers are), but if all the reject-reviews are for aesthetic reasons, I'll at least take the author appeal.

I want to eliminate a feature in favor of an equivalent or more powerful feature, but I can't.

You mean something like predicate dispatch?

"Allocation isn't a real side-effect" is a paraphrasing of the popular view in "mainstream" PL, such as Haskell, where allocation is performed ALL THE TIME without the IO or St monads becoming involved, for some strange reason.

Depends who you ask. Region-based memory management clearly considers allocation a side-effect. Most languages don't because then just about every language is effectful.

You mean something like predicate dispatch?

Multimethods, particularly hierarchical unambiguous multimethods as invented by Millstein et al and used by myself, end up acting pretty much (not quite the full moral equivalent, but close enough) like a pattern-match done at runtime on the variant tags or class-tags of the actual data.

Type-classes and implicit parameters match on static types in much the same way.

So the question is: could we have hierarchical, dynamically-dispatched type classes? Can we assemble a tree of possible dictionaries at compile time (just as we do for the hierarchical multi-methods). At runtime, we use a hierarchical tag-match to select the most appropriate of those known cases and dispatch through the appropriate dictionary.

Why would we even want that? Because that would give a multimethod system one of the most desirable features of both Haskell and Java: the guarantee that a class implementation must implement all the relevant methods.

There's also an obstacle, at least as Deca sees things. Type-classes and implicit parameters are usually considered moral equivalents. They are not, however, semantic equivalents, and this extension shows up the difference: you can't use matching a tag tree to fill in an implicit parameter of a dictionary because the function parameters are contravariant. The dictionary selected based on the tag matching wouldn't subtype or type-equal the implicit parameter's type.

And if we go for full Haskell-style type-classes, does the definition of an instance method see its own dictionary, with type-class methods having the correctly specific signature? What sort of semantics does that have? I can't see anything outstandingly wrong about that, I think that's how Haskell mostly does it, but I'm not sure the semantics remain sound in the presence of subtyping and hierarchical dictionary selection.

Of course, I would normally want to keep the implicit parameters, because as noted sometimes on LtU, they have their own "perks" aside from being usable for type-classes.

So yeah, multimethod type-classes sound nice but need a lot of work, semantically.

Depends who you ask. Region-based memory management clearly considers allocation a side-effect. Most languages don't because then just about every language is effectful.

Well at the systems level, just about every language should be considered effectful. House's (as in House the Haskell kernel) monadic treatment is one way of handling it, Deca's importation of effect-system work is another, but you do need some way of handling it.

Because that would give a multimethod system one of the most desirable features of both Haskell and Java: the guarantee that a class implementation must implement all the relevant methods.

I wasn't aware that Deca's multimethods weren't statically checked. Some references that may help:

• Type-checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance -- directly relevant to multimethods
• Extensible Programming with First-Class Cases -- perhaps indirectly relevant, but in principle it does the same thing you're after, ie. gathers disparate type and case definitions into single case statements and checks for exhaustiveness.

Well at the systems level, just about every language should be considered effectful.

Oops, my sentence should have read "just about every function is effectful (because it allocates)". Don't know what I was thinking...

Deca's multimethods are statically checked, according to exactly the methods given in that first paper, which I cite. decac can statically verify that every call to a multimethod has a non-empty set of valid possible cases onto which to dispatch. It helps to use Deca's terminology here: "methods" are the generic functions, "overrides" are the defmethod'd cases.

What I meant was, consider a type-class in the Haskell sense, say Eq a. We all know it has two methods, two functions that must be implemented to provide a valid dictionary for any a. Java's Comparable interface can express the same thing.

So how do we express that in a multimethod system? As I've seen multimethods traditionally presented, we can't... YET. There's no major theoretical reason why we can't, we just haven't figured out a clean, non-bloated syntax and semantics for expressing that some class/variant/ADT/$WHATEVER must not only implement one multimethod but several.

If we didn't need to have default cases for statically safe multimethods, which IIRC we do, we could just declare our methods to be dispatched on the appropriate supertype and then every subclass, or even combination of subclasses as it may be, would be required to provide an implementing method for every such multimethod. If this sounds like it completely ruins modularity by letting any foreigner and his module impose an implementation requirement on my type, I think that's because it does -- hence default cases and such.

So: how do we specify, in a modular and type-safe way, that the method-case trees (see Millstein) of certain multimethods must overlap, or, put another way, that certain types must implement method-cases not only of one multimethod but of several?

So: how do we specify, in a modular and type-safe way, that the method-case trees (see Millstein) of certain multimethods must overlap, or, put another way, that certain types must implement method-cases not only of one multimethod but of several?

This is a good question I sumbled across again this morning, but still didn't have an answer. Fortuitously, I just came across a paper which does address this in one way: A Second Look at Overloading.

Think of it like type classes, but without the class declarations. You instead specify the overloaded operations by name. This obviously implies more verbose function types, since you have overloaded name constraints instead of class constraints, but this does address the question above: to ensure a type implements several multimethods, just explicitly declare it on at least one function signature.

That the used mulimethods don't appear in function signatures is where the problem really lies.

I would write a GC in Deca by casting back and forth between pointers and integers to do the arithmetic.

I had been planning for the semantics of Deca to follow C semantics, but with a Pascal-like compiler switch for adding exceptions at things like integer overflows. Unfortunately, the platform-dependence here is pretty thorny: I can guarantee platform-independent semantics either by tying Deca to an "imaginary" platform like LLVM, or by carefully reimplementing the desired semantics by hand in custom-built code generator backends.

There is no runtime system that hooks up to lambdas and closures. Closures are existential packages. Existential packages are allocated as blobs of bytes, the least-bad of several different pretty bad options for how to handle them without garbage collection.

The one upside to doing existentials that way is that any pointers captured by the existential have their regions "leaked" into the existential signature, making it statically impossible to pass data up the stack beyond where it remains validly accessible.

Cold comfort to everyone used to dynamically-allocated, garbage-collected closures, though.

I can guarantee platform-independent semantics either by tying Deca to an "imaginary" platform like LLVM

You have to be careful there though, because LLVM bitcode is not entirely platform independent . Depends entirely on how you handle platform word size.