Lambda the Ultimate

I wonder whether there is work on the idea of minimally typing a program. Assume that I have a program and a property I wish it satisfies. Is there a way to derive the least amount of typing to apply to the program such this property is satisfied?

I'd like to implement a language with polymorphic variants, but instead of using pattern matching, I'd like to use Common Lisp-like generic functions that are defined with define-generic, and to which cases can be added with define-method.

Where in pseudo-ML I'd say

let length list =
  case list of 
    `Nil -> 0
  | `Cons _ cdr -> 1 + length cdr

in my language I'd say

(define-generic length)
(define-method (length `Nil) 0) 
(define-method (length (`Cons _ cdr)) (+ 1 (length cdr))) 

I'd like to able to add methods in different compilation units, and only type-check generic functions at the end of compile-time, once all methods are known. Another possibility might be to defer type checking of generic functions to link time.

Any ideas or pointers to things I should check out? I'm currently reading Simple Type Inference for Structural Polymorphism, and TAPL is lying on the coffee table.

A new ACM conference focused on High-Integrity Language Technology is coming to Boston in Dec. 2012. Keynote speakers at HILT2012 include programming language luminaries Barbara Liskov of MIT, Greg Morrisett of Harvard, and Guy Steele of Oracle Labs. Guy Steele wrote the original two Lambda the Ultimate ... papers, and is the father (or at least the sage uncle) of many important programming languages. Barbara Liskov is of course a recent ACM Turing Award winner, and brought the whole notion of abstraction to modern programming languages, and Greg Morrisett is a pioneer in providing secure programming at the very lowest levels of abstraction. Information on all five of the keynotes, the overall schedule, registration, and accommodations is available at:

  http://www.sigada.org/conf/hilt2012

Functional programming is based on useful and practical ideas. Unfortunately, there is a problem with how functional programs look. They are often hard to read.

Improving the visual appearance of functional programs can make them easier to understand. One way of doing it is to combine some existing functional language with a graphic notation.

DRAKON-Erlang is an attempt to do so. This hybrid language can be described as Erlang that uses DRAKON for flow control.

Each of these two technologies have been successful on their own.

DRAKON was developed within the Russian space program. It was used in Buran, Sea Launch and other space projects. The strong point of DRAKON is that it makes algorithms easier to understand by relying on ergonomics.

Erlang is one of the most widely used functional languages. It started its path in telecom and later spread out to many other industries. Erlang is well known for its simplicity, reliability and built-in support for concurrent programming.

Read more: http://drakon-editor.sourceforge.net/drakon-erlang/intro.html

http://www.typescriptlang.org

TypeScript starts from the syntax and semantics that millions of JavaScript developers know today.

TypeScript types let you define interfaces between software components and to gain insight into the behavior of existing JavaScript libraries.

Suppose we have the typical immutable list, with some immutable operations:

type 'a list = Nil | Cons 'a * 'a list
let head l = match l with Nil -> raise "Error!" | Cons(x,next) -> x
let add l x = Cons(x,l)
let map f l = match l with Nil -> Nil | Cons(x,next) -> Cons(f x, map f next)
...
let update l item newitem = match l with
    Nil as cur -> cur
  | Cons(x,next) as cur ->
      if item = x then Cons(newitem, next)
      else let u = update next item newitem in 
            if u = next then cur else Cons(x, u)
let append x l = match l with Nil -> Cons(x, Nil) | Cons(x,next) -> Cons(x, append x next)
...

Is there any reason in principle we wouldn't be able to derive a mutable version automatically? At first blush, mutability seems somewhat distributive up to polymorphic parameters. Any recursive function on abstraction Foo that returns a Foo of the exact same type is an mutable update candidate.

Transforming outwards-in on a Foo:

1. Return types are replaced by unit.
2. Arguments of type Foo become "mutable Foo".
3. A recursive call propagates the update forwards.
4. For any application of the same Foo constructor to function arguments and referencing the remainder of the data structure, an in-place update for the closest mutable variable is inserted.
5. For any application of a different Foo constructor than the one just matched, the in-place update bubbles up to the previous activation frame.
6. Any code that simply returns the current element is eliminated.

