Lambda the Ultimate

Once upon a time we might have leavened the LtU fare with lighter articles like this The Problem with Programming, Bjarne Stroustrup interview

Now I see that stuff on programming.reddit.com

Hello Everyone,
I have posted an alpha version of a new Object System Library that I'm writing in Scheme (currently using MzScheme only). It combines the Prototypes with Multiple Dispatch object model from the Slate programming language (as described in this document) with Method Combination from CLOS (as described in section ten of this document), to create an object system which I believe to be novel (having found no evidence to the contrary). It is available from the project page or directly from the download site.

I have not had much time to work on it, so it currently only has some debug behavioral print-outs, but if anyone's interested, I could clean up the code into a portable library, and perhaps document it a bit more.

Feedback is appreciated,
Ryan Kaulakis

Note: This is an update from this earlier post.

Hello Lambdans:

Under the influence of tryptophan, I published a blog post giving a hobbyist's perspective on The Significance of the Meta-Circular Interpreter.

My blog's audience are mainly comprised of other hobbyists and professional programmers who dream of escape from their BigCo humdrum. As you would expect, the post lacks academic rigour and some feedback on factual errors would improve it greatly. One early version conflated self-hosting, self-interpreting, and meta-circular evaluation. Thanks to an early comment, I was able to revise the content.

What are your thoughts on the significance of languages that contain a meta-circular evaluator, a self-interpreter, or that are self-hosting? How could this post be improved (either from the perspective of accuracy or of advocacy?)

A teaser from POPL'07: A Complete, Co-Inductive Syntactic Theory of Sequential Control and State by Støvring and Lassen.

We present a new co-inductive syntactic theory, eager normal
form bisimilarity, for the untyped call-by-value lambda calculus
extended with continuations and mutable references.

We demonstrate that the associated bisimulation proof principle
is easy to use and that it is a powerful tool for proving equivalences
between recursive imperative higher-order programs.

The theory is modular in the sense that eager normal form
bisimilarity for each of the calculi extended with continuations
and/or mutable references is a fully abstract extension of eager
normal form bisimilarity for its sub-calculi. For each calculus, we
prove that eager normal form bisimilarity is a congruence and is
sound with respect to contextual equivalence. Furthermore, for the
calculus with both continuations and mutable references, we show
that eager normal form bisimilarity is complete: it coincides with
contextual equivalence.

Sigfpe

...sometimes you can write useful Haskell code merely by writing something that type checks successfully. Often there's only one way to write the code to have the correct type. Going one step further: the Curry-Howard isomorphism says that logical propositions corresponds to types. So here's a way to write code: pick a theorem, find the corresponding type, and find a function of that type.

Learning category theory and formal logic by writing proofs in Haskell.

Cool. :-D

from channel9.msdn.com:

Programming in the Age of Concurrency: Software Transactional Memory

Recently, we visited MSR Cambridge(UK) to meet some of the great minds working there. In this case, we were fortunate enough to get an hour's time with Simon Peyton-Jones and Tim Harris, who are researchers working on a very hard problem: making it easier (more predictable, more reliable, more composable) to write concurrent applications in this the age of Concurrency (multi-core is a reality, not a dream).

I've built a search engine dedicated to searching sites about programming languages (with an emphasis on theory) using the Google co-op services. You can find the search engine at: http://www.cdiggins.com/search/

Now you don't have to append your Google searches with extra superflous terms like "fish language" or "cat language" or "mixin types", you can just type in "fish", "cat" or "mixin".

There is still a fair amount of work to be done to fine-tune it, and increase the number of sites it searches. Let me know though if you can think of ways it can be improved.

"Lisp is the Red Pill" by Conrad Barski, M.D. (Title taken from John Fraser's c.l.l. post of long ago) at Ebenezer's Coffee House (They have this awesome conference/party room in the basement...). An attempt will be made to introduce people to Lisp and to give them a flavor of the crown jewels of Lisp/Scheme: closures, true macros, continuations, etc. We will create a small video game and use examples from my Lisp Comic Book Casting SPELs in Lisp! Then, I'll give a sneak peek at my followup comic book- A web-based game that illustrates the essence of Scheme continuations! Also, Beer and Pizza at a nearby deep dish pizzeria after the presentation :)

http://www.lisperati.com/fringedc.html

Thanks!

--
Conrad Barski, M.D.

hi,

can someone help me out, i need the code for below 2 functions:

Question)Implement the higher order insertion sort algorithm hoInsertSort which
is similar to insertion sort except that an element x is placed before an
element y if fun x b is a function taken
as input by higher order insertion sort. In other words, the result of
evaluating hoInsertSort fun xs should be a list [y1,y2,..., yn] such
that
fun y1

-- Higher order insertion sort
-- Hint: first write a function hoins that inserts an element
-- in the right place
hoins :: Ord b => (a -> b) -> a -> [a] -> [a]
//add your code here

-- The function hoInsertionSort sorts a list

hoInsertionSort :: Ord b => (a -> b) -> [a] -> [a]
//add your code here

Here is a simple idea intended to plug a few semantic holes in the imperative programming style. The idea is to provide a full proof way to handle mutable state in imperative programs. Basically we want to introduce a class called an ASTB or applicative state transition block. The definition is simple. We will need four data structures: a read only state, and a write only temporary state a structure to hold the input and one for the output. There seem to be six external methods: a driver that provides an input and starts the computation of the new state, and returns the output on completion. A constructor and a destructor, and a method to read the state and output at any time. We need one more external method to initialize the state. This is a little more tricky so we will provide some sort of security, and only allow update when a transition is not in progress (some sort of mutex lock).

Internally the object does the following: when an input is supplied a series of functions compute new state values and output values and puts them in the temporary state data structure, and the output data structure. Internally there is a method that has permission to transfer the temporary state to the state when the output is returned. That seems to be enough to do the job, although we might also want a temporary output, and an output, and transfer that on completion with a lock. This wouldn't be needed if we output through the driver return value.

There is certainly nothing new about this and we suspect that there are patterns for doing this. The point is that we want to make the case that there are sound ways to handle state, get comments, and perhaps encourage a little more attention to these issues.