Lambda the Ultimate

In the thread on value level programming we started discussing an HM (like) type system with principal typings. Although based on Olaf Chitil and Grego Erdi's work, it seems what I have implemented has significant differences. There is also some influence from Kfoury and Well's System-I and System-E.

Key differences: There is no type environment (as it is compositional), and the typing context is a multi-set instead of a set. This seems equivalent to allowing rank-1 intersection types in the context, but by keeping the types themselves free of intersection operators, a normal HM unification operation can be used, which is decidable.

A few key claims: It is decidable, compositional, and has principal typings.

- I would like comments on the notation for the formal description of the type system, can it be improved?

- I tend to assume everything has been done before, but looking back this seems more original than I thought? Has anyone seen this before or can I count this as its first publication?

As the multi-set context effectively allows rank-1 intersections in the context, but not in the types themselves, a rank-0 intersection type seems a good term for this.

So here's my first attempt at writing the rules:

Rank 0 Intersection Type System Definition:

------------- LIT
{} |- N : Int


---------------- VAR
{x : a} |- x : a

where
    new a


M1 |- E1 : t1    M2 |- E2 : t2
------------------------------ APP
       M |- E1 E2 : t

where
    new a
    SUBS = t1 unify (t2 -> a)
    M = SUBS(M1 multi-set-union M2)
    t = SUBS(a)


 M1 |- E1 : t1
---------------- ABS
M |- \x . E1 : t

