Lambda the Ultimate

On page 56 at the top of the page he has the reduction:

( λx . x ( λx . x ) )( u r ) evaluates to u r ( λx . x )

My question is:

I see how the lhs can be written as: (id(id))(ur) which is then (id)(ur). What I don't get is: (id)(ur) = (ur)(id). Is the point that the identity term is commutative in this context? Is this the same idea as the composition operation between functions in that the composition of two functions is generally not commutative, but the identity function is always commutative?

Didn't notice this being mentioned on LtU yet: PLT is going really really un-mutable, which seems like a rather cool and worthy experiment to my mind, and will probably highlight some of the more pragmatic and cultural aspects of managing the development of a language in light of the user community.

For PLT Scheme v4.0, we’re going to try it. In our main dialects of Scheme (such as the mzscheme language), cons will create immutable pairs, and pair? and list? will recognize only immutable pairs and lists. The set-car! and set-cdr procedures will not exist. A new set of procedure mcons, mcar, mcdr, set-mcar!, and set-mcdr! will support mutable pairs.

Given the expanding pool of small multi-core chips (that search doesn't include all of them e.g. ARM, Mips, ...), what "advanced" (at least having garbage collection :-) languages can fit in a small memory space and yet support some form of concurrency which takes advantage of these various architectures? There's two things that would be neat: #1 a chip + language that Just Works but is affordable (e.g. a decent breadboard development kit is < $200), #2 a nice language which would somehow be relatively easy to port to these different architectures.

Is this a compelling thing for neat languages to target? Or are we doomed to hand-roll with C? :-)

I've poked around reading up on some of the usual suspects like Erlang, various Schemes, various concurrent C things, I guess there's OcamlP3L, but I haven't come across any of them clearly being already targeted or easily re-targeted at these whacky chips. (I guess maybe ARM would be the most likely to be targeted but haven't hit pay dirt yet.) Presumably two of the hold-ups are: #1 whacky instruction sets and #2 super small memory space. E.g. something like Spin is not-so-portable I guess. And I don't know how expensive the SEAforth stuff is, or how much I want to be working in Forth.

Also, debugging (sorry if an ad shows up first) might be "fun".

I had a session with Oleg at POPL this year trying to understand the shift/reset control operators and particularly the printf examples of Danvy & Filinski and Asai & Kameyama. Late night thinkings ensued and now I can say I understand this thing a bit better. I've documented the whole development in Coq and Oleg reviewed it now so it should be mostly free of errors. I hope others could be enlightened by this development, it also shows some nice features of programming in dependently-typed languages like Coq, notably having proofs of the actual laws of your structures or writing functions at the type level. Enjoy this fine bit of type theory !

Genuine shift reset

In a post in a different thread, Ben Titzer explains why he doesn't include reflection capabilities in his language Virgil, a language intended for very small and/or deeply embedded systems. In the context of his requirements, the exclusion makes perfect sense.

Introspection (the ability of a program to inspect itself at runtime) is well-established as a powerful facility--especially in languages with otherwise weak typing systems, or in dynamically typed languages. Some argue that it breaks Liskov substitution (as via introspection one can discover the differences between a subtype and a supertype; differences which are not visible from the interface of the type), but it's useful to have around.

But what of reflection--the ability for a running program to *modify* itself--changing subroutines or type definitions "on the fly", and in some cases having extant data objects reconfigured when the underlying schema changes? Many LISPs (culminating in CLOS; far less so in Scheme) are highly reflective, as is Smalltalk. More recently, many of the popular scripting languages feature reflective capabilities. RDBMSs, which generally have no phase distinction as they have to be running 24/7, are highly reflective systems--the schema of a particular relation (table) is defined in a different relation, which can be altered by a user with sufficient authority (a DBA and nobody else, one hopes).

Excluding the RDBMS example, and other high-availability, dynamically-reconfigurable systems--the most common use of reflection capabilities (again, here I mean mutating runtime structures on the fly; not merely inspecting them) seems to be... debugging and development. A common complaint about "traditional" languages with a phase distinction is that the edit/compile/run/debug cycle is too long; and that use of reflection improves programmer productivity. OTOH, many non-reflective languages nowadays come with rapid-turnaround editing environments (whether a REPL or something fancier).

