Lambda the Ultimate

This is neat:

Live Coding at Come Alive.

From the FAQ:

Alive is an extension to Visual Studio that instantly shows you what your code is doing.
It was created with one purpose: To provide immediate feedback to developers.

(Requires WebEx Player.)

Art Brock & Eric Harris-Braun - "Just a Spoonful of Ceptr".

Ceptr evolved from the MetaCurrency Project as we needed to build distributed tools that went far beyond blockchain approaches. Ceptr provides semantic computing, a self-describing protocol stack, distributed/byzantine processing, fractal virtual machines, autonomous contracts and organizations, and more. Since it is such a wide-reaching project, we'll only be able to get a taste of it in a 1 hour webinar. So we've set up some demonstrations of how approaching things with Ceptr allows us to easily tackle problems which are normally intractable. After a bit of show and tell, we'll have time for questions and discussion about our tools and approach.

I think it is worth watching through this -- this presentation was the only thing so far I've seen on CEPTR that actually made me understand what is being talked about since they tend to have made up new lingo and don't always tell you what it is most like from the past. It has aspects of tuple spaces, of objects, of actors, or cap'n proto, IoT, etc.

This is a fork of another topic.

I think it is high time that we stop talking about programming languages in isolation of the tools that support them. The tools have always depended on the languages, obviously, but increasingly the languages depend on the tools, especially in professional language design contexts. Dart and TypeScript are extreme examples of this where the type systems are there primarily to support tooling, and are much less about early error detection. As another example, C# design is heavily influenced by Visual Studio.

Designing a language invariably involves trade offs, and if we accept tools as part of the core experience, we are able to make decisions that are impossible given the language by itself. For example, many people find type inference bad because it obscures developer documentation, especially if it is not completely local. However, given an editor where inferred type annotations are easily viewed when needed, this is no longer a problem. Likewise, a type system that cannot provide good comprehensible error messages in the tooling is fundamentally broken, but tooling can be enhanced to reach that point of comprehensibility. Type systems in general are heavily intertwined with tooling these days, playing a huge role in features like code completion that many developers refuse to live without.

And of course, there are huge advances to be had when language and programming model design can complement the debugging experience.

There are other alternative opinions about this, to quote and reply to Andreas from the other topic:

Only if you do so for the right reason. Tooling is great as an aid, but making it a prerequisite for an acceptable user experience isn't. A language is an abstraction and a communication device. Supposedly, a universal means of expression, relative to a given domain. It fails to be a (human-readable) language if understanding is dependent on technical devices.

This is a good point: code should stand on its own as a human communication medium. However even our human communication is increasingly tool dependent, as we rely on things like the Google to extend our capabilities. We are becoming cyborgs whether we like it or not.

There are many other places than your editor where you need to read and understand code: in code reviews, in diffs, in VCSs, in debuggers, in crash dumps, in documentation, in tutorials, in books printed on paper.

Code isn't bound to paper. Even when printed out on paper, it does not need to printed out as it was typed in.

You can try to go on a life-long crusade to make every tool that ever enters the programming work flow "smart" and "integrated", and denounce books and papers as obsolete. But that is going to vastly increase complexity, coupling, and cost of everything, thus slows down progress, and just creates an entangled mess. And in the mean time, every programmer will struggle with the language.

This is more of an observation about current and future success of programming experiences. I would say it has already happened: successful programming languages already pay these costs, and new languages must either devote a lot of resources to tooling, or build them in at the beginning, or they simply won't be successful. Some people wonder why language X isn't successful, and then chalk it up to unenlightened developers...no.

Nothing ideological or academic about that, just common sense.

Since an appeal to common sense is made, I would just think we have different world views. We at least exist in different markets.

Recent LtU discussions have mentioned (eg. here) that it is hard to get programming language "design work" to get recognized academically. Good design work that is *also* accompanied by solid benchmarks or strong correctness argument will get recognized for the benchmarks or formal guarantees, but design work on domains that do not lend themselves to easy performance metrics, or done by people that do not use formalization as a validation tool will be hard to get recognized. A recent blog post by Jonathan Edwards echoes the same frustration (note that it also complains about the worse-is-better philosophy prevalent in industry not being good at fostering radical changes either).

(I would like to apologize to the part of the LtU community that does not care about academia. I try to keep my usual submissions/topics independent of professional occupation, and this one is the exception. Feel free to just skip it.)

