LtU Forum

How Useful is Erlang Hot-Swapping of Code?

Please discuss. I am interested.

minor lexical tokenization idea via character synonyms

A few days ago I had a tokenization-stage lexical idea that seems not to suck after going over it several times. On the off chance at least one person has similar taste, I can kill a few minutes and describe it. Generally I don't care much about syntax, so this sort of thing seems irrelevant to me most of the time. So I'll try to phrase this for folks of similar disposition (not caring at all about nuances in trivial syntax differences).

The idea applies most to a language like Lisp that over-uses tokens like parens with high frequency. I'm okay with lots of parens, but it drives a lot of people crazy, apparently hitting some threshold that says gibberish to some folks. Extreme uniformity of syntax loses an opportunity to imply useful semantics with varied appearance. Some of the latent utility in human visual system is missed by making everything look the same. A few dialects of Lisp let you substitute different characters, which are still understood as meaning the same thing, but letting you show a bit more organization. I was thinking about taking this further, where a lot of characters might act as substitutes to imply different things.

The sorts of things you might want to imply might include:

  • immutable data
  • critical sections
  • delayed evaluation
  • symbol binding
  • semantic or module domain

A person familiar with both language and codebase might read detail into code that isn't obvious to others, but you might want to imply such extra detail by how things look. Actually checking those things were true by code analysis would be an added bonus.

I'm happy using ascii alone for code, and I don't care about utf8, but it would not hurt to include a broader range of characters, especially if you planned on using a browser as a principle means of viewing code in some context. When seen in an ascii-only editor, it would be good enough to use character entities when you wanted to preserve all detail. It occurred to me that a lexical scan would have little trouble consuming both character entities and utf8 without getting confused or slowing much unless used very heavily. You'd be able to say "when you see this, it's basically the same as a left paren" but with a bit of extra associated state to imply the class of this alternate appearance. (Then later you might render that class in different ways, depending on where code will be seen or stored.)

A diehard fan of old school syntax would be able to see all the variants as instances of the one-size-fits-all character assignments. But newbies would see more structure implied by use of varying lexical syntax. It seems easy to do without making code complex or slow, if you approach it at the level of tokenization, at the cost of slightly more lookahead in spots. As a side benefit, if you didn't want to support Unicode, you'd have a preferred way of forcing everything into char entity encoding when you wanted to look at plain text.

Note I think this is only slightly interesting. I apologize for not wanting to discuss character set nuances in any detail. Only the lossless conversion to and from alternatives with different benefits in varying contexts is interesting to me, not the specific details. The idea of having more things to pattern match visually was the appealing part.

POPL 2016 Research program...

is out here:

Many of the papers sound cool (Newtonian Program Analysis via Tensor Product, Transforming Spreadsheet Data Types using Examples, Program Synthesis with Noise, Memoryful Geometry of Interaction II: Recursion and Adequacy, Is Sound Gradual Typing Dead?) even if I'm not really connecting with them (maybe just in my field of work).

On type safety for core Scala: "From F to DOT: Type Soundness Proofs with Definitional Interpreters"

From F to DOT: Type Soundness Proofs with Definitional Interpreters by Tiark Rompf and Nada Amin:

Scala's type system unifies aspects of ML-style module systems, object-oriented, and functional programming paradigms. The DOT (Dependent Object Types) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, type soundness has only been established for a very restricted subset of DOT (muDOT), and it has been shown that adding important Scala features such as type refinement or extending subtyping to a lattice breaks at least one key metatheoretic property such as narrowing or subtyping transitivity, which are usually required for a type soundness proof.
The first main contribution of this paper is to demonstrate how, perhaps surprisingly, even though these properties are lost in their full generality, a richer DOT calculus that includes both type refinement and a subtyping lattice with intersection types can still be proved sound. The key insight is that narrowing and subtyping transitivity only need to hold for runtime objects, but not for code that is never executed. Alas, the dominant method of proving type soundness, Wright and Felleisen's syntactic approach, is based on term rewriting, which does not make an adequate distinction between runtime and type assignment time.
The second main contribution of this paper is to demonstrate how type soundness proofs for advanced, polymorphic, type systems can be carried out with an operational semantics based on high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proof for System F<: based on a definitional interpreter. We discuss the challenges that arise in this setting, in particular due to abstract types, and we illustrate in detail how DOT-like calculi emerge from straightforward generalizations of the operational aspects of F<:.

Not only they solve a problem that has been open for 12 years, but they also deploy interesting techniques to make the proof possible and simple. As they write themselves, that includes the first type-soundness proof for F<: using definitional interpreters — that is, at least according to some, denotational semantics.

Understated Twitter announcement here.

Socializing in the Real World?