This translation is predicated on a "mutable Foo" being like a "ref Foo". The derived mutable abstraction would look something like:

let mutable 'a list = Nil | Cons mutable 'a * mutable 'a list

let update l item newitem = match !l with
   Nil -> ()
 | Cons(x,next) as cur ->
     if item = !x then x := newitem
     else update next item newitem

let append x l = match !l with Nil as x -> l := Cons(x, Nil) | Cons(x,next) -> append x next

I can't think of any language that allows this, or any work along these lines, but I don't really know what to search for. It seems like it would be a pretty handy language feature though. Sometimes you really need a mutable data structure, and even though you have a perfectly good immutable equivalent at hand for which the mutable version seems like a mechanical translation, you still have to translate it by hand.

Can anyone provide pointers to work like this or explain the difficulties why it's not feasible in general?

I was skimming through Sipser the other day and came across an anomaly I believe I may have encountered before (I think I recall reading this sometime in 1997 for the first time). It points to something I dont quite understand about the P = NP question so I decided to do some scribbling on a note pad and type it up in latex.

The question I had points to the following:

1) Why don't TM based trie (radix-tree) like data structures trivially decide any language in O(n) time (and thus yield a trivial solution to P = NP since every deterministic Turing Machine is a nondeterministic one)?

2) If this is the case it would seem that there is something wrong with the definitions of NP and P in that having a DTM or NTM decide a language may not be strong enough to capture what someone means by a language.

3) There are obviously cases of languages that seem to be decided by algorithms which are in NP but not P. An example would be something like a generalized password cracking tool akin to John the Ripper(for those security gurus).

I tossed it up on google docs here:

https://docs.google.com/open?id=0B8BIjzf4onOFeFk2cVpyY3hkemM

I am curious if there was anything wrong with my reasoning.

A lot of posts here are about how to show a language to be well-behaved for some definition of well-behaved.

How about the opposite? How do we construct a language which, while it has a well-behaved and consistent subset, also allows us to reproduce and demonstrate every kind of important semantic problem and ambiguity that a student needs to be aware of and understand? Or serve as a "direct" translation target for programs written in languages that had those problems?

By "direct" I mean we may need to define operations and locally transform syntax to the new language, but we wouldn't need to write an interpreter to achieve, eg, their problematic calling discipline or argument passing or exception handling or the way their dynamic environments interfered with their macrology.

Ideally, the constructions that are connected to known problems would form a "minimal set" -- ie, we would like to introduce the smallest number of such constructs possible to get a complete map of these problems, and be able to demonstrate each concept.

So what would you look for in a language intended to demonstrate *unsafe* behavior, especially in correct implementations of features that some reasonably smart people once thought were good ideas?

Ray

Another feature on which we scratched our heads in Opa is the records (and variants, as it turns out to be) structure named Power Rows.

I wrote a couple of blog posts that detail them. The articles are intended to a less PL-savvy audience, but it might interest some of you.

Bret Victor wrote another great essay, Learnable Programming: Designing a programming system for understanding programs, in the wake of StrangeLoop.

The goals of a programming system should be:

• to support and encourage powerful ways of thinking
• to enable programmers to see and understand the execution of their programs

A live-coding Processing environment addresses neither of these goals. JavaScript and Processing are poorly-designed languages that support weak ways of thinking, and ignore decades of learning about learning. And live coding, as a standalone feature, is worthless.

Alan Perlis wrote, "To understand a program, you must become both the machine and the program." This view is a mistake, and it is this widespread and virulent mistake that keeps programming a difficult and obscure art. A person is not a machine, and should not be forced to think like one.

How do we get people to understand programming?

We change programming. We turn it into something that's understandable by people.

Bret Victor writes in a flowing, highly accessible, and richly exampled style that I have, perhaps unfairly, come to expect from him. This essay will be of great interest to anyone who is exploring live programming, interactive programming, augmented programming, or integration of programming language with development environment.

TOPLAP, a community for live coding since 2004, provides a little extra context for the essay.