where
    new a
    SUBS = empty-substitution-list
    for t' in M1(x):
        SUBS = SUBS append (SUBS(a) unify SUBS(t'))
    M = SUBS(M1 - x)
    t = SUBS(a -> t1)


M1 |- E1 : t1      M2 |- E2 : t2
-------------------------------- LET
   M |- let x = E1 in E2 : t

where
    SUBS = emtpy-substitution-list
    M' = M2 - x
    for t' in M2(x):
        (M1' t1') = SUBS(M1 t1) with fresh free variables
        SUBS = SUBS append (SUBS(t') unify t1')
        M' = M' multi-set-union M1'
    M = SUBS(M')
    t = SUBS(t2)

There are a lot of currying-in-X tutorials floating around, for example I've written my own for Javascript and PHP.

Recently this one appeared on Hacker News and I got involved in the discussion, which made me think a bit harder about a peculiarity of my implementations which I've not seen in anyone else's.

My blog post on PHP discusses this peculiarity in the "Returning Functions" section. My Javascript implementation linked above was written before this discovery, but I've detailed it in this followup.

The idea with all implementations is that we make a 'curry' function such that the following hold:

// Curry a function
var curried = curry(function(a, b, c) { return [a, b, c]; });

// By the definition of currying
curried(x)(y)(z) == [x, y, z]

// For convenience and interoperability
curried(x, y, z) == curried(x)(y, z)
                 == curried(x, y)(z)
                 == curried(x)(y)(z)
                 == [x, y, z]

The difference in my implementations is what happens when we're given more arguments than the function's arity:

// Curry another function
var two_level = function(a, b, c) {
                  return function(d, e, f) {
                    return [a, b, c, d, e, f];
                  };
                };
var curried2 = curry(two_level);

// Most implementations pass all arguments once arity has been reached
curried2(u, v, w, x, y, z) == two_level(u, v, w, x, y, z)
                           == function(d, e, f) {
                                return [u, v, w, d, e, f];
                              };

// My implementations only pass the minimum number; the rest go to the return value
curried2(u, v, w, x, y, z) == two_level(u, v, w)(x, y, z)
                           == [u, v, w, x, y, z]

Two consequences of this are:

• All function arities become constant (though overridable via wrappers)
• Currying a manually-curried function (ie. a function which returns a function) will *uncurry* it, allowing both levels to be called as one!

My current implementations either pass all remaining arguments to the first return value (PHP) or pass one argument at a time to successive return values (Javascript; essentially "foldl ($) f args"). These work best when the returned functions are also curried, but there's no reason we can't curry them on-the-fly, or look up how many to supply and loop until we run out. We could even use such a loop to execute tail-calls while we're at it ;)

This uncurrying is effectively the same as the convenience functionality shown in the first code block, but extended to our return values as well as our arguments. In other words:

When we have too few values, we produce wrapper functions to accept the leftovers as their arguments.
When we have too many values, we consume wrapper functions by passing the leftovers as their arguments.

I'd love to hear people's opinions on this. Is my approach better, worse or complementary to the standard approach? Has this duality been noticed before? Is this just a reason not to use n-ary functions? ;)

Edit: In case you can't tell, my aim is to have expressions like "a(b, c, d, e, f, g, ...)" behave like a Haskell expression "a b c d e f g ...".

Sophia Drossopolou, Greg Meredith, and I have written a paper demonstrating that we can use Caires' behavioral-spatial types to write security policies for objects in an ocap-secure language; then it's possible for the compiler to statically check that the implementation satisfies the policy. In an object capability language, dependency injection is the only way you get access to any ability to side-effect the world; all authority is embodied in object references, which are unforgeable. To deny someone the ability to perform an action, you simply do not give them a reference to the object that performs it. We focused on demonstrating that we can type deniability in the paper.

Lucius G Meredith, Mike Stay, Sophia Drossopoulou, "Policy as Types".

Greg and I are currently seeking crowdfunding to build a platform called splicious; should we get funded, part of our plan is to port the spatial logic model checker to Scala and add spatial-behavioral types as annotations with a plugin.

I have a meager syntax proposal and am curious if anyone has explored this design, knows of a language that uses it, or can think of a problem with it. It's comprised of two aspects that work together to support certain idioms in a neighborhood of Haskell syntax.

The first aspect is to generalize sectioning of binary operators to chains of binary operators where the first and/or last operand in the chain is missing. Here's a GHCi interaction:

Prelude> (1 + 2*)

    The operator `*' [infixl 7] of a section
        must have lower precedence than that of the operand,
          namely `+' [infixl 6]
        in the section: `1 + 2 *'

So Haskell doesn't like the expression (1 + 2*). The proposal is that this would instead be a section of an operator chain, equivalent to (λx. 1 + 2*x). Similarly for (*2 + 1).

The second aspect is to use dot for reverse application (rather than composition). That is,

x.f = f x

Dot and juxtaposition would have equal precedence allowing an OOP-like style (after modifying map and filter to take the list first):

[1, 2, 3].map (+1).filter (>2)  ===  filter (map [1, 2, 3] (+1)) (>2) 

In combination with the first aspect, we can recover composition as:

f `compose` g = (.g.f)

And in general we can capture the tails of OOP-like expressions like this:

frob = (.map (+1).filter (>2))

Has anyone used or seen this approach or does anyone see problems with it?

I was very inspired by the post Scrap your type classes by Gabriel Gonzalez, where he proposes to pass around explicit dictionaries instead of defining instances of type classes. That leads to a distinct style of programming that we may call "value-level programming", where you avoid using any kind of type-directed dispatch and instead pass values around.

To show some examples of that style, I wrote a couple blog posts translating generic algorithms from the C++ STL into Java. Where the C++ version uses implicit concepts like "forward iterator" that the types must satisfy, I pass around explicit objects describing these concepts, while keeping the type parameters completely generic. That way you can e.g. use built-in Integers as iterators. The only features used are Java interfaces and basic generics (no type bounds, etc.)

In the first post, I do a line by-line translation of the STL algorithm std::partition into Java, in a way that works on both Java's built-in arrays and arbitrary user-defined containers. In the second post, I explore a technique to simulate template specialization from C++, like using a more efficient version of an algorithm when a forward iterator is actually a random access iterator, and demonstrate it with a translation of std::advance.

A nice programming language feature to support that style could be something like Agda's instance arguments, to avoid passing around explicit dictionaries all the time. Another related idea can be found in Oleg Kiselyov's delimcc library, where "throwing" and "catching" a specific exception uses a specific value as a point of communication, instead of using the exception's type. It's interesting to translate programming idioms from "type-level" to "value-level" in this way, because it often makes things simpler and more first-class.

What do you think?

I'd like to draw attention to the TechEmpower Web Framework Benchmarks, which compare solutions to simple web programming tasks in different programming languages and frameworks. For now, the formal comparison is entirely about performance, in particular throughput and latency. I believe the long-term plan is to expand to include measures of code complexity, memory usage, and other good stuff.

Eric Easley and I contributed a solution in Ur/Web, a statically typed, purely functional DSL. It's managing to compete pretty well, despite a configuration error that should be fixed for the next round. You, too, can contribute to future rounds! I think it would be great to see languages further outside the mainstream represented!

On the functional programming front, there are already solutions in Erlang, Haskell, and Racket, as well as more "mainstreamed" hybrid languages like Clojure and Scala. Other popular scrappy newcomers include D, Dart, and Go. I think Ur/Web is the most avant-garde language currently represented, and I challenge LtUers to one-up us on that front!

I saw a link to the Mezzo programming language on Hacker News, and I came here to see what had already been discussed. To my surprise there seems to be hardly a mention about it. So I figured I'd post and perhaps stir up a discussion.

According to the Mezzo website the language has been formalized in Coq and is:

... a programming language in the ML tradition, which places strong emphasis on the control of aliasing and access to mutable memory. A balance between simplicity and expressiveness is achieved by marrying a static discipline of permissions and a dynamic mechanism of adoption and abandon.

A PLDI 2014 paper by Yufei Cai et al; abstract:

If the result of an expensive computation is invalidated by a small change to the input, the old result should be updated incrementally instead of reexecuting the whole computation. We incrementalize programs through their derivative. A derivative maps changes in the program’s input directly to changes in the program’s output, without re-executing the original program. We present a program transformation taking programs to their derivatives, which is fully static and automatic, supports first-class functions, and produces derivatives amenable to standard optimization.

We prove the program transformation correct in Agda for a family of simply-typed -calculi, parameterized by base types and primitives. A precise interface specifies what is required to incrementalize the chosen primitives. We investigate performance by a case study: We implement in Scala the program transformation, a plugin and improve performance of a nontrivial program by orders of magnitude.

I'm skeptical of the differential approach, which to me seems wouldn't scale in general. But its a very interesting read regardless.

A new version of Moony Parser is out (namely 2.3). It is a javascript library that implements "Earley" algorithm which makes it CFG complete. It provides a custom cool structurized grammar definition language that is more readable and more compact than BNF or PEG languages.

U can try it online on web page: Moony Parser

It features cool HTML based grammar testing environment.

A CHI 2014 paper by Tom Lieber et al, abstract:

We present Theseus, an IDE extension that visualizes run-time behavior within a JavaScript code editor. By displaying real-time information about how code actually behaves during execution, Theseus proactively addresses misconceptions by drawing attention to similarities and differences between the programmer's idea of what code does and what it actually does. To understand how programmers would respond to this kind of an always-on visualization, we ran a lab study with graduate students, and interviewed 9 professional programmers who were asked to use Theseus in their day-to-day work. We found that users quickly adopted strategies that are unique to always-on, real-time visualizations, and used the additional information to guide their navigation through their code.

Edit: up to date paper linked in.