Again excluding databases and such ('cause they've been covered above, not because I don't think they are worth considering)--and now excluding debugging/development--what about production code? Should deployed code, in the general case, ever be using reflection capabilities to "rewrite" itself--epsecially "destructive" changes? What user requirements call for reflective capabilities--requirements which are harder to implement in languages with a phase distinction (and lack of mutability of structures handled in earlier phases)?

Hey again,

I was just working through "Faking It: ..." by Conor McBride.

One of the examples in the paper, he introduces Fridlender & Indrika's variadic zipWith:

(<<) :: [a -> b] -> [a] -> [b]
(f:fs) << (a:as) = (f a) : (fs << as)
_ << _ = []

z = id
s = \n fs as -> n (fs << as)

s :: ([b] -> c) -> [a -> b] -> [a] -> c


And then creates a type-safe version by induction:

data Zero = Zero
data Suc n = Suc n

class Nat n
instance Nat Zero
instance Nat n => Nat (Suc n)

class Nat n => ZipWithN n s t | n s -> t where
manyAppN :: n -> [s] -> t
zipWithN :: n -> s -> t
zipWithN n f = manyAppN n (repeat f)

instance ZipWithN Zero t [t] where
manyAppN Zero fs = fs

instance ZipWithN n t ts => ZipWithN (Suc n) (s -> t) ([s] -> ts) where
manyAppN (Suc n) fs ss = manyAppN n (fs << ss)


_{[Note: This is not exactly how the code appears.]}

To use this, you need to supply a faux-numeric argument like Suc( Suc( ... Zero ... )).

Slightly related is the fact that I just made a linear algebra library based on lists, but would have done it on tuples had there been a (syntactically) nice way of mapping and folding etc. Well, I know that tuples aren't really recursive, but the Faking It: ... paper makes a convincing argument that variadic functions like zipWith can (should) be defined inductively.

This is a vague question about what kind of environment would make this possible. Since it is desirable to remove the numeric argument, I question whether dependent types are really what I want. I haven't delved too much into dependent types, but I feel like this is more about induction on the structure of the function, as opposed to induction on the numerical argument.

It will be a while before I can fully appreciate the power of staging, but some of the stuff I have read here recently by Carette, Kiselyov and Chan looks pretty cool. Jay's work on FISh and program shape analysis looks interesting as well. I also heard (somewhere on here) of Prolog being able to infer structure like this.

My brain works a lot faster than I can learn, and I am really trying to get a feel for what I might study (honors) next year. So thanks if you can find the time to point me in the right direction...

_{[fixed: '(f s)' became '(f a)'. thanks fruehr]}

Hey,

I was just reading the discussion where William Cook is critiquing CTM. In this post, where he is contrasting Objects and ADTs, he says:

...the well-known problem of 'binary methods' in object-oriented programming. It is also one reason why numbers are hard to implement as objects: the operations +, *, / etc all require access to representations unless you are willing to give up a lot of performance. The way Smalltalk handles numbers is really fascinating, and not very well known.

Further down, he illustrates objects as follows:

The argument O is not the Client, the function is the Client:

Client = Fun{Container O}.... {O.get...} {O.put....} ... end.

It gets even more interesting when you have operations that take multiple object values, like "compare dictionary" or "append lists". Then you would have

Client2 = Fun{Container O1, Container O2}.... {O1.append(O2)...} {O2.compare(O1)....} ... end.

In this case the "class" of the two container objects O1 and O2 can be completely unrelated and everything will still work! This is a strong illustration of the power of objects. Again, see my paper on ADT vs OOP for more discussion. This is how numbers work in Smalltalk.

Oz makes me a bit cross-eyed, but this seems a pretty straight-forward use of OO. Hopefully someone can explain why binary operators are so fascinating in Smalltalk...

Cheers...

I'm designing a generic object oriented language, and I would like to replace all of those silly declaration modifiers that you often see (e.g. public, protected, private, internal, const, static, etc.) with annotations. My plan is to introduce a preprocess phase, executed immediately after compilation, that allows the program to verify that the semantics associated with the various annotations are respected.

This phase would be simply a call to some "preprocess" function from the compiler, which uses the langauge's own reflection facilities to allow the programmer to walk the code and verify things. This seems relatively straightforward, but I am concerned that there are well-known pitfalls that in my infinite naivete I may be overlooking. There is of course the really obvious stuff like the possibility of a non-terminating or intractably complex algorithm at compile-time, but that I can live with. Thanks in advance for your suggestions.

In another thread Paul Snively mentions the Logic of Proofs with references to several papers.

The Basic Intuitionistic Logic of Proofs (PDF), Explicit Provability and Constructive Semantics (PS) are two. The third is probably the one most immediately relevant/applicable to LtU.

Reflective lambda-calculus (PS) by Jesse Alt and Sergei Artemov. 2001.

We introduce a general purpose typed λ-calculus λ∞ which contains intuitionistic logic, is capable of internalizing its own derivations as λ-terms and yet enjoys strong normalization with respect to a natural reduction system. In particular, λ∞ subsumes the typed λ-calculus. The Curry-Howard isomorphism converting intuitionistic proofs into λ∞terms is a simple instance of the internalization property of λ∞. The standard semantics of λ∞ is given by a proof system with proof checking capacities. The system λ∞ is a theoretical prototype of reflective extensions of a broad class of type-based systems in programming languages, provers, AI and knowledge representation, etc.

Hello!

I just completed a functional programming course that I enjoyed, so much in fact, I find myself addicted to programming with scheme. I am coming here because I am only a computer science minor, and this one course was my only exposure to functional programming, where we used DrScheme for the course.

We were given a term project, and my submission earned me a free pass from the final exam. The problem was based on a contest problem from our regional 2007 ACM contest, found here http://www.acmgnyr.org/year2007/e.pdf.

I had fun doing it, given my experience in the language it took me quite some time, however it was a fun exercise in working my logic and recursion skills. I am conducting some peer leader workshops at my university, and I would like to use my work as an example, but I think it can be improved, looking at the example below it prints unnecessary top (only when the greatest is on top) 'flips' because of the recursive nature; and the output probably leaves something to desire.

(1 -3 -2)
2 1 3 1 2 1""
(-3 1 -2 -4)
4 1 4 1 1 3 1 2 ""
(1 2 3 4 -5)
5 1 5 4 4 3 3 2 2 ""

There is no money or profit for me to gain from this, and I offer none either, I'm just looking for some willing code discussion! If interested in discussing the program, send me your email or send a request to me a weatherward_AT_gmail

Thank you!