Lambda the Ultimate

Subscribe to Lambda the Ultimate feed
Updated: 2 days 16 hours ago

LtU now supports Mathjax

Tue, 04/15/2014 - 18:56

Categories:

Engineering

LtU now supports MathJax, which allows the use of TeX markup in posts and comments. Note that only TeX/LaTeX markup is currently supported - the alternate MathML format conflict's with the blog's HTML sanitization.

This enhancement is dedicated to neelk, who most recently suggested this feature just over a year ago.

When I went searching for a bit of Mathjax-compatible LaTeX that was relevant to programming languages, the first good example Google found for me was on Neel's blog:

$$
\newcommand{\val}[1]{\mathsf{val}\,{#1}}
\newcommand{\rule}[2]{\frac{\array{#1}}{#2}}
\newcommand{\judge}[3]{{#1} \vdash {#2} : {#3}}
\newcommand{\letv}[3]{\mathsf{let}\;{#1} = {#2}\;\mathsf{in}\;{#3}}
\begin{array}{ll}
\rule{\judge{\Gamma}{e}{A}}
{\judge{\Gamma}{\val{e}}{T(A)}}
&
\rule{\judge{\Gamma}{e}{T(A)} \qquad
\judge{\Gamma, x:A}{e'}{T(C)}}
{\judge{\Gamma}{\letv{\val{x}}{e}{e'}}{T(C)}}
\end{array}
$$

Copy-pasting the above and making it work immediately made it clear that we're going to need a package of useful macros. But it's a start. Feedback welcome.

Note that MathJax rendering is entirely client-side - if you don't see a well-formatted formula above, check the MathJax browser compatibility page and their FAQ.

The broad ML Family workshop

Thu, 04/10/2014 - 07:19

Categories:

Engineering
It is not generally proper to post call-for-papers on LtU. Exceptions have been made, for broad workshops likely to appeal to many LtU readers. I hope the 2014 ML Family workshop also qualifies.

The ML Family workshop intends to attract the entire family of ML languages, whether related by blood to the original ML or not. Our slogan is ``Higher-order, Typed, Inferred, Strict''. Designers and users of the languages fitting the description have many issues in common, from data representation and garbage collection to fancy type system features. As an example, some form of type classes or implicits has been tried or been looked into in several languages of the broad ML family. We hope the ML Family workshop is a good forum to discuss these issues.

Also new this year is a category of submissions -- informed opinions -- to complement research presentation, experience reports and demos. We specifically invite arguments about language features, be they types, garbage collection, implicits or something else -- but the arguments must good and justified. Significant personal experience does count as justification, as do empirical studies or formal proofs. We would be delighted if language implementors or long-time serious users could tell, with examples from their long experience, what has worked out and what has not in their language.

The deadline for submitting an abstract of the presentation, up to 2 PDF pages, is in a month. Please consider submitting and attending!

F# compiler, library and tools now open for community contribution

Mon, 04/07/2014 - 16:22

Categories:

Engineering

F# is the first MS language to go open source. The F# team is now going further into the Open World to allow community contributions to the core language, library and tool set. This means the F# team will now take pull requests :)

From a recent blog post on the topic:

"Prior to today (April 3, 2014), contributions were not accepted to the core implementation of the F# language. From today, we are enabling the community to contribute to the F# language, library and tools, and to the Visual F# Tools themselves, while maintaining the integrity and unity of the F# language itself.

In more detail:
•Contributions can now be made to the core F# compiler, library and tools implementation.
•Proposed changes will be rigorously moderated by ourselves and other community contributors from Microsoft Research and the F# community.
•The full tests for the F# compiler and library are now available.
•In time, the full source code and test suite for the Visual F# Tools will be made available."

.NET Compiler Platform ("Roslyn")

Fri, 04/04/2014 - 06:21

Categories:

Engineering

The .NET Compiler Platform (Roslyn) provides open-source C# and Visual Basic compilers with rich code analysis APIs. You can build code analysis tools with the same APIs that Microsoft is using to implement Visual Studio!

In a nutshell: OPEN SOURCE C# COMPILER. Putting aside possible practical implications of this for the .NET ecosystem, I think it is good for programming language geeks to be able to peruse the source code for compilers and language tools.

For the debate about MS being evil, you can head directly to HN where you'll also find an explanation of what bootstrapping a compiler means.

Future of Programming workshop

Thu, 04/03/2014 - 23:36

Categories:

Engineering

The call for submissions is out. There will be two opportunities this first year to participate: at Strangeloop in September and at SPLASH in October. The call:

We are holding two events. First, in partnership with the Emerging Languages Camp, FPW×ELC will be at Strange Loop on September 17 in St. Louis MO. Second, at SPLASH in Portland OR around Oct. 19 (pending approval).

We want to build a community of researchers and practitioners exploring the frontiers of programming. We are looking for new ideas that could radically improve the practice of programming. Ideas too embryonic for an academic paper yet developed enough to demonstrate a prototype. Show us your stuff!

FPW×ELC will present live demonstrations before an audience. The SPLASH event will be an intense, private writer’s workshop1,2. This process will be a chance to give and take both creative support and incisive criticism.

Submissions will be 15 minute demo screencasts. You can select either or both of the events in your submission. The submission deadline is June 8 and notifications will be sent June 27. After the events participants will have until December 1 to revise their screencasts for archival publication on our website. The submission site is now open. For questions please see the FAQ or ask info@future-programming.org.

Brought to you by Richard Gabriel, Alex Payne, and Jonathan Edwards.

This is a good idea for the more edgy language designers to exhibit their work and receive useful critique to improve presentation, which ultimately helps with our goal of world domination (or at least, pushing the community to take more risks).

Functional Geometry and the Traite ́ de Lutherie

Thu, 04/03/2014 - 01:29

Categories:

Engineering

Functional Geometry and the Traite ́ de Lutherie by Harry Mairson, Brandeis University.

We describe a functional programming approach to the design of outlines of eighteenth-century string instruments. The approach is based on the research described in Francois Denis’s book, Traite ́ de lutherie. The programming vernacular for Denis’s instructions, which we call functional geometry, is meant to reiterate the historically justified language and techniques of this musical instrument design. The programming metaphor is entirely Euclidean, involving straightedge and compass constructions, with few (if any) numbers, and no Cartesian equations or grid. As such, it is also an interesting approach to teaching programming and mathematics without numerical calculation or equational reasoning.

The advantage of this language-based, functional approach to lutherie is founded in the abstract characterization of common patterns in instrument design. These patterns include not only the abstraction of common straightedge and compass constructions, but of higher-order conceptualization of the instrument design process. We also discuss the role of arithmetic, geometric, harmonic, and subharmonic proportions, and the use of their rational approximants.

Study finds that when no financial interests are involved programmers choose DECENT languages

Tue, 04/01/2014 - 05:01

Categories:

Engineering

For immediate release. By studying the troves of open source software on the github service, a recent (and still unpublished) study by a team of empirical computer scientists found that programmers prefer to use DECENT languages. DECENT languages were defined by the team to be languages that conform to a set of minimal ethical standards, including clean syntax, expressive type systems, good package managers and installers, free implementations, no connection to the military-industrial complex and not harming animals. The researchers argue that their data support the view that the prevalent use of indecent languages, Java in particular, is the result of money influencing programmer decisions. The principal author of the study notes that DECENT languages do not necessarily make the most MORAL choices (e.g., many of them are not statically typed). He attributed this to a phenomenon called the "weakness of the will."

Details to follow.

Brendan Eich, CEO of mozilla

Mon, 03/24/2014 - 23:34

Categories:

Engineering

Correct me if I'm wrong, but I think this is the first case of a language designer making it to the top slot of a company!

Facebook Introduces ‘Hack,’ the Programming Language of the Future

Fri, 03/21/2014 - 15:11

Categories:

Engineering

From Wired, Facebook Introduces ‘Hack,’ the Programming Language of the Future

You can think of Hack as a new version of PHP. It too runs on the Hip Hop Virtual Machine, but it lets coders use both dynamic typing and static typing. This is what’s called gradual typing, and until now, it has mostly been an academic exercise. Facebook, O’Sullivan says, is the first to bring gradual typing to a “real, industrial strength” language.

Hack is open source and is available at hacklang.org. It supports type annotation, generics, lambdas and host of other features on top of PHP.

Propositions as Types

Fri, 03/07/2014 - 16:38

Categories:

Engineering

Propositions as Types, Philip Wadler. Draft, March 2014.

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.

Philip Wadler has written a very enjoyable (Like busses: you wait two thousand years for a definition of “effectively calculable”, and then three come along at once) paper about propositions as types that is accessible to PLTlettantes.

Haxe 3.1 is here

Tue, 03/04/2014 - 22:41

Categories:

Engineering

Haxe 3.1 is here. It is a language that is sorta rooted in the bog-standard main-stream (it came out of Action/Ecma scripts), but has gradually (especially in the move from 2.0 to 3.0+) been adding some of its own ideas. I've used 2.x for making cross-platform games. I sorta love/hate it, but I'd certainly be a lot more sad if it stopped existing, having known it (not in the biblical sense or anything). There's probably too many random things to go into any detail here, but I'll try to summarize it as: A cross-platform (compiles down to other languages) statically and dynamically typed (including structural typing) language and libraries, with some nifty typing ideas/constructs and syntax of its own. Oh, and: macros. (But it has seemingly weird lapses, like I dunno that it will ever really support The Curiously Recurring Template Pattern, tho which I find personally sad).

Wirth Symposium

Fri, 02/28/2014 - 13:47

Categories:

Engineering

Celebrating Niklaus Wirth's 80th Birthday, 20th Feb 2014.

Niklaus Wirth was a Professor of Computer Science at ETH Zürich, Switzerland, from 1968 to 1999. His principal areas of contribution were programming languages and methodology, software engineering, and design of personal workstations. He designed the programming languages Algol W, Pascal, Modula-2, and Oberon, was involved in the methodologies of structured programming and stepwise refinement, and designed and built the workstations Lilith and Ceres. He published several text books for courses on programming, algorithms and data structures, and logical design of digital circuits. He has received various prizes and honorary doctorates, including the Turing Award, the IEEE Computer Pioneer, and the Award for outstanding contributions to Computer Science Education.

We celebrated Niklaus Wirth's 80th birthday at ETH Zürich with talks by Vint Cerf, Hans Eberlé, Michael Franz, Bertrand Meyer, Carroll Morgan, Martin Odersky, Clemens Szyperski, and Kathleen Jensen. Wirth himself gave a talk about his recent port of Oberon onto a low-cost Xilinx FPGA with a CPU of his own design.

The webpage includes videos of the presentations.

Determinism Is Not Enough: Making Parallel Programs Reliable with Stable Multithreading

Thu, 02/27/2014 - 20:10

Categories:

Engineering

Junfeng Yang, Heming Cui, Jingyue Wu, Yang Tang, and Gang Hu, "Determinism Is Not Enough: Making Parallel Programs Reliable with Stable Multithreading", Communications of the ACM, Vol. 57 No. 3, Pages 58-69.

We believe what makes multithreading hard is rather quantitative: multithreaded programs have too many schedules. The number of schedules for each input is already enormous because the parallel threads may interleave in many ways, depending on such factors as hardware timing and operating system scheduling. Aggregated over all inputs, the number is even greater. Finding a few schedules that trigger concurrency errors out of all enormously many schedules (so developers can prevent them) is like finding needles in a haystack. Although Deterministic Multi-Threading reduces schedules for each input, it may map each input to a different schedule, so the total set of schedules for all inputs remains enormous.

We attacked this root cause by asking: are all the enormously many schedules necessary? Our study reveals that many real-world programs can use a small set of schedules to efficiently process a wide range of inputs. Leveraging this insight, we envision a new approach we call stable multithreading (StableMT) that reuses each schedule on a wide range of inputs, mapping all inputs to a dramatically reduced set of schedules. By vastly shrinking the haystack, it makes the needles much easier to find. By mapping many inputs to the same schedule, it stabilizes program behaviors against small input perturbations.

The link above is to a publicly available pre-print of the article that appeared in the most recent CACM. The CACM article is a summary of work by Junfeng Yang's research group. Additional papers related to this research can be found at http://www.cs.columbia.edu/~junfeng/

Jeeves

Wed, 02/26/2014 - 18:33

Categories:

Engineering

It is increasingly important for applications to protect user privacy. Unfortunately, it is often non-trivial for programmers to enforce privacy policies. We have developed Jeeves to make it easier for programmers to enforce information flow policies: policies that describe who can see what information flows through a program. Jeeves allows the programmer to write policy-agnostic programs, separately implementing policies on sensitive values from other functionality. Just like Wooster's clever valet Jeeves in Wodehouse's stories, the Jeeves runtime does the hard work, automatically enforcing the policies to show the appropriate output to each viewer.

From what I gather, Jeeves taken Aspect Oriented approach to privacy. This is of course not a new idea. I presume that many of the classic problems with AOP would apply to Jeeves. Likewise, using information flow analysis for handling privacy policies is not an new idea. Combining the two, however, seems like a smart move. Putting the enforcement at the run-time level makes this sound more practical than other ideas I have heard before. Still, I personally think that specifying privacy policies at the end-user level and clarifying the concept of privacy at the normative, legal and conceptual levels are more pressing concerns. Indeed, come to think of it: I don't really recall a privacy breach that was caused by a simple information flow bug. Privacy expectations are broken on purpose by many companies or data breaches occur when big databases are shared (recall the Netflix Prize thing). Given this, I assume the major use-case if for Apps, maybe even as a technology that someone like Apple could use to enforce the compliance of third-party Apps to their privacy policies.

I haven't looked too closely, so comments from more informed people are welcome.

Jeeves is implemented as a embedded DSL in Scala and Python.

The marriage of bisimulations and Kripke logical relations

Wed, 01/29/2014 - 13:18

Categories:

Engineering
CK Hur, D Dreyer, G Neis, V Vafeiadis (POPL 2012). The marriage of bisimulations and Kripke logical relations. There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages---that is, languages that combine features like higher-order functions, recursive types, abstract types, and general mutable references. Two of the most prominent types of techniques to have emerged are bisimulations and Kripke logical relations (KLRs). While both approaches are powerful, their complementary advantages have led us and other researchers to wonder whether there is an essential tradeoff between them. Furthermore, both approaches seem to suffer from fundamental limitations if one is interested in scaling them to inter-language reasoning.

In this paper, we propose relation transition systems (RTSs), which marry together some of the most appealing aspects of KLRs and bisimulations. In particular, RTSs show how bisimulations' support for reasoning about recursive features via coinduction can be synthesized with KLRs' support for reasoning about local state via state transition systems. Moreover, we have designed RTSs to avoid the limitations of KLRs and bisimulations that preclude their generalization to inter-language reasoning. Notably, unlike KLRs, RTSs are transitively composable. I understand the paper as offering an extension to bisimulation that handles the notion of hidden transitions properly and so allows a generalisation of KLRs to any systems that can be treated using bisimulations. Applications to verified compilation are mentioned, and everything has been validated in Coq.

POPL 2014 proceedings available freely for all

Sat, 01/18/2014 - 07:18

Categories:

Engineering

The proceedings can be downloaded from the POPL webpage.

I find this extremely exciting (not only because I didn't get funds to attend POPL this year). To my knowledge, this is the first time that this is done in POPL/ICFP/PLDI; electronic proceedings were previously only delivered to attendees, with an explicit request not to share them.

I am not sure what is the reasoning that make which people decide to do it this year, or not to do it before. I hope that the proceedings will remain available after the conference (next week), and that this idea will be adopted for the years to come.

Multiple Dispatch as Dispatch on Tuples

Thu, 01/09/2014 - 14:10

Categories:

Engineering

Multiple Dispatch as Dispatch on Tuples, by Gary T. Leavens and Todd D. Millstein:

Many popular object-oriented programming languages, such as C++, Smalltalk-80, Java, and Eiffel, do not support multiple dispatch. Yet without multiple dispatch, programmers find it difficult to express binary methods and design patterns such as the "visitor" pattern. We describe a new, simple, and orthogonal way to add multimethods to single-dispatch object-oriented languages, without affecting existing code. The new mechanism also clarifies many differences between single and multiple dispatch.

Multimethods and multiple dispatch has been discussed numerous times here on LtU. While the theory has been fully fleshed out to the point of supporting full-fledged type systems for multiple dispatch, there has always remained a conceptual disconnect between multimethods and the OO model, namely that methods are supposed to be messages sends to objects with privileged access to that object's internal state. Multimethods would seem to violate encapsulation inherent to objects, and don't fit with the conceptual messaging model.

This paper goes some way to solving that disconnect, as multiple dispatch is simply single dispatch on a distinct, primitive class type which is predicated on N other class types and thus supporting N-ary dispatch. This multiple dispatch support can also be retrofitted to an existing single-dispatch languages without violating its existing dispatch model.

Oral History of Adele Goldberg

Tue, 01/07/2014 - 18:36

Categories:

Engineering

Interesting and wide-ranging interview with Adele Goldberg from Computer History
Transcript and Video at Computer History Also on YouTube

Adele Goldberg reflects on her life and career from her early days at the University of Chicago and Stanford University through her career at Xerox Palo Alto Research Center (PARC) and ParcPlace Systems.

Another Oral History interview with her by IEEE Global History Network

Goldberg discusses her educational and work history. She recalls her experiences as a student at the University of Michigan and at the University of Chicago. Next, she covers her stretch at Xeorx PARC, sharing her views on the work environment. Here she speaks at length about her work on Smalltalk, including her leading role in its commercialization. Goldberg is candid about the challenges she faced in forming and running spin-out company ParcPlace Systems. In addition, she discusses her two-year tenure as President of ACM. Finally, Goldberg offers advice for young women who are considering a career in computing.