Learn You an Agda

> But in your example the program doesn't represent the code itself but a program written in some new language.

That's the key idea ;)

If I write some Java like `DB.connect(credentials).select("users").where("name", "Kevin")`, am I using "some new language"? As far as Alan Kay is concerned, yes; that was one of his main inspirations for OOP:

> My math background made me realize that each object could have several algebras associated with it, and there could be families of these, and that these would be very very useful.

From http://www.purl.org/stefan_ram/pub/doc_kay_oop_en

The only difference between that Java example and my earlier Haskell/Agda example is that the functional version operates in two phases: calculating which operations to perform (building a `Program` containing `Ops`) is separate to performing those operations (applying an interpreter function to a `Program`).

However, keep in mind that we're not doing imperative programming, so there's is no inherent notion of time: we get the same result no matter which order we evaluate stuff in (that's the Church-Rosser Theorem). Hence these two "phases" are logically distinct, but not necessarily temporally distinct. In practice, we tend to define our `Program` lazily, so it gets constructed on-demand by the interpreter.

This is a bit like having a `main` loop containing a `switch`, for example (forgive mistakes; I've never used function pointers in C):

    void main(op* instruction, int* length, void* callback) {
        socket* s = set_up_socket();
        int close = 0;
        char* data;
        while (!close) {
            switch(*instruction) {
                case READ:
                    // Read logic
                    data = read_from_socket(s, *length);
                    *callback(instruction, data);  // Update instruction based on data
                    break;
                case WRITE:
                    // Write logic
                    data = *callback(instruction);  // Update instruction and return data
                    write_to_socket(*length, data);
                    break;
                case CLOSE:
                    // Close logic (ignores any other instructions)
                    close = 1;
                    break;
        }
        close_socket(s);
    }

This main function is basically the same as our interpreter; it's keeping the dangerous socket-related stuff in one place, providing some safety that the socket will be closed after use, etc. The values of `data` and `instruction` are being computed by arbitrary C code living at `callback`, just like our `Program` can be computed by arbitrary Haskell/Agda/whatever code. In this case the interleaving of choosing and executing instructions is explicit, but a lazily-evaluated `Program` will behave similarly in practice.

Does this mean that those callbacks are in "some different language" to C? No; everything is regular C except that we just-so-happen to be labelling some ints as `READ`, `WRITE` and `CLOSE`. Likewise, in Haskell/Agda/etc. we have the full breadth of the whole language available to us; we just-so-happen to be returning values of type `Op` and `Program`. All of our logic, concurrency, etc. is done in the "host" language; we only define `Op`s for the things we want to restrict, like `Read` and `Write`; there's absolutely no point defining operations for boolean logic, arithmetic, string manipulation, arrays/lists, etc. because that's available already. Of course, once we've finished defining our socket library, that too will be available to everyone (if we release it); just because it might use some crazy `Op`, `Program` and `runSocket` things internally doesn't mean anyone has to care about that; it's just an implementation detail.

Notice that this is very similar to an OOP dynamic dispatch system, where `READ`, `WRITE` and `CLOSE` are method names and the callbacks just-so-happen to be kept together in a struct which we call an "object". Just like Alan Kay said.

I'm not talking about standardization but about a different kind of type system, where the intersection types of callees interact in interesting ways with the type of the caller[1] (taking into account ordering). From what I understand this kind of thing is being research but we don't have anything close to being practical just yet.

[1]: for example, the type of the caller can be: "this function locks A, then B, then unlocks B, then unlocks A". This type can arbitrarily intersect other effect types, such as: "this function writes to socket X" and also "mutates variable V"

Could you expand upon this?

Sure. Take a look at all the mathematical theories and models out there. They're all languages, and solving problems within a framework of any given mathematical theory is pretty similar to a process of compilation - a source language should be transformed into another language in which the solution can be "executed".

Let's take CAD as an example. We've got a source language: a constructive solid geometry, for simplicity. Pretty much everything a CAD does boils down to various transforms of this language - into an optimised octree for rendering purposes, into G-code slices for production, into, say, SVG for blueprints, etc.

CRUD stuff boils down to transforms between different semantic domains - a relational structure at one end and workflow graphs and document trees on another.

It's really hard to come up with any practically important problem domain which would not benefit from being represented in terms of languages and transforms.

Thanks! Can't believe I didn't think of that :/

What's the distinction between C-c C-space and C-c C-r? It looks like the former computes proof obligations for ?s, but what does the latter do? And why couldn't we use the latter in the first instance, to deduce the outermost STEP ? ?

Edit: never mind, that did work.