Lambda the Ultimate

I will always have a soft spot in my (otherwise cold, desolate, inchoate) heart for SML.

Their main page is unreachable for me just now (you can get e.g. the google cached version of it still if you like), but their last announcement was in April of this year (2014) so I hope the project is still alive.

SML# is an extension of Standard ML with practically important features, including record polymorphism, seamless interoperability with C, true separate compilation and linking, and native multithread support on multicore CPUs.

The most notable change in SML# version 2 is that the SML# compiler now works with the LLVM Compiler Infrastructure. The new SML# compiler compiles SML# code including all of the above features to LLVM IR code and produces native code through LLVM. More than half of compilation phases and library modules has been rewritten for the LLVM support. These changes also greatly speed up the compilation processes.

The major difficulties we have overcome in SML#-LLVM codegen is the treatment of polymorphism and separate compilation with SML#'s native ("unboxed") data representations. This aspect requires both a certain amount of additional type theoretical development specific to LLVM target and careful constructions of LLVM codegen. We hope to report this somewhere.

This wasn't posted yet, that I could find. Sorry if this is a dupe. Neelk doesn't self-promote, I guess. :-)

Abstract

In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency. Next, we give an application of this calculus by giving a proof-theoretic account of imperative programming, which requires extending the calculus with computationally irrelevant quantification, proof irrelevance, and a monad of computations. We show the soundness of our theory by giving a realizability model in the style of Nuprl, which permits us to validate not only the B laws for each type, but also the n laws.

These extensions permit us to decompose Hoare triples into a collection of simpler type-theoretic connectives, yielding a rich equational theory for dependently-typed higher-order imperative programs. Furthermore, both the type theory and its model are relatively simple, even when all of the extensions are considered.

Personally I find the abstract a little over my head, but am excited when I read stuff like, "We would like to fully integrate dependent and linear type theory. Linear type theory would permit us to extend the Curry-Howard correspondence to (for example) imperative programs, and type dependency permits giving very precise types to describe the precise functional behavior of those programs."

Funny how the 'Fair Reactive' paper was just recently mentioned on the ATS list.

My day job involves GUI work on smartphones (pity me) so I like finding out about things like this:

Abstract
We combine visual programming using Google Blockly with a single-threaded implementation of behavioral programming (BP) in JavaScript, and propose design patterns for developing reactive systems such as client-side Web applications and smartphone customization applications as collections of independent cross-cutting scenarios that are interwoven at run time. We show that BP principles can be instrumental in addressing common software engineering issues such as separation of graphical representation from logic and the handling of inter-object scenarios. We also show that a BP infrastructure can be implemented with limited run-time resources in a single-threaded environment using coroutines. In addition to expanding the availability of BP capabilities, we hope that this work will contribute to the evolving directions of technologies and design patterns in developing interactive applications.

The final program from the SPLASH Future of Programming workshop is up. A lot of great videos with a lot of great ideas for the future of our field!

Contents with brief one liners (see the program page for more detailed abstracts):

• Dynamic Organisms in Céu: a new abstraction mechanism for synchronous reactive programming where organisms reconcile objects and threads into a single concept.
• Shadershop: an interface for programming GPU shaders in the mode of a direct manipulation image editor like Photoshop.
• Lamdu - towards a next generation IDE:a structural code editor which mimics the convenience of textual code editing while leveraging its understanding of the code to offer intelligent type-aware completions and significantly simplify complier feedback and type errors.
• Two-way Dataflow: combining the power of frameworks like Rails and iOS with the simplicity of a spreadsheet.
• Moonchild: a toolkit for experimenting with new kinds of programming interfaces, based on a text editor written in HTML and JavaScript.
• Traveling through Time and Code: Omniscient Debugging and Beyond: a prototype of a live coding environment that makes it easy to navigate the execution and extends omniscient debugging with an additional dimension in order to navigate to different versions of the code.
• CodeHint: Dynamic and Interactive Synthesis for Modern IDEs: a technique for synthesizing code that generates and evaluates code at runtime.
• Genyris: a programming paradigm inspired by the semantic web.
• Version Control Optimized for Teaching and Learning: a prototype tool that acts as a version control system that captures very fine grained information about the development process.
• Kaya: Declarative Reactive: a declarative (like SQL) and reactive (like a spreadsheet) language where applications are composed in a spreadsheet-like editor.
• Leisure overview: a document-based computing environment that makes programming fun and let kids (and grownups) open the hood to see what's going on inside.
• Virtual World Framework & OMeta: collaborative programming of distributed objects with user defined languages: a synchronized collaborative 3D environment that allows easy application creation, and provides a simple interface to allow multiple users to interact with the state of the application that is synchronized across clients, using the notion of virtual time.

