Lambda the Ultimate

Steve Jobs (1955 - 2011) had a profound influence on the computing world. As others discuss his many contributions and accomplishments, I think it is appropriate that we discuss how these affected programming, and consequently programming languages. Bringing to life some of the ideas of the Mother of All Demos, Jobs had a hand in making event loops standard programming fare, and was there when Apple and NeXT pushed languages such as Objective-C and Dylan and various software frameworks, and decided to cease supporting others. Some of these were more successful than others, and I am sure members have views on their technical merits. This thread is for discussing Jobs -- from the perspective of programming languages and technologies.

Update:

Eric Schmidt on Jobs and OOP

Stephen Wolfram on Jobs and Mathematica

The iPhone mandate decision

I'm working on a toy language, intended as a functional implementation of Date and Darwen's vision for a 'D' language to compete with SQL.

Right now, I'm considering how far to go with the ideas in Turner's Total Functional Programming.

Distinguishing data from codata and statically enforcing termination is pretty much entirely a win for this language, I think. Nearly all of the functions and I-wish-they-were-functions-SQL-views-queries-procedures I have in any of my example databases are structurally recursive or have entirely opaque implementations.

Some questions I am stuck on:

• Where do the function types fall on this distinction? They are codata, right, because you can only observe them by applying (~= deconstructing) them? (As an aside, if so, is it possible to write a Turner-style codata declaration that starts codata (->) a b = ? I'm not sure if the answer is yes, no, or not without referencing the built-in (->) type.)
• It seems like equality and serializability, both obviously of interest to a database language, are sensibly defined for precisely those types that are data "all the way down" (counting function types as codata types). True, false, or true-ish-but-distinguish-them-anyway?
• There is a weird thing that happens to function types when the following conditions are met:
  • The argument type and result type are both data types
  • The argument type is "finitely inhabited" (I'm not sure what the real name of this concept is) in that it classifies finitely many values. data DayOfWeek = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday is finitely inhabited, as are Haskell's Int and even Float, but neither Integer nor [DayOfWeek]

  When this happens, the (necessarily total) functions magically look like data again. Taking |t| to be the cardinality of the type t, |a -> b| = |b| ^ |a| when these conditions are met. At least in principle (it might take a long time in some or most cases), we can compare functions of such a type for (extensional) equality by evaluating them at every inhabitant of the argument type. We can serialize them by (there may be more efficient ways, but who cares) serializing this table of results. What's happening here? Could/should a language recognize this special case and allow serializing functions with types like DayOfWeek -> Bool? Or provide conversions to/from Map a b from/to a -> b if and only if these conditions hold? Or ignore this whole thing as an oddity?