Lambda the Ultimate

C. Guy Yarvin recently published an interesting new project in language/systems design. It includes a simple formal model of computation called Nock ("comparable to the lambda calculus, but meant as foundational system software rather than foundational metamathe­matics") and a self-hosted language called Watt that compiles to Nock. The motivation? To provide a fully-specified foundation for Urbit, a hypothetical system architecture that uses content-centric networking to distribute code and data in a functional global namespace.

Yarvin's own descriptions are rather lengthy, so I tried to provide a shorter introduction here.

Interesting questions for LtU readers: Nock formulas are terribly inefficient for real computation (for example, decrement(n) is an O(n) operation). Yarvin intends to make Watt efficient by writing fast implementations (in C, say) for standard "kernel" functions like decrement, add, multiply, and more. He calls these fast native implementations "jets." So how one can trust that jets are equivalent to the functional Nock/Watt code that they replace? Yarvin has proposed the classic n-version software engineering trick of comparing both implementations with the same inputs, but in addition the classic problems with that approach, there is the additional hurdle that the pure Nock code might be so inefficient that it is impractical to run it on most inputs. Is the goal of a minimal pure standard compromised by the need to implement a common set of "impure" jets too?

I came across this paper proposing that Let Should Not Be Generalized (TLDI 2010, Vytiniotis, Peyton Jones, and Schrijvers).

While generalisation for local let bindings is straightforward in Hindley-Milner, we show that it becomes much more complicated in more sophisticated type systems. The extensions we have in mind include functional dependencies, GADTs, units of measure, and type functions. The only technically straightforward way to combine these developments with let-generalisation has unpalatable practical consequences, that appear to be unavoidable.

I'm actually fairly convinced by this. Among other things, it provides a fairly clear path to eliminating the monomorphism restriction:

Our [] proposal completely subsumes the [Haskell monomorphism restriction] for local let bindings, so the MR would then only apply to top-level bindings. In that case the arguments for its abolition, or for generating a warning rather than rejecting the program, would become very strong. A nasty wart would thereby be removed from the face of Haskell.

Are they right? Are they wrong? Has anyone laid out the case for the defense?

I am pleased to announce that LaTiKi is now available as a public beta.

LaTiKi accepts LaTeX syntax as input rather than the wiki syntax that is
standard across many wiki implementations. This Wiki enables LaTeX users to
collaborate on papers, edit, and track each paper. It is entirely based upon
the open-source and widely used platform MediaWiki. I am looking for
interested users to contribute, try out how well the system works and how
useful the system really is. I also hope that any major underlying bugs are
identified.

I have prepared a sandbox wiki with some of Philip Wadler's papers on the
site to demonstrate how the system works. Note that to be able to edit
papers on the sandbox you MUST sign up to the site and confirm your email
address. This is available at http://www.stuartbeard.com/wiki
Feedback is greatly appreciated.

If any readers are interested in this project and would like to do a similar
thing with their own papers then a tarball is available
at http://www.stuartbeard.com/project or http://www.mediafire.com/file/lymzlwz3m0m/latexwiki-1.0.1b.tar

I've been watching the interpreter and JIT compiler competitions a bit in the JavaScript and Lua worlds. I haven't collected much organized data but the impression I'm getting is that tracing JIT's are turning up as the winners: sometimes even beating programs statically compiled with GCC. Is there a growing body of evidence that tracing JIT compilers are the horse to bet on? Will a more static style JIT like Google's V8 be able to keep up?

Thanks,
Peter

[I promoted this item to the front page, since the discussion is highly interesting & informative. -- Ehud]

didn't see it mentioned yet. i would excerpt the abstract were it not for the fact that the pdf is horribly broken such that no spaces are copied-and-pasted. yay usability.

the gist: statically typed collections library ends up with duplication, ironically? and new advances let it be excitingly refactored to make everybody happy again. i think that is interesting because i do believe static typing has some gotchyas.

Hi! Let's say it makes a lot of sense in my domain to define the types WriteReference and ReadOnlyReference. I wish to create a monad that manipulates references, so my first idea was to define


(>>=) :: WriteReference a -> (a -> WriteReference b) -> WriteReference b
(>>=) :: WriteReference a -> (a -> ReadOnlyReference b) -> ReadOnlyReference b
(>>=) :: ReadOnlyReference a -> (a -> ReadOnlyReference b) -> ReadOnlyReference b
(>>=) :: ReadOnlyReference a -> (a -> WriteReference b) -> WriteReference b

