Lambda the Ultimate

Trying to get to grips with continuations I was looking at Scheme's call/cc (not being a Scheme programmer). I think I have a sufficient idea what a continuation is, I think of it as a snapshot of the current call stack. My question now is specifically, why do I have to provide a function argument to call/cc, what is the rational for this design? Why doesn't call/cc just return the current continuation as a value, so I could do whatever I please with it (store it, call it, pass it around, etc.)? On this page, it talks about "Essentially it's just a clean way to get the continuation to you and keep out of the way of subsequent jumps back to the saved point.", but I'm not getting it. It seems unnecessarily complicated. Can anybody enlighten me?

On my way to publishing my programming language Dawn (which I radically failed to promote for discussion in earlier posts :-) I have created and released a tool BNFT.

The tool takes a BNF input, a source file and outputs a target file. The BNF features an operator "->" where literals and nonterminals specified on the right side of the operator replaces the leftside in the output. This makes it suitable for a lot of purposes:

DSL creation, Advanced substitions (more advance that RegExps), Code prettifying etc.

The tools is vital in Dawns claim of syntax agnosticism, where programmers are allowed to roll their own syntax, while observering a few rules, that will allow other syntax flavors to view the same code with different syntaxes.

It is implemented in Java for now, windows examples are available and released under BSD license.

Feel free to try it out at my blog: Consistent Oxymoron, Neutral Bias, or something

Disclaimers: i'm struggling to grok half of the words in the paper, so it might not be as interesting as i think it is. I searched but didn't find it explicitly mentioned before on LtU.

The abstract of the paper says:

We recast dataflow in a modern categorical light using profunctors as a generalisation of relations. The well known causal anomalies associated with relational semantics of indeterminate dataflow are avoided, but still we preserve much of the intuitions of a relational model. The development fits with the view of categories of models for concurrency and the general treatment of bisimulation they provide. In particular it fits with the recent categorical formulation of feedback using traced monoidal categories. The payoffs are: (1) explicit relations to existing models and semantics, especially the usual axioms of monotone IO automata are read off from the definition of profunctors, (2) a new definition of bisimulation for dataflow, the proof of the congruence of which benefits from the preservation properties associated with open maps and (3) a treatment of higher-order dataflow
as a biproduct, essentially by following the geometry of interaction programme.

I've been having trouble finding papers on giving a categorical semantics to F or F_\omega. I know the book "Categorical Logic and Type Theory" gets into this material a bit, but I'm presuming there's been papers on the subject that I'm just entirely ignorant of. Does anyone have pointers?

Cheers,

Internet servers are good applications for scripting, e.g. VCL for the Varnish HTTP cache.

Now there's again talk about using Lua for Apache configuration.

Choice quote:

Can all be done in plain lua.

Given that there's MetaLua, it might even be possible to create Apache-specific syntax.

(via Hacker News)

Create Your Own Programming Language by Marc-André Cournoyer.

I love these quotes, and I think that LtU had its part in making programming languages the hot new thing to build up your online reputation:

The ultimate system to achieve every programmer’s dream.

Become the next Guido Van Rossum, Matz, Larry Wall or Rasmus Lerdorf by creating your own revolutionary programming language in a few days.

Impress your employer and peers with a résumé that says: I created my own programming language.

Sorry if this is OT, but I can't for the life of me figure out which paper I saw this in. I'm trying to gather some papers on the expression problem, and I recall one paper that was not specifically about the expression problem, but that mentioned a solution, hence my difficulty finding it.

The paper dealt with type classes, and one of the subsections specifically mentioned that the structure described in the paper incidentally implied a solution to the expression problem using type classes. So the mention of the expression problem was only an aside; not a footnote, it was discussed in a subsection of the paper itself. I don't recall if the solution described was actually novel, but IIRC the discussion in the paper implied that it was.

I remember the paper was in a two-column format if that helps, and I believe it was published after 2005, but I can't be certain. I'm almost certain I have it somewhere on my hard drive, but I haven't been able to find it in all my manual inspections, greping and file system searching. I'm pretty sure I came across it in the past 6 months, a year at the most, so it may have been posted to LtU. It doesn't seem to be on any list of links describing solutions to the expression problem, like this one.

If anyone has any clue, I'd very much appreciate a heads up!

Hello everybody,

I ask you to excuse my ignorance in the question, I am a hobbyist programmer and I don't have any degree in CS. Recently I've found that some operations on types in advanced type systems are quite similar to logical operators.
For example, algebraic types are similar to exclusive OR operation, and multiple inheritance looks a lot loke AND operation.

I am sure this has been discovered and studied before (I can even remember reading about something similar in Wikipedia), but I cannot find any papers on the subject, probably because keywords like "type system" and "logical operators" do not really yield relevant results.

So, if such similarity exists, does it have a name? And what paper could you recommend that are relevant to this?

I'm carrying out some experiments in theorem proving using combinator logic with equality, the rationale being that combinator logic is a variable-free substitute for lambda calculus, and getting rid of variables simplifies both semantics and code quite a bit.

I've run into a stumbling block for which suggests that I'm missing some inference rules, and would appreciate it if anyone could point me to what I'm missing. Here's what I have so far.

In first-order predicate calculus, practically all inference can be boiled down to two rules:

Unification: consistent substitution of terms for variables.
This would seem to be unnecessary in combinator logic, since there are no variables.

Paramodulation: free substitution of equals for equals.
This translates directly, and I have implemented it accordingly.

Lambda calculus adds a third rule:

Evaluation: expanding out a function call.
The obvious equivalent of this in combinator logic is expanding out full combinator calls, where I is given one argument, K is given two arguments or S is given three arguments; I have implemented this.

The simplest case on which the resulting system trips up is the set of clauses p(X) and ~p(X), which in first-order predicate calculus easily resolve to a contradiction. Translating these formulas and each step of the refutation proof into combinator logic gives (using Unlambda's ` notation, `a b means a(b)):

p(X)
p(X)=true
``eq ``s `k [p] i `k true

~p(X)
(p(X)=false)=true
``eq ``s ``s ``s `k s ``s ``s `k s ``s `k k `k eq `k i ``s `k k `k false ``s `k [p] i `k true

p(X) in the first statement unifies with p(X) in the second statement
p(X)=true, so in the second statement, substitute true for p(X)
(false=true)=true
``eq ``s ``s ``s `k s ``s ``s `k s ``s `k k `k eq `k i ``s `k k `k false `k true `k true

So far so good?
Now,
(false=true) trivially simplifies to false
But my program can't see how to simplify eq `k i ``s `k k `k false `k true and neither can I.

Why does (false=true) trivially simplify to false?
Because the inputs are constants not functions, and with constants, literal inequality means logical inequality
But the same is not true for functions
In the case of eq `k i ``s `k k `k false `k true the inputs to the equals comparison are functions, so there is no general rule that will determine they are unequal.

So what am I missing?

Back in university, I only learned to analyse running times of simple imperative algorithms. I don't see how the techniques extend to higher order algorithms, or ones that rely on lazy evaluation. I've looked at papers describing lazy algorithms, but their running times are only analysed in hand-waving form. Is that the best anyone can do, or are there better ways? I haven't seen anything even attempt to describe the running time of higher order algorithms.

I'm exploring for my own interest adding support for proofs of worst-case running time to a lazy language with first-class functions, possibly using dependent types, and I'm trying to see what notation and techniques are already used out there for doing the proofs by hand.

So, got any papers or languages relevant to this?