There are some academic spaces where design work can stand of its own. I know of the Future of Programming workshop, the Onward! conference, and maybe (it's probably too soon to tell) the new SNAPL conference. However, at least the first two events are considered somewhat second-class in the academic community (which has an unfortunate tendancy to foster competitivity through metrics and will keep core of "top tier" conferences, creating strong incentives to publish only at the most selective/established places). ICFP has a "functional pearl" category (see Call For Papers (CFP), section "Special categories of papers") that counts as a first-class ICFP publication, ITP has a "rough diamond" category (CFP, but-last paragraph), Oleg just mentioned FLOPS "system descriptions" (it also has "declarative pearls", CFP, "Scope"), what would a category of "design papers" look like? (Yes, the idea is have a niche to protect endangered species that the free market would tend to root out; I think we can win big by dedicating a reasonable proportion of our scarce resources to fostering intellectual and methodological diversity.)

Here is a proposal for how it would be defined, or rather, how it would be reviewed (which I think is the subtle question):

Each proposed language/feature design must come with a working implementation. The author should highlight the proper domain area in the submission, and maybe make a few suggestion of potential programs to implement. Reviewers are then asked to actually implement some programs using this language/feature, and rate the system based on whether they enjoyed this implementation attempt.

(I don't know where such a category would fit; PLDI has a D for "Design" in the name, but then I don't know much about this conference.)

LtU generally is not appropriate venue for posting call-for-papers, but there have been exceptions, if the CFP has an exceptionally wide appeal. Hopefully FLOPS 2016 might qualify.
http://www.info.kochi-tech.ac.jp/FLOPS2016/

FLOPS has been established to promote cooperation between logic and functional programmers, hence the name. This year we have taken the name exceptionally seriously, to cover the whole extent of declarative programming, which also includes program transformation, re-writing, and extracting programs from proofs of their correctness. There is another strong emphasis: on cross-fertilization among people developing theory, writing tools and language systems using that theory, and the users of these tools. We specifically ask the authors to make their papers understandable by the wide audience of declarative programmers and researchers.

As you can see from the Program Committee list, the members have done first-rate theoretic work, and are also known for their languages, tools and libraries. PC will appreciate the good practical work. Incidentally, there is a special category, ``System Descriptions'' that FLOPS has always been known for. We really want to have more submissions in that category.

One can see even on LtU that there is some rift between theoreticians and practitioners: Sean McDermid messages come to mind. He does have many good points. We really hope that FLOPS will help repair this rift.

For an Actor to cast an address of another Actor is a dubious operation. Instead, an Actor should only cast its own address to interfaces that it implements. For example,

Consider the following definition:

Interface Account with getBalance[ ] ↦ Currency,
                       deposit[Currency] ↦ Void,
                       withdraw[Currency] ↦ Void

The following is an implementation of Account:

Actor SimpleAccount[aBalance:Currency]
     myBalance ≔ aBalance｡
     implements Account using  
        getBalance[ ] → myBalance
        deposit[anAmount] → Void afterward  myBalance ≔ myBalance+anAmount   
        withdraw[anAmount] → (anAmount > myBalance) �
                               True ⦂ Throw Overdrawn[ ]
                               False ⦂ Void afterward myBalance ≔ myBalance–anAmount

 
The above implementation of Account can be extended as follows to provide the ability to revoke some abilities to change an account by providing AccountSupervisor and AccountRevoker interfaces:

The implementation AccountSupervisor below implements the Account interface as well as AccountSupervisor and AccountRevoker interfaces as an extension of the implementation SimpleAccount: 

  Actor AccountSupervisor[initialBalance:Currency] extends SimpleAccount[initialBalance]
  withdrawableIsRevoked ≔ False,
  depositabeIsRevoked ≔ False｡
  implements AccountSupervisor using  
     getRevoker[ ]→ ⍠AccountRevoker
     getAccount[ ] → ⍠Account
     withdrawFee[anAmount] → Void afterward myBalance ≔ myBalance–anAmount //  withdraw fee even if balance goes negative
  also partially reimplements exportable Account using
    withdraw[anAmount] → withdrawableIsRevoked �
                           True ⦂ Throw  Revoked[ ]
                           False ⦂ ⍠SimpleAccount.withdraw[anAmount] 
    deposit[anAmount] → depositableIsRevoked �
                           True ⦂ Throw  Revoked[ ]
                           False ⦂ ⍠SimpleAccount.deposit[anAmount] 
   also implements exportable AccountRevoker using
      revokeDepositable[ ] →  Void afterward depositableIsRevoked ≔ True   
      revokeWithdrawable[ ] → Void afterward withdrawableIsRevoked ≔ True

 
For example, the following expression returns negative €3:
   Let  anAccountSupervisor ← AccountSupervisor.[€3]｡
      Let   anAccount ← anAccountSupervisor.getAccount[ ],
            aRevoker ← anAccountSupervisor.getRevoker[ ]｡
         anAccount.withdraw[€2]                           //  the balance is €1
         aRevoker.revokeWithdrawable[ ]
                                                                  //  withdrawableIsRevoked in is True        
         Try anAccount.withdraw[€5]                  //  try another withdraw
                 catch�  _  ⦂ Void                    //  ignore the thrown exception
               //  the balance remains €1
         anAccountSupervisor.withdrawFee[€4]
                           //  €4 is withdrawn even though  withdrawableIsRevoked
         anAccount.getBalance[ ]  //  the balance is negative €3

Callisto -- Versioned objects (github)
Wyago
2015

This is a micro prototype on how a versioned objects would look in a programming system. It's a horrific implementation (and system) meant only to explore ideas, so it ignores reality in many ways, including performance and memory usage.

The syntax of the language is similar to that of the Io language (at iolanguage.org), hence the name Callisto. The object model is pretty weird though. Instead of having an object with slots, objects are simply stored as a simple union type of Base, the root of the object tree, or a Delta with the name of the slot being changed, the value it's being changed to, and the parent of the delta. (There's also an error value with a string describing the error, but that's not part of the object system itself, it's just a tool for expression evaluation errors.)