return :: a -> ReadOnlyReference a


It looks ugly but it does its job, even though I fear it won't play nice with Haskell syntactic sugar for monads.

Does it make more sense to define Reference as a class, and then to define WriteReference and ReadOnlyReference as instances of this class, so that we can write something like:


data WR a = WR a
data RR a = RR a

bind :: (Reference r1, Reference r2) => r1 a -> (a -> r2 b) -> r2 b
bind e k = let x = get e in k x


Can anyone help me understand why I should favor one approach over the other?

Thanks

I've been thinking about the feasibility of a type system that incorporated the type of variable into its name using symbols.

E.g.:
var @4-VariableName;


The system could use symbols like @, #, $ and % for signed, unsigned, character and object and the number would be the size of the variable in bytes (objects wouldn't have this) and the hyphen to separate the name from the type. The symbols would be used every time the variable is used (for the programmer's advantage of readability).

So what are people's views on this idea?

Hi all,

I want to make a minimal set of LISP functions, by which all computable functions on S-Expressions
can be computed. {car, cons, cdr, atom, equal, if} is a basis. I don't know how to prove that this is the minimal. Can you help me?

What advantages does purity offer in a programming language? I often hear (read) about these advantages, but never with concrete examples. I figured here is the best place in the whole www to ask this question :)

Gerald P. Weinberg's second law says: "If builders built houses the way programmers build programs, the first woodpecker that came along would destroy civilization." We've all heard that one, right?

Thousands of reams of paper have been spent (wasted?) on "what can we do about it?" And, to date, we don't have really good answers. A single bit going stray usually crashes a program, or causes it to give ridiculously wrong answers. Every program has to have everything it depends on arranged just so, or it ignominiously fails or bails out with an error. And entire industries are built around putting together suites of software that don't have conflicting requirements that prevent them from working together, or babysitting complicated applications that will die horribly if there is so much as a bobble in any of a score of systems that provide it with a score of different things it needs.

What we've seldom done is to look at the relatively robust very large systems that we *have* studied and try to abstract principles that can be applied to programming. Two such systems are ecologies and free markets. Both are characterized by: many relatively independent agents with limited lifespans; agents in proximity, even if previously unknown to each other, are able to perceive each other and interact; competition and cooperation between independent agents; a small number of outliers, atavisms, recessives and contrarians constantly explore non-mainstream strategies for many generations, even when those strategies have failed or had limited success in the past; survival/reproduction advantages given to more efficient (or more correct) agents; diminished returns for doing something when there are many agents which do that same thing, and, crucially, dynamic reconfiguration of dependencies in that when some agent fails (dies or goes out of business) other agents that formerly depended on its output can switch to depending on different agents rather than dying or going out of business themselves.

Can these lessons be taken to heart in a software system or programming paradigm? Should threads "pay" other threads for services, in tokens redeemable for compute time or memory space (and, in finding a "going rate", eliminate inefficient providers?) How would we simulate "ecology" or "marketplace" of services that different threads can provide, to one another and ultimately to end-user programs? Should threads reproduce or "copy successful business strategies" automatically?

I think you'd need to keep track of state pretty carefully. If a subcontractor makes a hash of something, or dies due to an error, you need the power to detect the problem, revert your data, and hire a different subcontractor. So each thread would need data versioning, or something like it; the power to remember the current state of its own local environment, and return to that state if needed. You'd also need to automatically check subcontractors' work against each other from time to time, to detect errors/cheaters.

I think you'd need a "DoOneOf" statement, for trying to do something in each (or all) of many different ways (or via subcontracting to many different threads or spawning many different threads) and proceeding if any one of them is successful.

I think you'd need to automatically make occasional "configuration tests" (maybe whenever launching new threads of the relevant type) even when things were going fine, to find, for example, databases at new locations, new network interfaces, etc. This might be handled via a "DoOneOf" mentioned above - and would also automate load-balancing, since the query to the least-used database or interface would tend to return first and thereby get "paid" for the completion of the task.

I think you'd need capabilities (revocable or failable service hooks via other threads) rather than a simple linked-call interface.

How, in a programming language, would you handle a marketplace of software services, where threads advertise what they do and offer rates for which they'll do it (and the schedules on which they will do it, where appropriate)? Can that be abstracted below programmer notice, or not?

Ray