Antha is a high-level language for biology, making it easy to rapidly compose reproducible work flows using individually testable and reusable Antha Elements.

Recently made open source, the programming system Antha uses flow based programming. They have set up a bioinformatics related set of types in said system.

(I have nothing to do with the project, haven't even used it, but sure wish I could get paid to do so. :-)

From the other thread, I read Relations as First-Class Citizen from which I wonder: If we are seeking good support for compositionality, how might a declarative/calculus approach go wrong? What is it about SQL or Make or whatever else (e.g. random thing IBM's Collage) that might contribute to compositional frustration?

While the declarative style of programming of SQL is very nice for solving very specific and well isolated sub-problems in your requirements & design space, it is of almost no aid for putting the architectural pieces together. Yet, putting the pieces together is something software engineers do every single day. And so is writing algorithms. Exposing a relational algebra therefore appears more natural when it comes to software development, and when it comes to manipulating data vs. querying database. To be fair, libraries such as ARel, Sequel, and jOOQ already show the way: they provide an API that is closer to relational algebra than relational calculus. Alf and Axiom simply go further this path by abstracting from SQL and choosing a sound algebra known as Tutorial D as a better inspiration than SQL towards the same objective.

An algebra is about providing operators for putting operands together, a calculus simply is not.

International Conference on Live Coding
13-15th July 2015, University of Leeds, UK
http://iclc.github.io

With pleasure we announce the initial call for papers and performances for the first International Conference on Live Coding, hosted by ICSRiM in the School of Music, University of Leeds, UK.

This conference follows a long line of international events on liveness in computer programming; the Changing Grammars live audio programming symposium in Hamburg 2004, the LOSS Livecode festival in Sheffield 2007, the annual Vivo festivals in Mexico City from 2012, the live.code.festival in Karlsruhe, the LIVE workshop at ICSE on live programming, and Dagstuhl Seminar 13382 on Collaboration and Learning through Live Coding in 2013, as well as numerous workshops, concerts, algoraves and conference special sessions. It also follows a series of Live Coding Research Network symposia on diverse topics, and the activities of the TOPLAP community since 2004. We hope that this conference will act as a confluence for all this work, helping establish live coding as an interdisciplinary field, exploring liveness in symbolic abstractions, and understanding the perceptual, creative, productive, philosophical and cultural consequences.

The proceedings will be published with ISSN, and there will also be an follow-on opportunity to contribute to a special issue of the Journal on Performance Arts and Digital Media; details will be announced soon.

Timeline

* Templates available and submissions system open: 8th December 2014
* Performance submissions deadline: 16th February 2015
* Paper submissions deadline: 1st March 2015
* Notification of results: 10th April 2015
* Camera ready deadline: 10th May 2015
* Conference: 13-15th July 2015

Submission categories

* Long papers (6-12 pages)
* Short papers (4-6 pages)
* Poster/demo papers (2-4 pages)
* Performances (1-2 page abstract and technical rider)

ICLC is an interdisciplinary conference, so a wide range of approaches are encouraged and we recognise that the appropriate length of a paper may vary considerably depending on the approach. However, all submissions must propose an original contribution to Live Coding research, cite relevant previous work, and apply appropriate research methods.

The following long list of topics, contributed by early career researchers in the field, are indicative of the breadth of research we wish to include:

* Live coding and the body; tangibility, gesture, embodiment
* Creative collaboration through live code
* Live coding in education, teaching and learning
* Live coding terminology and the cognitive dimensions of notation
* Live language and interface design
* CUIs: Code as live user interface
* Domain specific languages, and the live coding ecosystem
* Programming language experience design: visualising live process and state in code interfaces
* Virtuosity, flow, aesthetics and phenomenology of live code
* Live coding: composition, improvisation or something else?
* Time in notation, process, and perception
* Live coding of and inside computer games and virtual reality
* Live programming languages as art: esoteric and idiosyncratic systems
* Bugfixing in/as performance
* Individual expression in shared live coding environments
* Live coding across the senses and algorithmic synaesthesia
* Audience research and ethnographies of live coding
* Live coding without computers
* Live coding before Live Coding; historical perspectives on live programming languages
* Heritage, vintage and nostalgia – bringing the past to life with code
* Live coding in public and in private
* Cultural processes of live programming language design
* General purpose live programming languages and live coding operating systems
* Connecting live coding with ancient arts or crafts practice
* Live coding and the hacker/maker movement: DIY and hacker aesthetics
* Critical reflections; diversity in the live coding community
* The freedom of liveness, and free/open source software

Submissions which work beyond the above are encouraged, but all should have live coding research or practice at their core. Please contact us if you have any questions about remit.

Please email feedback and/or questions to livecodenet@gmail.com

http://iclc.github.io

I want generics, in particular polymorphic functions as well as function overloading based on type-classes. For the moment think about Haskell type-classes and C++ Concepts. I also want code completion. Code completion works for OO languages because they are polymorphic on the object type, which prefixes the function call, and hence the type is known when code completion lookup occurs. Generic functions can be polymorphic on any argument. This suggests that all the arguments need to go before the operator in postfix format. This way code completion can operate on the argument types, and only offer valid generic functions. It can also offer all generic functions that take those arguments in alphabetic order. I want to discuss whether this idea has any merit, and second I want to discuss syntax:

So, a reverse lisp style (likely to confuse people as no clear difference from lisp function first format):

(list comparator sort)

or perhaps reverse C:

(list, comparator) sort

Or perhaps a template C++ like syntax:

<list,comparator>.sort

Or:

list,comparator.sort

I think this paper is a really nice blast from the past.

L is a subset of Common Lisp with multi-processing extensions. It is ideal for use in embedded systems with small computers. The system has a minimal memory footprint and can run on small processors.

Too bad it doesn't seem to be available online anywhere. Might any LtU user have the social network to find it / obtain it / write an eulogy about it?

I enjoyed discussion in Why do we need modules at all? (about Joe Armstrong's post on the same topic) more than anything else on LtU the last few years. Several comments reminded me of something I've been thinking about several years now. But describing it doesn't seem on topic in reply (or, I lack the objectivity to tell). The modules thread is already long, and I don't want to pollute it with junk.

This is mainly about transpiling, where you compile one source to generate another, with a goal of automated rewrite, where both syntax and complexity in the input and output are similar: compiling one language to itself, but re-organized. For example, you can use continuation passing style (CPS) to create fibers (lightweight threads) in a language without them natively, like C. Obviously this is language agnostic. You can add cooperative fibers to any language this way, from assembler to Lisp to Python, as long as you call only code similarly transformed. You're welcome to free associate about this or anything else mentioned, though. For the last year or so, almost all my thinking on the topic has been about environment structure, lightweight process management, and scripts effecting loose coupling relationships via mechanisms similar to Unix, such as piping streams, etc. Once you work out how a core kernel mechanism works, all the interesting parts are in the surrounding context, which grow in weirdly organic ways as you address sub-problems in ad hoc ways. Thematically, it's like a melange of crap sintered together, as opposed to being unified, or even vaguely determined by constraints stronger than personal taste.

Note I'm not working on this, thus far anyway, so treat anything I say as an armchair design. There's no code under way. But I probably put a couple thousand hours thinking into it the last seven years, and parts may have a realistic tone to them, in so far as they'd work. It started out as a train of thought beginning with "how do I make C behave like Erlang?" and grew from there. I've been trying to talk myself into wanting to code parts of it, sometime.

Several folks mentioned ideas in the other thread I want to talk about below, in the context of details in the armchair design problem. (I'll try to keep names of components to a minimum, but it gets confusing to talk about things with no names.) Most of the issues I want to touch deal with names, dependencies, modules, visibility, communication, and the like, in concurrent code where you want to keep insane levels of complexity in control if possible.