An object looks like a simple line of deltas leading back to base:

Base ← x is 10 ← y is 10 ← x is 20

You can note that this is kind of similar to a git commit chain (or any vaguely similar system; you're probably pretty familiar with git as a specific example though). This example could, for example, be a point with a coordinate. It's interesting to note that it's modification history is encoded in it's delta chain. This is obviously horrible, as it means any mutation will leak memory. There could certainly be a variant of garbage collection that resolves an objects current state and eliminates old changes that are no longer relevant.

The designer, Wyago, seems interested in experimental micro-languages, and recently posted on reddit about another minimalist language based on term rewriting, called Mantra.

I think the language lacks examples.

Deny Capabilities for Safe, Fast Actors.

Combining the actor-model with shared memory for per- formance is efficient but can introduce data-races. Existing approaches to static data-race freedom are based on unique- ness and immutability , but lack flexibility and high perform- ance implementations. Our approach, based on deny prop- erties , allows reading, writing and traversing unique refer- ences, introduces a new form of write uniqueness , and guar- antees atomic behaviours .

As a subject, garbage collection has a nice glossary that can be used as a reference while reading the literature. Do type systems/type theory have a comparable online glossary?

I haven't come across one, but it seems like a it could be valuable resource.

The paper:

Resourceable, Retargetable, Modular Instruction Selection Using a Machine-Independent, Type-Based Tiling of Low-Level Intermediate Code

Ramsey and Dias have a series of papers about making it ever easier to generate compiler backends, and the claim is that they produce decent code to boot. I wonder if this stuff has/will show up in compilers I can use? (Or, do you think it not actually matter, for some pragmatic reason or other?)

Abstract: We present a novel variation on the standard technique of selecting instructions by tiling an intermediate-code tree. Typical compilers use a different set of tiles for every target machine. By analyzing a formal model of machine-level computation, we have developed a set of tiles that is machine-independent while retaining the expressive power of machine code. Using this tileset, we reduce the number of tilers required from one per machine to one per architectural family (e.g., register architecture or stack architecture). Because the tiler is the part of the instruction selector that is most difficult to reason about, our technique makes it possible to retarget an instruction selector with significantly less effort than standard techniques. Retargeting effort is further reduced by applying an earlier result which generates the machine-dependent implementation of our tileset automatically from a declarative description of instructions' semantics. Our design has the additional benefit of enabling modular reasoning about three aspects of code generation that are not typically separated: the semantics of the compiler's intermediate representation, the semantics of the target instruction set, and the techniques needed to generate good target code.