It looks like I might be in Tokyo over the winter holiday / new year. Long ago I attended the long defunct Starling meetup. Wondering if other LtUers will be around this 2015-16? (No, I don't speak Japanese.)

In general, it might be nice to let people know if/when we travel in case we want to take turns buying rounds of beers somewhere?

Garbage Collection Based on a Linear Type System

An oldie (2000), but in my current (ignorant, admittedly) mind a goodie, from Igarashi & Kobayashi. I just wish the research hadn't apparently immediately died off? Garbage Collection Based on a Linear Type System. Or, chocolate + peanut butter.

We propose a type-directed garbage collection (GC) scheme for a programming language with static memory management based on a linear type system. Linear type systems, which can guarantee certain values (called linear values) to be used only once during program execution, are useful for memory management: memory space for linear values can be reclaimed immediately after they are used. However, conventional pointer-tracing GC does not work under such a memory management scheme: as linear values are used, dangling pointers to the memory space for them will be yielded.

This problem is solved by exploiting static type information during garbage collection in a way similar to tag-free GC. Type information in our linear type system represents not only the shapes of heap objects but also how many times the heap objects are accessed in the rest of computation. Using such type information at GC-time, our GC can avoid tracing dangling pointers; in addition, our GC can reclaim even reachable garbage. We formalize such a GC algorithm and prove its correctness.

inter-language PL theory patterns relevant to IPC?

I'd like some PL theory perspective on the idea outlined below, if you have relevant insight. Let me know if admin believes this is off-topic. But my interest is the PL angle, not the "let's write a cool app" angle. You can always hack away at getting a desired result without following any disciplined PL scheme, which isn't on-topic here.

As context, I want to start from a use-case, about processes interacting in a certain way. This is in contrast to how tech is sometimes discussed, first thinking of a neat formal idea, then trying to find a use. I want to start instead with a particular use and ask about any relevant neat formal ideas. My payoff is hearing ideas I would not have considered.

Instead of a boil-the-ocean scenario, where you pretend you can rewrite all software in a shiny new language, this use-case assumes things are not rewritten, that we operate in terms of whatever languages they use. So sometimes you talk to them in their own language, perhaps converting a new language to an old one at the boundary between new and old. Next is a concrete example scenario.

Suppose your new stuff goes in a new process that talks to others, like a browser and an IDE. If you have no UI frontend yourself, it looks like a daemon with one or more protocols to interact with other things. For example, a port serving http would let a browser interact easily with your process. This is especially easy because browsers are designed to work like that, but other standalone apps might also cooperate nicely, provided they have api to interact with other processes. I think this is true of emacs, to the extent you could use emacs as a frontend with a better IDE focus than a browser. Presumably other editors would also work as peers of your own process.

A browser likes Javascript, while emacs likes elisp, so presumably you would generate code to send them, if neither of those was a native focus in your process. (Altering a browser and/or an editor to understand your new paradigm is possible too, but it's interesting to work with existing tools that know nothing about you, and require no development changes at all.) Other tools will have their own preferred languages.

How do you go about doing that in a disciplined way with PL theory rigor? What PL concepts apply at different points and times? What general idea persists across different tools and languages? The new process speaking to each tool in its own language has some theory-of-mind about other tools, but that's not a PL concept as far as I know. Instead of winging each case in a one-off, specific, concrete way, what approach preserves some generality?

[I have little to add in discussion unless I think of questions about ideas suggested. It was recently suggested some things I say resemble a con artist's patter in some way, but I haven't been able to think of something I'm conning anyone about. I've had the same job for nine years, and it's boring. I don't look for a new job because web apps are not interesting to me, nor is commerce generally. I can't buff my reputation if I ignore social venues outside this one. I figure I'm pretty anonymous. I just crave interesting ideas. Coworkers want to talk about whether a local code style guide needs tuning; or if adventurous, they suggest rewriting tools in Erlang. So it's a creative desert. Being interested in PL topics is like being a Martian in places grinding away at the next incremental release.]

Edit: If you want code to run in a browser, you send it JS; if you want code to run in emacs, you send it elisp. (For some other executable, you send another language it wants.) The PL question is about being able to translate your model of code into another model, having a reason to believe qualities you want are present, and having something consistent in translation schemes.

Free JFP papers

Are these really the most cited or read?

Halide: a language for image processing and computational photography

Apparently this has not come up.

Halide (principle: Jonathan Ragan-Kelley).

Halide is a programming language designed to make it easier to write high-performance image processing code on modern machines.

The core concept is apparently to split programs into two parts. One part of the program specifies the algorithm, which relates inputs to outputs. The other part of the program specifies the schedule, specifying which parts of the output should be computed when and where.

In lieu of a distinct surface syntax, Halide programs are apparently built by programmatically assembling ASTs:

Its front end is embedded in C++. Compiler targets include x86/SSE, ARM v7/NEON, CUDA, Native Client, and OpenCL.

You build a Halide program by writing C++ code using objects of type Halide::Var, Halide::Expr, and Halide::Func, and then calling Halide::Func::compile_to_file to generate an object file and header (good for deploying large routines), or calling Halide::Func::realize to JIT-compile and run the pipeline immediately (good for testing small routines).

Additionally, Dan Tull has a demo of "Live Coding Halide" for which there is a video here:

Learning to Execute and Neural Turing Machines

First, Learning to Execute on training neural nets to execute simple programs. Abstract:

Recurrent Neural Networks (RNNs) with Long Short-Term Memory units (LSTM) are widely used because they are expressive and are easy to train. Our interest lies in empirically evaluating the expressiveness and the learnability of LSTMs in the sequence-to-sequence regime by training them to evaluate short computer programs, a domain that has traditionally been seen as too complex for neural networks. We consider a simple class of programs that can be evaluated with a single left-to-right pass using constant memory. Our main result is that LSTMs can learn to map the character-level representations of such programs to their correct outputs. Notably, it was necessary to use curriculum learning, and while conventional curriculum learning proved ineffective, we developed a new variant of curriculum learning that improved our networks’ performance in all experimental conditions. The improved curriculum had a dramatic impact on an addition problem, making it possible to train an LSTM to add two 9-digit numbers with 99% accuracy.

Next, Neural Turing Machines on training Turing machines. Abstract:

We extend the capabilities of neural networks by coupling them to external memory resources, which they can interact with by attentional processes. The combined system is analogous to a Turing Machine or Von Neumann architecture but is differentiable end-toend, allowing it to be efficiently trained with gradient descent. Preliminary results demonstrate that Neural Turing Machines can infer simple algorithms such as copying, sorting, and associative recall from input and output examples.

Perhaps these are baby steps to a future field of neuro PL.

XML feed